English
In a commutative diagram with surjective left, bijective middle, and injective right vertical maps, Exact f g is equivalent to Exact f' g' for the bottom row.
Русский
В коммутативной диаграмме с сюръективной левой части, биективной средней и инъективной правой, точность верхней пары эквивалентна точности нижней пары.
LaTeX
$$$$ \\text{Given } f,g,f',g',\\tau_1,\\tau_2,\\tau_3 \\text{ with the stated commutativity and surjectivity/bijectivity/injectivity } \\operatorname{Exact}(f,g) \\iff \\operatorname{Exact}(f',g'). $$$$
Lean4
/-- When we have a commutative diagram from a sequence of two linear maps to another,
such that the left vertical map is surjective, the middle vertical map is bijective and the right
vertical map is injective, then the upper row is exact iff the lower row is.
See `ShortComplex.exact_iff_of_epi_of_isIso_of_mono` in the file
`Mathlib/Algebra/Homology/ShortComplex/Exact.lean` for the categorical version of this result. -/
theorem exact_iff_of_surjective_of_bijective_of_injective {M₁ M₂ M₃ N₁ N₂ N₃ : Type*} [AddCommMonoid M₁]
[AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R M₁]
[Module R M₂] [Module R M₃] [Module R N₁] [Module R N₂] [Module R N₃] (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃)
(f' : N₁ →ₗ[R] N₂) (g' : N₂ →ₗ[R] N₃) (τ₁ : M₁ →ₗ[R] N₁) (τ₂ : M₂ →ₗ[R] N₂) (τ₃ : M₃ →ₗ[R] N₃)
(comm₁₂ : f'.comp τ₁ = τ₂.comp f) (comm₂₃ : g'.comp τ₂ = τ₃.comp g) (h₁ : Function.Surjective τ₁)
(h₂ : Function.Bijective τ₂) (h₃ : Function.Injective τ₃) : Function.Exact f g ↔ Function.Exact f' g' :=
AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective f.toAddMonoidHom g.toAddMonoidHom f'.toAddMonoidHom
g'.toAddMonoidHom τ₁.toAddMonoidHom τ₂.toAddMonoidHom τ₃.toAddMonoidHom (by ext; apply DFunLike.congr_fun comm₁₂)
(by ext; apply DFunLike.congr_fun comm₂₃) h₁ h₂ h₃
