[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
⊢ SolutionSetCondition G
[PROOFSTEP]
intro A
[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
⊢ ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
[PROOFSTEP]
refine' ⟨PUnit, fun _ => (leftAdjoint G).obj A, fun _ => (Adjunction.ofRightAdjoint G).unit.app A, _⟩
[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
⊢ ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, (fun x => NatTrans.app (Adjunction.ofRightAdjoint G).unit A) i ≫ G.map g = h
[PROOFSTEP]
intro B h
[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ i g, (fun x => NatTrans.app (Adjunction.ofRightAdjoint G).unit A) i ≫ G.map g = h
[PROOFSTEP]
refine' ⟨PUnit.unit, ((Adjunction.ofRightAdjoint G).homEquiv _ _).symm h, _⟩
[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
B : D
h : A ⟶ G.obj B
⊢ (fun x => NatTrans.app (Adjunction.ofRightAdjoint G).unit A) PUnit.unit ≫
      G.map (↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint G) A B).symm h) =
    h
[PROOFSTEP]
rw [← Adjunction.homEquiv_unit, Equiv.apply_symm_apply]
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
⊢ IsRightAdjoint G
[PROOFSTEP]
refine' @isRightAdjointOfStructuredArrowInitials _ _ _ _ G ?_
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
⊢ ∀ (A : C), HasInitial (StructuredArrow A G)
[PROOFSTEP]
intro A
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
A : C
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
specialize hG A
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
hG : ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
choose ι B f g using hG
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
let B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
have hB' : ∀ A' : StructuredArrow A G, ∃ i, Nonempty (B' i ⟶ A') :=
  by
  intro A'
  obtain ⟨i, _, t⟩ := g _ A'.hom
  exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
⊢ ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
[PROOFSTEP]
intro A'
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
A' : StructuredArrow A G
⊢ ∃ i, Nonempty (B' i ⟶ A')
[PROOFSTEP]
obtain ⟨i, _, t⟩ := g _ A'.hom
[GOAL]
case intro.intro
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
A' : StructuredArrow A G
i : ι
w✝ : B i ⟶ A'.right
t : f i ≫ G.map w✝ = A'.hom
⊢ ∃ i, Nonempty (B' i ⟶ A')
[PROOFSTEP]
exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
obtain ⟨T, hT⟩ := has_weakly_initial_of_weakly_initial_set_and_hasProducts hB'
[GOAL]
case intro
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
T : StructuredArrow A G
hT : ∀ (X : StructuredArrow A G), Nonempty (T ⟶ X)
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
apply hasInitial_of_weakly_initial_and_hasWideEqualizers hT
