finsupp — Mathlib

English

Free modules over discrete index sets are flat; in particular, the finsupp module (ι → R) is faithfully flat when ι is nonempty.

Русский

Свободные модули над конечными/дискретными индексами плоски; например, модуль finsupp над ι верноподобен, если ι непуст.

LaTeX

$$$\forall \iota\ [\text{Nonempty }\iota]:\mathsf{Finsupp}_R(\iota)\text{ is FaithfullyFlat over }R$$$

Lean4

/-- Free `R`-modules over discrete types are flat. -/
instance finsupp (ι : Type v) [Nonempty ι] : FaithfullyFlat R (ι →₀ R) := by
  classical exact of_linearEquiv _ _ (finsuppLEquivDirectSum R R ι)

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