Nyll.SchemeTheory.Etale.ResidueBaseChange

Module documentation

Purely inseparable residue extensions under base change

For an actual prime of a tensor product, pure inseparability at its image in the original algebra implies pure inseparability over the new base. The proof uses the uniqueness of field embeddings and the two generators of the tensor product. No universal injectivity away from the selected point is required.

theorem

isPurelyInseparable_residueFieldMap_tensorProduct

L36 ↗

Algebra.isPurelyInseparable_residueFieldMap_tensorProduct

Documentation

Pure inseparability at a selected prime is preserved by arbitrary base change, expressed through the canonical maps of the actual residue fields.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public noncomputable section
open scoped TensorProduct
universe u v w
namespace Algebra

Lean source · statement

theorem isPurelyInseparable_residueFieldMap_tensorProduct
    {R : Type u} {S : Type v} {T : Type w}
    [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T]
    (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    (P : Ideal T) [P.IsPrime] [P.LiesOver p]
    (Q : Ideal (T ⊗[R] S)) [Q.IsPrime] [Q.LiesOver P]
    (hq : q = Q.comap (TensorProduct.includeRight : S →ₐ[R] T ⊗[R] S).toRingHom)
    (hpure : (Ideal.ResidueField.map p q (algebraMap R S) (q.over_def p)).IsPurelyInseparable) :
    (Ideal.ResidueField.map P Q (algebraMap T (T ⊗[R] S))
      (Q.over_def P)).IsPurelyInseparable

Module documentation

Purely inseparable residue extensions under base change

Declarations

isPurelyInseparable_residueFieldMap_tensorProduct