Theorems · Theorem · commutative algebra

Subalgebra.LinearDisjoint.isDomain_of_injective

∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [IsDomain S]
  {A : Type u_1} {B : Type u_2} [inst_4 : Semiring A] [inst_5 : Semiring B] [inst_6 : Algebra R A]
  [inst_7 : Algebra R B] {fa : A →ₐ[R] S} {fb : B →ₐ[R] S},
  Function.Injective ⇑fa → Function.Injective ⇑fb → fa.range.LinearDisjoint fb.range → IsDomain (TensorProduct R A B)

If A and B are R-algebras, such that there exists a domain S over R such that A and B inject into it and their images are linearly disjoint, then A ⊗[R] B is also a domain.

Defined in

Mathlib.RingTheory.LinearDisjoint

Cited by

1 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraIsDomainSemiringSemiringAlgebraAlgebra