exists_fin_quot_equiv — Mathlib

English

There exist n and a Submodule S of Fin n → R such that the quotient (Fin n → R)/S is linearly isomorphic to M.

Русский

Существуют n и подмодуль S ⊆ (Fin n → R), такой что тormanный фактор-модуль (Fin n → R)/S изоморфен M по линейному отображению.

LaTeX

$$$\\exists n (S : Submodule R (Fin n \to R)), Nonempty ((Fin n \to R) / S \simeq_\\!{R} M).$$$

Lean4

/-- A finite module can be realised as a quotient of `Fin n → R` (i.e. `R^n`). -/
theorem exists_fin_quot_equiv (R M : Type*) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] :
    ∃ (n : ℕ) (S : Submodule R (Fin n → R)), Nonempty ((_ ⧸ S) ≃ₗ[R] M) :=
  let ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  ⟨n, LinearMap.ker f, ⟨f.quotKerEquivOfSurjective hf⟩⟩

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