Auxiliary results on tensor products

theorem Ideal.under_mono {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {I J : Ideal S} (hIJ : I ≤ J) : under R I ≤ under R J

theorem Ideal.under_mem_minimalPrimes (R : Type u_2) {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingDown R S] (p : Ideal S) (hp : p ∈ minimalPrimes S) : under R p ∈ minimalPrimes R

theorem RingHom.Flat.tensorProductMap_left {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [CommRing B] [Algebra R B] [CommRing C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] (f : A →ₐ[S] C) (hf : f.Flat) : (Algebra.TensorProduct.map f (AlgHom.id R B)).Flat

theorem RingHom.Flat.tensorProductMap {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [CommRing B] [Algebra R B] [CommRing C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [CommRing D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) (hf : f.Flat) (hg : g.Flat) : (Algebra.TensorProduct.map f g).Flat

theorem Algebra.TensorProduct.exists_intermediateField_isSeparable_and_mem_range {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] (Ω : Type u_2) [Field Ω] [Algebra k Ω] [Algebra.IsSeparable k Ω] (x : TensorProduct k Ω R) : ∃ (K : IntermediateField k Ω), Algebra.IsSeparable k ↥K ∧ Module.Finite k ↥K ∧ x ∈ Set.range ⇑(map (IsScalarTower.toAlgHom k (↥K) Ω) (AlgHom.id k R))

theorem Algebra.TensorProduct.exists_field_isSeparable_and_mem_range {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] (Ω : Type v) [Field Ω] [Algebra k Ω] [Algebra.IsSeparable k Ω] (x : TensorProduct k Ω R) : ∃ (K : Type v) (x_1 : Field K) (x_2 : Algebra k K) (x_3 : Algebra K Ω) (x_4 : IsScalarTower k K Ω), Algebra.IsSeparable k K ∧ Module.Finite k K ∧ x ∈ Set.range ⇑(map (IsScalarTower.toAlgHom k K Ω) (AlgHom.id k R))

theorem subsingleton_minimalPrimes_of_isSeparable {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] (H : ∀ (K : Type v) [inst : Field K] [inst_1 : Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K], (minimalPrimes (TensorProduct k K R)).Subsingleton) (Ω : Type v) [Field Ω] [Algebra k Ω] [Algebra.IsSeparable k Ω] : (minimalPrimes (TensorProduct k Ω R)).Subsingleton

If K ⊗[k] R has up to one minimal prime for every finite, separable extension K of k, the same holds for Ω ⊗[k] R for every separable extension Ω of k.

theorem eq_zero_or_eq_one_of_isIdempotentElem_of_forall_isSeparable {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] (H : ∀ (K : Type v) [inst : Field K] [inst_1 : Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K] (e : TensorProduct k K R), IsIdempotentElem e → e = 0 ∨ e = 1) (Ω : Type v) [Field Ω] [Algebra k Ω] [Algebra.IsSeparable k Ω] (e : TensorProduct k Ω R) (he : IsIdempotentElem e) : e = 0 ∨ e = 1

If K ⊗[k] R has no non-trivial idempontents for every finite, separable extension K of k, the same holds for Ω ⊗[k] R for every separable extension Ω of k.

theorem Subalgebra.baseChange_mono {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (B : Type u_4) [CommSemiring B] [Algebra R B] {C C' : Subalgebra R A} (h : C ≤ C') : baseChange B C ≤ baseChange B C'

Given subalgebras C and C' of an R-algebra A and another R-algebra B, the base change of C along B is a subalgebra of the base change of C' along B.

theorem isDomain_tensorProduct_of_forall_isDomain_of_FG_right {R : Type u_2} {S : Type u_3} {T : Type u_4} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Module.Flat R S] (h : ∀ (T' : Subalgebra R T), T'.FG → IsDomain (TensorProduct R S ↥T')) : IsDomain (TensorProduct R S T)

If S is flat over R and for every finitely generated subalgebra T' of T, the tensor product S ⊗[R] T' is a domain, then also S ⊗[R] T is a domain.

theorem isDomain_tensorProduct_of_forall_isDomain_of_FG {R : Type u_2} {S : Type u_3} {T : Type u_4} [Field R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (h : ∀ (S' : Subalgebra R S) (T' : Subalgebra R T), S'.FG → T'.FG → IsDomain (TensorProduct R ↥S' ↥T')) : IsDomain (TensorProduct R S T)

If for every finitely generated subalgebra S' of S and finitely generated subalgebra T' of T, the tensor product S' ⊗[R] T' is a domain, then also S ⊗[R] T is a domain.

theorem Polynomial.aeval_one_tmul {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_4} [CommRing T] [Algebra R T] (x : S) (p : Polynomial R) : (aeval (1 ⊗ₜ[R] x)) p = 1 ⊗ₜ[R] (aeval x) p

noncomputable def AdjoinRoot.mapEquivTensorProduct {R : Type u_2} (S : Type u_3) [CommRing R] [CommRing S] [Algebra R S] (p : Polynomial R) : AdjoinRoot (Polynomial.map (algebraMap R S) p) ≃ₐ[S] TensorProduct R S (AdjoinRoot p)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def IsAdjoinRoot.tensorProduct {R : Type u_2} {S : Type u_3} {T : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (p : Polynomial R) [CommRing T] [Algebra R T] (h : IsAdjoinRoot T p) : IsAdjoinRoot (TensorProduct R S T) (Polynomial.map (algebraMap R S) p)

Equations

• One or more equations did not get rendered due to their size.

theorem IsReduced.of_isAdjoinRoot_of_squareFree {R : Type u_2} {S : Type u_3} [CommRing R] [DecompositionMonoid (Polynomial R)] [CommRing S] [Algebra R S] (p : Polynomial R) (h : IsAdjoinRoot S p) (hp : Squarefree p) : IsReduced S

theorem Ideal.isMaximal_comap_iff_of_surjective {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (I : Ideal S) : (comap f I).IsMaximal ↔ I.IsMaximal

theorem IsAdjoinRoot.isArtinianRing_of_field {k : Type u_2} {R : Type u_3} [Field k] [CommRing R] [Algebra k R] (p : Polynomial k) (h : IsAdjoinRoot R p) (hp : p ≠ 0) : IsArtinianRing R

def instAlgebraTensorProduct_geometricallyP (R : Type u_2) (S : Type u_3) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_4) (B : Type u_5) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : Algebra (TensorProduct R A S) (TensorProduct R B S)

Equations

• instAlgebraTensorProduct_geometricallyP R S A B = (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R A B) (AlgHom.id R S)).toAlgebra

theorem instIsScalarTowerTensorProduct_geometricallyP (R : Type u_2) (S : Type u_3) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_4) (B : Type u_5) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : IsScalarTower A (TensorProduct R A S) (TensorProduct R B S)

theorem Algebra.IsPushout.tensorProduct_tensorProduct (R : Type u_2) (S : Type u_3) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_4) (B : Type u_5) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : IsPushout A (TensorProduct R A S) B (TensorProduct R B S)