Tensor products of reduced algebras and domains

TheoremReduced algebras stay reduced under base change over a perfect field#✓fully proved

Tensoring a reduced algebra with a field extension over a perfect field preserves reducedness.

theorem Algebra.isReduced_tensorProduct_of_perfectField
    (k : Type u) [Field k] [PerfectField k] (A : Type v) [CommRing A] [Algebra k A]
    [IsReduced A] (L : Type w) [Field L] [Algebra k L] :
    IsReduced (L ⊗[k] A)

Used by 1

Used byReduced schemes over a perfect field are geometrically reduced

TheoremTensor products of domains over an algebraically closed field#✓fully proved

Over an algebraically closed field, the tensor product of a finite-type domain with a domain is a domain.

theorem isDomain_of_isAlgClosed_of_finiteType (A : Type v) (B : Type w)
    [CommRing A] [Algebra K A] [Algebra.FiniteType K A] [IsDomain A]
    [CommRing B] [Algebra K B] [IsDomain B] :
    IsDomain (A ⊗[K] B)

Used by 1

Used byField-with-domain tensor products over an algebraically closed field

TheoremField-with-domain tensor products over an algebraically closed field#✓fully proved

Over an algebraically closed field, the tensor product of a field with a domain is a domain.

theorem isDomain_of_isAlgClosed_of_field (F : Type v) (B : Type w) [Field F] [Algebra K F]
    [CommRing B] [Algebra K B] [IsDomain B] : IsDomain (F ⊗[K] B)

Uses 1 · Used by 1

Proof usesTensor products of domains over an algebraically closed field

Used byGeometric irreducibility over an algebraically closed field

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.