English
If a square is a pushout, then the short complex map g on that pushout is an epimorphism.
Русский
Если квадрат является пуш-аутом, то краткий комплексный отображение g на этом пуш-ауте голый эпиморфизм.
LaTeX
$$IsPushout(f,g,inl,inr) ⇒ Epi(h.shortComplex.g)$$
Lean4
/-- A commutative square in a preadditive category is a pullback square iff
the corresponding diagram `0 ⟶ X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0` makes `X₁` a kernel. -/
noncomputable def isLimitEquivIsLimitKernelFork (sq : CommSq fst snd f g) :
IsLimit (PullbackCone.mk _ _ sq.w) ≃ IsLimit sq.kernelFork
where
toFun
h :=
Fork.IsLimit.mk _
(fun s ↦
PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd)
(by
rw [← sub_eq_zero, assoc, assoc, ← Preadditive.comp_sub]
convert s.condition <;> cat_disch))
(fun s ↦ by
dsimp
ext
· simp only [assoc, biprod.lift_fst]
apply PullbackCone.IsLimit.lift_fst h
· simp only [assoc, biprod.lift_snd]
apply PullbackCone.IsLimit.lift_snd h)
(fun s m hm ↦ by
apply PullbackCone.IsLimit.hom_ext h
· replace hm := hm =≫ biprod.fst
dsimp at hm ⊢
simp only [assoc, biprod.lift_fst] at hm
rw [hm]
symm
apply PullbackCone.IsLimit.lift_fst h
· replace hm := hm =≫ biprod.snd
dsimp at hm ⊢
simp only [assoc, biprod.lift_snd] at hm
rw [hm]
symm
apply PullbackCone.IsLimit.lift_snd h)
invFun
h :=
PullbackCone.IsLimit.mk _ (fun s ↦ h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) (by simp [s.condition])))
(fun s ↦ by
simpa using h.fac (KernelFork.ofι (biprod.lift s.fst s.snd) (by simp [s.condition])) .zero =≫ biprod.fst)
(fun s ↦ by
simpa using h.fac (KernelFork.ofι (biprod.lift s.fst s.snd) (by simp [s.condition])) .zero =≫ biprod.snd)
(fun s m hm₁ hm₂ ↦ by
apply Fork.IsLimit.hom_ext h
convert (h.fac (KernelFork.ofι (biprod.lift s.fst s.snd) (by simp [s.condition])) .zero).symm
cat_disch)
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _
