English
Let f: M → N and g: N → P be linear maps forming an exact sequence M → N → P → 0 of R-modules, and assume g is surjective. Then the quotient N / im(f) is canonically isomorphic to P via a linear isomorphism.
Русский
Пусть f: M → N и g: N → P – линейные отображения, образ которых образует точную последовательность M → N → P → 0 над кольцом R, и при этом g сюръективен. Тогда фактор-пространство N / im(f) изоморфно P как линейное пространство.
LaTeX
$$$\left( \operatorname{Im}(f) = \ker(g) \right) \wedge \operatorname{Surj}(g) \Rightarrow (N / \operatorname{range}(f)) \cong_R P$$$
Lean4
/-- The linear equivalence `(N ⧸ LinearMap.range f) ≃ₗ[A] P` associated to
an exact sequence `M → N → P → 0` of `R`-modules. -/
@[simps! apply]
noncomputable def linearEquivOfSurjective (h : Function.Exact f g) (hg : Function.Surjective g) :
(N ⧸ LinearMap.range f) ≃ₗ[R] P :=
LinearEquiv.ofBijective ((LinearMap.range f).liftQ g (h · |>.mpr))
⟨LinearMap.injective_range_liftQ_of_exact h, LinearMap.surjective_range_liftQ _ hg⟩
