quotTorsionOfEquivSpanSingleton — Mathlib

English

For any x ∈ M, the quotient of R by the torsionOf(x) is canonically isomorphic (as an R-module) to the submodule R · x (the span of x).

Русский

Для любого x ∈ M существует каноническое изоморфное отображение между R/ torsionOf(x) и R · x как R-модуля.

LaTeX

$$$(R \;\grave{\div}\; \operatorname{torsionOf}(R,M,x)) \ \cong_{R} \\ R \cdot x$$

Lean4

/-- The span of `x` in `M` is isomorphic to `R` quotiented by the torsion ideal of `x`. -/
noncomputable def quotTorsionOfEquivSpanSingleton (x : M) : (R ⧸ torsionOf R M x) ≃ₗ[R] R ∙ x :=
  (LinearMap.toSpanSingleton R M x).quotKerEquivRange.trans <|
    LinearEquiv.ofEq _ _ (LinearMap.span_singleton_eq_range R M x).symm

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