English
In a commutative diagram of additive groups with exact rows, if i1 and i3 are surjective and i4 is injective, then i2 is surjective.
Русский
В коммутативной диаграмме аддитивных групп с точными рядами, если i1 и i3 сюръективны, а i4 инъективен, то i2 сюръективен.
LaTeX
$$surjective_of_surjective_of_surjective_of_injective hi1 hi3 hi4 : Function.Surjective i1 → Function.Surjective i3 → Function.Injective i4 → Function.Surjective i2$$
Lean4
/-- One four lemma in terms of (additive) groups. For a diagram explaining the variables,
see the module docstring. -/
theorem surjective_of_surjective_of_surjective_of_injective (hi₁ : Function.Surjective i₁)
(hi₃ : Function.Surjective i₃) (hi₄ : Function.Injective i₄) : Function.Surjective i₂ :=
by
intro x
obtain ⟨y, hy⟩ := hi₃ (g₂ x)
obtain ⟨a, rfl⟩ : y ∈ Set.range f₂ :=
(hf₂ _).mp <| by simpa [hy, hg₂.apply_apply_eq_zero, map_eq_zero_iff _ hi₄] using (DFunLike.congr_fun hc₃ y).symm
obtain ⟨b, hb⟩ : x - i₂ a ∈ Set.range g₁ :=
(hg₁ _).mp <| by simp [← hy, show g₂ (i₂ a) = i₃ (f₂ a) by simpa using DFunLike.congr_fun hc₂ a]
obtain ⟨o, rfl⟩ := hi₁ b
use f₁ o + a
simp [← show g₁ (i₁ o) = i₂ (f₁ o) by simpa using DFunLike.congr_fun hc₁ o, hb]
