nontrivial_of_algebraMap_injective_of_flat_right

English

If B is a nontrivial flat R-algebra and there is an injection R → A as algebras, then A ⊗_R B is nontrivial.

Русский

Если B — ненулевой плоский R-алгебра и R инъективно в A, то A ⊗_R B ненулево.

LaTeX

$$$\\text{Nontrivial}(A \\otimes_R B)$ given injective algebraMap R A and $\\text{Module.Flat } R B$, $\\text{Nontrivial } B$$$

Lean4

/-- If `A`, `B` are `R`-algebras, `R` injects into `A`,
and `B` is a nontrivial flat `R`-algebra, then `A ⊗[R] B` is nontrivial. -/
theorem nontrivial_of_algebraMap_injective_of_flat_right (h : Function.Injective (algebraMap R A)) [Module.Flat R B]
    [Nontrivial B] : Nontrivial (A ⊗[R] B) :=
  TensorProduct.nontrivial_of_linearMap_injective_of_flat_right R A B (Algebra.linearMap R A) h

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