English
In a commutative diagram of additive monoid homomorphisms with the outer vertical maps surjective, i2,i4 bijective, i5 injective, and the horizontal maps exact, the middle vertical map i3 is bijective.
Русский
В коммутативной диаграмме гомоморфизмов аддитивных моноидов при внешних отображениях i1,i2,i4 surjective/bijective и i5 injective, и при точности горизонтальных отображений, середина i3 является биективной.
LaTeX
$$$\text{If } i_1,i_2,i_3,i_4,i_5 \\text{and the squares commute with } hf_1,hf_2,hf_3,gf_1,gf_2,gf_3,\text{ with } i_1\text{ surjective}, i_2,i_4\text{ bijective}, i_5\text{ injective}, \\text{then } i_3\text{ is bijective.}$$$
Lean4
/-- The five lemma in terms of (additive) groups. For a diagram explaining the variables,
see the module docstring. -/
theorem bijective_of_surjective_of_bijective_of_bijective_of_injective (hi₁ : Function.Surjective i₁)
(hi₂ : Function.Bijective i₂) (hi₄ : Function.Bijective i₄) (hi₅ : Function.Injective i₅) : Function.Bijective i₃ :=
⟨injective_of_surjective_of_injective_of_injective f₁ f₂ f₃ g₁ g₂ g₃ i₁ i₂ i₃ i₄ hc₁ hc₂ hc₃ hf₁ hf₂ hg₁ hi₁ hi₂.1
hi₄.1,
surjective_of_surjective_of_surjective_of_injective f₂ f₃ f₄ g₂ g₃ g₄ i₂ i₃ i₄ i₅ hc₂ hc₃ hc₄ hf₃ hg₂ hg₃ hi₂.2
hi₄.2 hi₅⟩
