English
In a commutative diagram of modules with exact rows, if i1 is surjective, i3 is surjective, and i4 is injective, then i2 is surjective.
Русский
В коммутативной диаграмме модулей с точной строкой, если i1 сюръективен, i3 сюръективен, а i4 инъективен, то i2 сюръективен.
LaTeX
$$$$\operatorname{Surjective}(i_1) \land \operatorname{Surjective}(i_3) \land \operatorname{Injective}(i_4) \Rightarrow \operatorname{Surjective}(i_2). $$$$
Lean4
/-- One four lemma in terms of modules. 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₂ :=
AddMonoidHom.surjective_of_surjective_of_surjective_of_injective f₁.toAddMonoidHom f₂.toAddMonoidHom f₃.toAddMonoidHom
g₁.toAddMonoidHom g₂.toAddMonoidHom g₃.toAddMonoidHom i₁.toAddMonoidHom i₂.toAddMonoidHom i₃.toAddMonoidHom
i₄.toAddMonoidHom (AddMonoidHom.ext fun x ↦ DFunLike.congr_fun hc₁ x)
(AddMonoidHom.ext fun x ↦ DFunLike.congr_fun hc₂ x) (AddMonoidHom.ext fun x ↦ DFunLike.congr_fun hc₃ x) hf₂ hg₁ hg₂
hi₁ hi₃ hi₄
