English
Two pseudoelements with equal pullback images admit a witness in the pullback making their images match.
Русский
Два псевдоэлемента с равными изображениями по каноническим отображениям тянут существование элемента в пирковдом квадрате, который делает изображения равными.
LaTeX
$$$\\exists s, pullback.fst f g s = p \\land pullback.snd f g s = q$ given $f p=g q$$$
Lean4
/-- If two morphisms are exact on pseudoelements, they are exact. -/
theorem exact_of_pseudo_exact (S : ShortComplex C) (hS : ∀ b, S.g b = 0 → ∃ a, S.f a = b) : S.Exact :=
(S.exact_iff_kernel_ι_comp_cokernel_π_zero).2
(by
-- If we apply `g` to the pseudoelement induced by its kernel, we get 0 (of course!).
have : S.g (kernel.ι S.g) = 0 :=
apply_eq_zero_of_comp_eq_zero _ _
(kernel.condition _)
-- By pseudo-exactness, we get a preimage.
obtain ⟨a', ha⟩ := hS _ this
obtain ⟨a, ha'⟩ := Quotient.exists_rep a'
rw [← ha'] at ha
obtain ⟨Z, r, q, _, eq, comm⟩ := Quotient.exact ha
obtain ⟨z, _, hz₂⟩ :=
@pullback.lift' _ _ _ _ _ _ (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) _
(r ≫ a.hom ≫ Abelian.factorThruImage S.f) q
(by
simp only [Category.assoc, Abelian.image.fac]
exact comm)
-- Let's give a name to the second pullback morphism.
let j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g :=
pullback.snd _
_
-- Since `q` is an epimorphism, in particular this means that `j` is an epimorphism.
haveI pe : Epi j := epi_of_epi_fac hz₂
haveI : IsIso j :=
isIso_of_mono_of_epi
_
-- But then `kernel.ι g` can be expressed using all of the maps of the pullback square, and we
-- are done.
rw [(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm]
simp only [Category.assoc, kernel.condition, HasZeroMorphisms.comp_zero])
