injective_of_surjective_of_injective_of_injective

English

In a commutative diagram of modules with exact rows, if i1 is surjective, i2 is injective, and i4 is injective, then i3 is injective.

Русский

В коммутативной диаграмме модулей с точной строкой, если i1 сюръективен, i2 инъективен, а i4 инъективен, то i3 инъективен.

LaTeX

$$$$\operatorname{Surjective}(i_1) \land \operatorname{Injective}(i_2) \land \operatorname{Injective}(i_4) \Rightarrow \operatorname{Injective}(i_3).$$$$

Lean4

/-- One four lemma in terms of modules. For a diagram explaining the variables,
see the module docstring. -/
theorem injective_of_surjective_of_injective_of_injective (hi₁ : Function.Surjective i₁) (hi₂ : Function.Injective i₂)
    (hi₄ : Function.Injective i₄) : Function.Injective i₃ :=
  AddMonoidHom.injective_of_surjective_of_injective_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₁ hf₂ hg₁
    hi₁ hi₂ hi₄

Похожие утверждения