nontrivial_of_algebraMap_injective_of_flat_left

English

If A and B are R-algebras, R injects into B, and A is a nontrivial flat R-algebra, then A ⊗_R B is nontrivial.

Русский

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

LaTeX

$$$\\text{Nontrivial}(A \\otimes_R B)$ under hypotheses: injective (algebraMap R B), [Module.Flat R A], [Nontrivial A]$$

Lean4

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

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