English
In a commutative diagram of modules with exact rows, if i1 is surjective, i2, i4 are bijective, i5 is injective, and the four square relations hold (g1∘i1 = i2∘f1, etc.), and the side maps form exact sequences with f and g, then i3 is bijective.
Русский
В коммутативной диаграмме модулей с точными рядами, если i1 сюръективен, i2 и i4 биективны, i5 инъективен, квадраты сходятся (g1∘i1 = i2∘f1 и т.д.), и соответствующие последовательности f и g точны, то i3 биективен.
LaTeX
$$$$\big( \operatorname{Surjective}(i_1) \wedge \operatorname{Bijective}(i_2) \wedge \operatorname{Bijective}(i_4) \wedge \operatorname{Injective}(i_5) \wedge \operatorname{Eq}(g_1 \circ i_1, i_2 \circ f_1) \wedge \operatorname{Eq}(g_2 \circ i_2, i_3 \circ f_2) \wedge \operatorname{Eq}(g_3 \circ i_3, i_4 \circ f_3) \wedge \operatorname{Eq}(g_4 \circ i_4, i_5 \circ f_4) \wedge \operatorname{Exact}(f_1,f_2) \wedge \operatorname{Exact}(f_2,f_3) \wedge \operatorname{Exact}(f_3,f_4) \wedge \operatorname{Exact}(g_1,g_2) \wedge \operatorname{Exact}(g_2,g_3) \wedge \operatorname{Exact}(g_3,g_4) \Big) \Rightarrow \operatorname{Bijective}(i_3). $$$$
Lean4
/-- The five lemma in terms of modules. 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₅⟩
