Separable residue field extensions

For a prime p of A, we introduce a predicate stating that the residue field extensions κ(q)/κ(p) are separable for every prime q of B lying over p. It holds automatically when κ(p) is finite, and so at any nonzero prime of a ring with finite quotients.

Main definitions

• Algebra.HasSeparableResidueFieldsAt A B p: the residue field extension κ(q)/κ(p) is separable for every prime q of B lying over p.

Main results

• an instance deducing Algebra.HasSeparableResidueFieldsAt when the residue field κ(p) is perfect;
• Algebra.HasSeparableResidueFieldsAt.isSeparable_quotient: at a maximal prime, the predicate also gives the separability of the extensions of quotient rings;
• Algebra.HasSeparableResidueFieldsAt.tower_top and Algebra.HasSeparableResidueFieldsAt.tower_bot: the predicate passes to an intermediate ring.

Implementation notes

The condition is on the residue fields rather than on the quotient rings (B ⧸ q)/(A ⧸ p) so that it makes sense at any prime: the quotients are fields only at maximal primes.

The algebra structure on κ(q) over κ(p) in the predicate is the one induced by the algebra structure on Localization.AtPrime q over Localization.AtPrime p given by Localization.AtPrime.algebraOfLiesOver. Any other structure making Localization.AtPrime q an algebra over Localization.AtPrime p in a compatible way with the action of A is equal to that one, see Localization.AtPrime.algebraMap_eq.

class Algebra.HasSeparableResidueFieldsAt (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) [p.IsPrime] : Prop

Algebra.HasSeparableResidueFieldsAt A B p states that for every prime q of B lying over p, the residue field extension κ(q)/κ(p) is separable.

• isSeparable' (q : Ideal B) [q.IsPrime] [q.LiesOver p] : Algebra.IsSeparable p.ResidueField q.ResidueField

instance Algebra.HasSeparableResidueFieldsAt.isSeparable {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p] [HasSeparableResidueFieldsAt A B p] [alg : Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime q)] : Algebra.IsSeparable p.ResidueField q.ResidueField

Algebra.HasSeparableResidueFieldsAt gives the separability for any compatible choice of the algebra structure on the localizations.

instance Algebra.instHasSeparableResidueFieldsAtOfIsIntegralOfPerfectFieldResidueField (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) [p.IsPrime] [Algebra.IsIntegral A B] [PerfectField p.ResidueField] : HasSeparableResidueFieldsAt A B p

If the residue field κ(p) is perfect, the residue field extensions above p are separable.

instance Algebra.HasSeparableResidueFieldsAt.isSeparable_quotient {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) [p.IsMaximal] [HasSeparableResidueFieldsAt A B p] (q : Ideal B) [q.IsMaximal] [q.LiesOver p] : Algebra.IsSeparable (A ⧸ p) (B ⧸ q)

At a maximal prime p, Algebra.HasSeparableResidueFieldsAt also gives the separability of the extension of quotient rings (B ⧸ q)/(A ⧸ p) for every maximal ideal q of B lying over p. Maximality is needed for the quotient rings to be fields; they are then canonically isomorphic to the residue fields.

theorem Algebra.HasSeparableResidueFieldsAt.tower_bot {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (p : Ideal A) [p.IsPrime] [Algebra.IsIntegral B C] [FaithfulSMul B C] [HasSeparableResidueFieldsAt A C p] : HasSeparableResidueFieldsAt A B p

For a tower of rings C/B/A, separability of the residue field extensions of C/A above p gives separability of those of B/A above p.

theorem Algebra.HasSeparableResidueFieldsAt.tower_top {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p] [HasSeparableResidueFieldsAt A C p] : HasSeparableResidueFieldsAt B C q

For a tower of rings C/B/A and a prime q of B lying over p, separability of the residue field extensions of C/A above p gives separability of those of C/B above q.