English
Two morphisms in a short exact sequence are exact on pseudoelements, yielding a pseudo-preimage for any pseudoelement in the target that is killed by g.
Русский
Два морфизма в краткой точной последовательности точны на псевдоэлементах, давая псевдообраз для любого псевдоэлемента в цели, который уничтожается g.
LaTeX
$$$S.Exact \\Rightarrow \\forall b, S.g(b)=0 \\Rightarrow \\exists a, S.f(a)=b$$$
Lean4
/-- Two morphisms in an exact sequence are exact on pseudoelements. -/
theorem pseudo_exact_of_exact {S : ShortComplex C} (hS : S.Exact) : ∀ b, S.g b = 0 → ∃ a, S.f a = b := fun b' =>
Quotient.inductionOn b' fun b hb =>
by
have hb' : b.hom ≫ S.g = 0 := (pseudoZero_iff _).1 hb
obtain ⟨c, hc⟩ := KernelFork.IsLimit.lift' hS.isLimitImage _ hb'
use pullback.fst (Abelian.factorThruImage S.f) c
apply Quotient.sound
refine
⟨pullback (Abelian.factorThruImage S.f) c, 𝟙 _, pullback.snd _ _, inferInstance, inferInstance, ?_⟩
-- Now we can verify that the diagram commutes.
calc
𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫ pullback.fst _ _ ≫ S.f = pullback.fst _ _ ≫ S.f :=
Category.id_comp _
_ = pullback.fst _ _ ≫ Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f) := by rw [Abelian.image.fac]
_ = (pullback.snd _ _ ≫ c) ≫ kernel.ι (cokernel.π S.f) := by rw [← Category.assoc, pullback.condition]
_ = pullback.snd _ _ ≫ b.hom := by
rw [Category.assoc]
congr
