instNontrivialTensorProduct — Mathlib

English

If M is a nontrivial module over a ring R and is finite, then the tensor product M ⊗R M is nontrivial.

Русский

Если модуль M над кольцом R не тривиален и конечен, то M ⊗R M не тривиален.

LaTeX

$$$\operatorname{Nontrivial}(M \otimes_R M)$$$

Lean4

instance : Nontrivial (M ⊗[R] M) :=
  by
  obtain ⟨I, ϕ, hI, hϕ⟩ := Module.exists_surjective_quotient_of_finite R M
  let ψ : M ⊗[R] M →ₗ[R] R ⧸ I := (LinearMap.mul' R (R ⧸ I)).comp (TensorProduct.map ϕ ϕ)
  have : Nontrivial (R ⧸ I) := by rwa [← not_subsingleton_iff_nontrivial, Submodule.subsingleton_quotient_iff_eq_top]
  have : Function.Surjective ψ := by intro x; obtain ⟨x, rfl⟩ := hϕ x; obtain ⟨y, hy⟩ := hϕ 1;
    exact ⟨x ⊗ₜ y, by simp [ψ, hy]⟩
  exact this.nontrivial

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