mem_baseChange_iff — Mathlib

English

Let m be a element of A ⊗_R M. Then m belongs to the base change N.baseChange A if and only if m lies in the spans of the image of N under the canonical map n ↦ 1 ⊗ n.

Русский

Пусть m ∈ A ⊗_R M. Тогда m ∈ baseChange_A(N) тогда и только тогда, когда m лежит в A-обобщении образа N под каноническим отображением n ↦ 1 ⊗ n.

LaTeX

$$$ m \\in N.bas eChange A \\;\\iff\\; m \\in \\operatorname{span}_A\\bigl( (N : \\operatorname{Submodule}_R M).map (\\operatorname{TensorProduct.mk} R A M 1) \\bigr) $$$

Lean4

theorem mem_baseChange_iff {m : A ⊗[R] M} :
    m ∈ N.baseChange A ↔ m ∈ Submodule.span A ((N : Submodule R M).map (TensorProduct.mk R A M 1)) := by
  rw [← Submodule.baseChange_eq_span]; rfl

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