[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesMonomorphisms F
inst✝ : PreservesMonomorphisms G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Mono f
⊢ Mono ((F ⋙ G).map f)
[PROOFSTEP]
rw [comp_map]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesMonomorphisms F
inst✝ : PreservesMonomorphisms G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Mono f
⊢ Mono (G.map (F.map f))
[PROOFSTEP]
exact inferInstance
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesEpimorphisms F
inst✝ : PreservesEpimorphisms G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Epi f
⊢ Epi ((F ⋙ G).map f)
[PROOFSTEP]
rw [comp_map]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesEpimorphisms F
inst✝ : PreservesEpimorphisms G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Epi f
⊢ Epi (G.map (F.map f))
[PROOFSTEP]
exact inferInstance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : PreservesMonomorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono f
⊢ Mono (G.map f)
[PROOFSTEP]
haveI : Mono (F.map f ≫ (α.app Y).hom) := mono_comp _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : PreservesMonomorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono f
this : Mono (F.map f ≫ (α.app Y).hom)
⊢ Mono (G.map f)
[PROOFSTEP]
convert (mono_comp _ _ : Mono ((α.app X).inv ≫ F.map f ≫ (α.app Y).hom))
[GOAL]
case h.e'_5
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : PreservesMonomorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono f
this : Mono (F.map f ≫ (α.app Y).hom)
⊢ G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom
[PROOFSTEP]
rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : PreservesEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
⊢ Epi (G.map f)
[PROOFSTEP]
haveI : Epi (F.map f ≫ (α.app Y).hom) := epi_comp _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : PreservesEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
this : Epi (F.map f ≫ (α.app Y).hom)
⊢ Epi (G.map f)
[PROOFSTEP]
convert (epi_comp _ _ : Epi ((α.app X).inv ≫ F.map f ≫ (α.app Y).hom))
[GOAL]
case h.e'_5
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : PreservesEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
this : Epi (F.map f ≫ (α.app Y).hom)
⊢ G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom
[PROOFSTEP]
rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : ReflectsMonomorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ Mono f
[PROOFSTEP]
apply F.mono_of_mono_map
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : ReflectsMonomorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ Mono (F.map f)
[PROOFSTEP]
haveI : Mono (G.map f ≫ (α.app Y).inv) := mono_comp _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : ReflectsMonomorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
this : Mono (G.map f ≫ (α.app Y).inv)
⊢ Mono (F.map f)
[PROOFSTEP]
convert (mono_comp _ _ : Mono ((α.app X).hom ≫ G.map f ≫ (α.app Y).inv))
[GOAL]
case h.e'_5
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : ReflectsMonomorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
this : Mono (G.map f ≫ (α.app Y).inv)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
[PROOFSTEP]
rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi f
[PROOFSTEP]
apply F.epi_of_epi_map
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi (F.map f)
[PROOFSTEP]
haveI : Epi (G.map f ≫ (α.app Y).inv) := epi_comp _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
this : Epi (G.map f ≫ (α.app Y).inv)
⊢ Epi (F.map f)
[PROOFSTEP]
convert (epi_comp _ _ : Epi ((α.app X).hom ≫ G.map f ≫ (α.app Y).inv))
[GOAL]
case h.e'_5
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
this : Epi (G.map f ≫ (α.app Y).inv)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
[PROOFSTEP]
rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
⊢ ∀ {Z : D} (g h : F.obj Y ⟶ Z), F.map f ≫ g = F.map f ≫ h → g = h
[PROOFSTEP]
intro Z g h H
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : F.map f ≫ g = F.map f ≫ h
⊢ g = h
[PROOFSTEP]
replace H := congr_arg (adj.homEquiv X Z) H
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : ↑(Adjunction.homEquiv adj X Z) (F.map f ≫ g) = ↑(Adjunction.homEquiv adj X Z) (F.map f ≫ h)
⊢ g = h
[PROOFSTEP]
rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi, Equiv.apply_eq_iff_eq] at H 
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
⊢ ∀ {Z : C} (g h : Z ⟶ G.obj X), g ≫ G.map f = h ≫ G.map f → g = h
[PROOFSTEP]
intro Z g h H
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : g ≫ G.map f = h ≫ G.map f
⊢ g = h
[PROOFSTEP]
replace H := congr_arg (adj.homEquiv Z Y).symm H
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : ↑(Adjunction.homEquiv adj Z Y).symm (g ≫ G.map f) = ↑(Adjunction.homEquiv adj Z Y).symm (h ≫ G.map f)
⊢ g = h
[PROOFSTEP]
rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono, Equiv.apply_eq_iff_eq] at H 
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
inst✝ : Faithful F
X Y : C
f : X ⟶ Y
hf : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map g ≫ F.map f = F.map h ≫ F.map f
[PROOFSTEP]
rw [← F.map_comp, hgh, F.map_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
inst✝ : Faithful F
X Y : C
f : X ⟶ Y
hf : Epi (F.map f)
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
⊢ F.map f ≫ F.map g = F.map f ≫ F.map h
[PROOFSTEP]
rw [← F.map_comp, hgh, F.map_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
s : SplitEpi (F.map f)
⊢ SplitEpi f
[PROOFSTEP]
refine' ⟨F.preimage s.section_, _⟩
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
s : SplitEpi (F.map f)
⊢ F.preimage s.section_ ≫ f = 𝟙 Y
[PROOFSTEP]
apply F.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
s : SplitEpi (F.map f)
⊢ F.map (F.preimage s.section_ ≫ f) = F.map (𝟙 Y)
[PROOFSTEP]
simp only [map_comp, image_preimage, map_id]
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
s : SplitEpi (F.map f)
⊢ s.section_ ≫ F.map f = 𝟙 (F.obj Y)
[PROOFSTEP]
apply SplitEpi.id
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ Function.LeftInverse (fun s => SplitEpi.mk (F.preimage s.section_)) fun f_1 => SplitEpi.map f_1 F
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ Function.RightInverse (fun s => SplitEpi.mk (F.preimage s.section_)) fun f_1 => SplitEpi.map f_1 F
[PROOFSTEP]
simp only [Function.RightInverse, Function.LeftInverse]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ ∀ (x : SplitEpi (F.map f)), SplitEpi.map (SplitEpi.mk (F.preimage x.section_)) F = x
[PROOFSTEP]
intro x
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
x : SplitEpi (F.map f)
⊢ SplitEpi.map (SplitEpi.mk (F.preimage x.section_)) F = x
[PROOFSTEP]
simp only [SplitEpi.map, preimage]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
x : SplitEpi (F.map f)
⊢ SplitEpi.mk (F.map (Full.preimage x.section_)) = x
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitEpi (F.map f) ↔ IsSplitEpi f
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitEpi (F.map f) → IsSplitEpi f
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
h : IsSplitEpi (F.map f)
⊢ IsSplitEpi f
[PROOFSTEP]
exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)
[GOAL]
case mpr
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitEpi f → IsSplitEpi (F.map f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
h : IsSplitEpi f
⊢ IsSplitEpi (F.map f)
[PROOFSTEP]
exact IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
s : SplitMono (F.map f)
⊢ SplitMono f
[PROOFSTEP]
refine' ⟨F.preimage s.retraction, _⟩
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
s : SplitMono (F.map f)
⊢ f ≫ F.preimage s.retraction = 𝟙 X
[PROOFSTEP]
apply F.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
s : SplitMono (F.map f)
⊢ F.map (f ≫ F.preimage s.retraction) = F.map (𝟙 X)
[PROOFSTEP]
simp only [map_comp, image_preimage, map_id]
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
s : SplitMono (F.map f)
⊢ F.map f ≫ s.retraction = 𝟙 (F.obj X)
[PROOFSTEP]
apply SplitMono.id
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ Function.LeftInverse (fun s => SplitMono.mk (F.preimage s.retraction)) fun f_1 => SplitMono.map f_1 F
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ Function.RightInverse (fun s => SplitMono.mk (F.preimage s.retraction)) fun f_1 => SplitMono.map f_1 F
[PROOFSTEP]
simp only [Function.RightInverse, Function.LeftInverse]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ ∀ (x : SplitMono (F.map f)), SplitMono.map (SplitMono.mk (F.preimage x.retraction)) F = x
[PROOFSTEP]
intro x
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
x : SplitMono (F.map f)
⊢ SplitMono.map (SplitMono.mk (F.preimage x.retraction)) F = x
[PROOFSTEP]
simp only [SplitMono.map, preimage]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
x : SplitMono (F.map f)
⊢ SplitMono.mk (F.map (Full.preimage x.retraction)) = x
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitMono (F.map f) ↔ IsSplitMono f
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitMono (F.map f) → IsSplitMono f
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
h : IsSplitMono (F.map f)
⊢ IsSplitMono f
[PROOFSTEP]
exact IsSplitMono.mk' ((splitMonoEquiv F f).invFun h.exists_splitMono.some)
[GOAL]
case mpr
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitMono f → IsSplitMono (F.map f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : Full F
inst✝ : Faithful F
h : IsSplitMono f
⊢ IsSplitMono (F.map f)
[PROOFSTEP]
exact IsSplitMono.mk' ((splitMonoEquiv F f).toFun h.exists_splitMono.some)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
⊢ Epi (F.map f) ↔ Epi f
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
⊢ Epi (F.map f) → Epi f
[PROOFSTEP]
exact F.epi_of_epi_map
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
⊢ Epi f → Epi (F.map f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
h : Epi f
⊢ Epi (F.map f)
[PROOFSTEP]
exact F.map_epi f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
⊢ Mono (F.map f) ↔ Mono f
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
⊢ Mono (F.map f) → Mono f
[PROOFSTEP]
exact F.mono_of_mono_map
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
⊢ Mono f → Mono (F.map f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
h : Mono f
⊢ Mono (F.map f)
[PROOFSTEP]
exact F.map_mono f
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : IsEquivalence F
inst✝ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
⊢ ∀ [inst : Epi f], IsSplitEpi f
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : IsEquivalence F
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi f
[PROOFSTEP]
rw [← F.inv.isSplitEpi_iff f]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : IsEquivalence F
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi ((inv F).map f)
[PROOFSTEP]
apply isSplitEpi_of_epi
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
h₁ : Functor.PreservesMonomorphisms F'
h₂ : Functor.PreservesEpimorphisms F
inst✝ : StrongEpi f
X Y : D
Z : X ⟶ Y
⊢ ∀ [inst : Mono Z], HasLiftingProperty (F.map f) Z
[PROOFSTEP]
intro
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
h₁ : Functor.PreservesMonomorphisms F'
h₂ : Functor.PreservesEpimorphisms F
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty (F.map f) Z
[PROOFSTEP]
rw [adj.hasLiftingProperty_iff]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
h₁ : Functor.PreservesMonomorphisms F'
h₂ : Functor.PreservesEpimorphisms F
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty f (F'.map Z)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
⊢ StrongEpi (F.map f) ↔ StrongEpi f
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
⊢ StrongEpi (F.map f) → StrongEpi f
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi (F.map f)
⊢ StrongEpi f
[PROOFSTEP]
have e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) := Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)
[GOAL]
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk ((inv F).map (F.map f))
⊢ StrongEpi f
[PROOFSTEP]
rw [StrongEpi.iff_of_arrow_iso e]
[GOAL]
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk ((inv F).map (F.map f))
⊢ StrongEpi ((inv F).map (F.map f))
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
⊢ StrongEpi f → StrongEpi (F.map f)
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : IsEquivalence F
a✝ : StrongEpi f
⊢ StrongEpi (F.map f)
[PROOFSTEP]
infer_instance
