English
If A and B are domains over R and the maps algebraMap R → A and algebraMap R → B are injective, then A ⊗_R B is nontrivial.
Русский
Если A и B — домены над R и отображения algebraMap R → A, algebraMap R → B инъективны, то A ⊗_R B не тривиален.
LaTeX
$$Nontrivial (A ⊗_R B)$$
Lean4
/-- If `A`, `B` are `R`-algebras, `R` injects into `A` and `B`, and `A` and `B` are domains
(which implies `R` is also a domain), then `A ⊗[R] B` is nontrivial. -/
theorem nontrivial_of_algebraMap_injective_of_isDomain (R A B : Type*) [CommRing R] [CommRing A] [CommRing B]
[Algebra R A] [Algebra R B] (ha : Function.Injective (algebraMap R A)) (hb : Function.Injective (algebraMap R B))
[IsDomain A] [IsDomain B] : Nontrivial (A ⊗[R] B) :=
by
haveI := ha.isDomain _
let FR := FractionRing R
let FA := FractionRing A
let FB := FractionRing B
let fa : FR →ₐ[R] FA := IsFractionRing.liftAlgHom (g := Algebra.ofId R FA) ((IsFractionRing.injective A FA).comp ha)
let fb : FR →ₐ[R] FB := IsFractionRing.liftAlgHom (g := Algebra.ofId R FB) ((IsFractionRing.injective B FB).comp hb)
algebraize_only [fa.toRingHom, fb.toRingHom]
exact
Algebra.TensorProduct.mapOfCompatibleSMul FR R FA FB |>.comp
(Algebra.TensorProduct.map (IsScalarTower.toAlgHom R A FA)
(IsScalarTower.toAlgHom R B FB)) |>.toRingHom.domain_nontrivial
