subsingleton_tensorProduct — Mathlib

English

For a finitely generated module M over a local ring R with residue field k, Subsingleton (k ⊗_R M) is equivalent to Subsingleton M.

Русский

Для конечно порожденного модуля M над локальным кольцом R с остаточным полем k, Subsingleton (k ⊗_R M) эквивалентен Subsingleton M.

LaTeX

$$$ \operatorname{Subsingleton}(k \otimes_R M) \iff \operatorname{Subsingleton}(M). $$$

Lean4

theorem subsingleton_tensorProduct [Module.Finite R M] : Subsingleton (k ⊗[R] M) ↔ Subsingleton M := by
  rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top, ← Submodule.subsingleton_iff R, ←
    subsingleton_iff_bot_eq_top, ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]

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