subsingleton_tensorProduct_iff_left

English

If N is faithfully flat over R, then Subsingleton(M ⊗R N) is equivalent to Subsingleton(M).

Русский

Если N верноподобна над R, то M ⊗R N тривиален тогда и только тогда, когда M тривиален.

LaTeX

$$$\forall N\ [\text{Module }R N]\ [\text{Module.FaithfullyFlat }R N] \Rightarrow \big( \operatorname{Subsingleton}(M \otimes_R N) \iff \operatorname{Subsingleton}(M) \big)$$$

Lean4

@[simp]
theorem subsingleton_tensorProduct_iff_left [Module.FaithfullyFlat R N] : Subsingleton (M ⊗[R] N) ↔ Subsingleton M :=
  ⟨fun _ ↦ rTensor_reflects_triviality R N M, fun _ ↦ inferInstance⟩

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