C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize F
⊢ ∃ f', f' ≫ g = f
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f
haveI := Adjunction.leftAdjointPreservesColimits.{0, 0} adj
case intro
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ ∃ f', f' ≫ g = f
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize F
⊢ ∃ f', f' ≫ g = f
rcases (@hP).1 (F.map f) (F.map g) with ⟨f', hf'⟩
case intro
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ (adj.unit.app P ≫ G.map f' ≫ inv (adj.unit.app E✝)) ≫ g = f
case intro
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ ∃ f', f' ≫ g = f
use adj.unit.app _ ≫ G.map f' ≫ (inv <| adj.unit.app _)
case intro
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ F.map ((adj.unit.app P ≫ G.map f' ≫ inv (adj.unit.app E✝)) ≫ g) = F.map f
case intro
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ (adj.unit.app P ≫ G.map f' ≫ inv (adj.unit.app E✝)) ≫ g = f
refine' Faithful.map_injective (F := F) _
no goals
case intro
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ F.map ((adj.unit.app P ≫ G.map f' ≫ inv (adj.unit.app E✝)) ≫ g) = F.map f
simpa