[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : IsSplitMono f
inst✝ : Epi f
⊢ f ≫ retraction f = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : IsSplitMono f
inst✝ : Epi f
⊢ retraction f ≫ f = 𝟙 Y
[PROOFSTEP]
simp [← cancel_epi f]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ f ≫ section_ f = 𝟙 X
[PROOFSTEP]
simp [← cancel_mono f]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ section_ f ≫ f = 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : g ≫ f = h ≫ f
⊢ g = h
[PROOFSTEP]
replace w := w =≫ sm.retraction
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : (g ≫ f) ≫ sm.retraction = (h ≫ f) ≫ sm.retraction
⊢ g = h
[PROOFSTEP]
simpa using w
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : f ≫ g = f ≫ h
⊢ g = h
[PROOFSTEP]
replace w := se.section_ ≫= w
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
⊢ g = h
[PROOFSTEP]
simpa using w
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitMono f
inst✝ : Mono hf.retraction
⊢ f ≫ hf.retraction = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitMono f
inst✝ : Mono hf.retraction
⊢ (hf.retraction ≫ f) ≫ hf.retraction = hf.retraction
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f ≫ hf.section_ = hf.section_
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f = 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
⊢ Groupoid C
[PROOFSTEP]
apply Groupoid.ofIsIso
[GOAL]
case all_is_iso
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
⊢ ∀ {X Y : C} (f : X ⟶ Y), IsIso f
[PROOFSTEP]
intro X Y f
[GOAL]
case all_is_iso
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
⊢ IsIso f
[PROOFSTEP]
have ⟨a, _⟩ := Trunc.exists_rep <| all_split_mono f
[GOAL]
case all_is_iso
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h✝ : (_ : Trunc (IsSplitMono f)) = (_ : Trunc (IsSplitMono f))
⊢ IsIso f
[PROOFSTEP]
have ⟨b, _⟩ := Trunc.exists_rep <| all_split_mono <| retraction f
[GOAL]
case all_is_iso
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h✝¹ : (_ : Trunc (IsSplitMono f)) = (_ : Trunc (IsSplitMono f))
b : IsSplitMono (retraction f)
h✝ : (_ : Trunc (IsSplitMono (retraction f))) = (_ : Trunc (IsSplitMono (retraction f)))
⊢ IsIso f
[PROOFSTEP]
apply IsIso.of_mono_retraction
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
sm : SplitMono f
F : C ⥤ D
⊢ F.map f ≫ F.map sm.retraction = 𝟙 (F.obj X)
[PROOFSTEP]
rw [← Functor.map_comp, SplitMono.id, Functor.map_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : C ⥤ D
⊢ F.map se.section_ ≫ F.map f = 𝟙 (F.obj Y)
[PROOFSTEP]
rw [← Functor.map_comp, SplitEpi.id, Functor.map_id]
