The tensor square of a purely inseparable extension

Let L / K be a purely inseparable field extension. For every x : L some p-power of x lies in K, so the element 1 ⊗ x - x ⊗ 1 of L ⊗[K] L is nilpotent. Consequently L ⊗[K] L is reduced only when L = K. This is the obstruction showing that a nontrivial finite purely inseparable extension is not geometrically regular over its base.

Mathlib proves the triviality of L / K from the stronger hypothesis that L is unramified over K (Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable); here the hypothesis is only that the tensor square is reduced, and no finiteness of L / K is assumed.

The same nilpotence controls the zero divisors of R ⊗[K] L for a K-algebra R: every element has a positive power in the subring R. So if R is a domain and R ⊗[K] L is reduced, then R ⊗[K] L is a domain as well. For a tower k → K → L and a k-algebra A, applying this to R = K ⊗[k] A shows that L ⊗[k] A is a domain when K ⊗[k] A is a domain and L ⊗[k] A is reduced.

Main results

• TauCeti.IsPurelyInseparable.isNilpotent_one_tmul_sub_tmul_one: 1 ⊗ x - x ⊗ 1 is nilpotent in L ⊗[K] L.
• TauCeti.IsPurelyInseparable.surjective_algebraMap_of_isReduced_tensorProduct: if L ⊗[K] L is reduced, then algebraMap K L is surjective.
• TauCeti.IsPurelyInseparable.isDomain_tensorProduct: if R is a domain and R ⊗[K] L is reduced, then R ⊗[K] L is a domain.
• TauCeti.IsPurelyInseparable.isDomain_tensorProduct_of_isDomain_tensorProduct: if K ⊗[k] A is a domain and L ⊗[k] A is reduced, then L ⊗[k] A is a domain.

theorem TauCeti.IsPurelyInseparable.isNilpotent_one_tmul_sub_tmul_one (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (x : L) : IsNilpotent (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1)

For a purely inseparable extension L / K and x : L, the element 1 ⊗ x - x ⊗ 1 of L ⊗[K] L is nilpotent.

theorem TauCeti.IsPurelyInseparable.surjective_algebraMap_of_isReduced_tensorProduct (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] [IsReduced (TensorProduct K L L)] : Function.Surjective ⇑(algebraMap K L)

A purely inseparable extension L / K whose tensor square L ⊗[K] L is reduced is trivial: algebraMap K L is surjective.

theorem TauCeti.IsPurelyInseparable.isDomain_tensorProduct (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (R : Type u_3) [CommRing R] [Algebra K R] [IsDomain R] [IsReduced (TensorProduct K R L)] : IsDomain (TensorProduct K R L)

Let L / K be a purely inseparable extension of fields and let R be a K-algebra that is a domain. If R ⊗[K] L is reduced, then it is a domain.

theorem TauCeti.IsPurelyInseparable.isDomain_tensorProduct_of_isDomain_tensorProduct (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] {k : Type u_3} [CommRing k] [Algebra k K] [Algebra k L] [IsScalarTower k K L] (A : Type u_4) [CommRing A] [Algebra k A] [hK : IsDomain (TensorProduct k K A)] [IsReduced (TensorProduct k L A)] : IsDomain (TensorProduct k L A)

Let L / K be a purely inseparable extension of fields over k, and let A be a commutative k-algebra. If K ⊗[k] A is a domain and L ⊗[k] A is reduced, then L ⊗[k] A is a domain.