Unramified algebras over local rings

Main results

• Algebra.FormallyUnramified.iff_map_maximalIdeal_eq: Let R be a local ring, A be a local R-algebra essentially of finite type. Then A/R is unramified if and only if κA/κR is separable, and m_R S = m_S.
• Algebra.isUnramifiedAt_iff_map_eq: Let A be an essentially of finite type R-algebra, q be a prime over p. Then A is unramified at p if and only if κ(q)/κ(p) is separable, and pS_q = qS_q.

instance Algebra.instFormallyUnramifiedResidueField {S : Type u_2} [CommRing S] [IsLocalRing S] : FormallyUnramified S (IsLocalRing.ResidueField S)

instance Algebra.instFormallyUnramifiedResidueField_1 {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [FormallyUnramified R S] : FormallyUnramified (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)

instance Algebra.instFiniteResidueFieldOfFormallyUnramified {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [EssFiniteType R S] [FormallyUnramified R S] : Module.Finite (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)

Stacks Tag 00UW ((2))

instance Algebra.instIsSeparableResidueFieldOfFormallyUnramified {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [EssFiniteType R S] [FormallyUnramified R S] : Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)

Stacks Tag 00UW ((2))

theorem Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [EssFiniteType R S] [FormallyUnramified R S] : IsField (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))

theorem Algebra.FormallyUnramified.map_maximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [EssFiniteType R S] [FormallyUnramified R S] : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S

Stacks Tag 00UW ((1))

theorem Algebra.FormallyUnramified.of_map_maximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [EssFiniteType R S] [Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)] (H : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S) : FormallyUnramified R S

Stacks Tag 02FM

theorem Algebra.FormallyUnramified.iff_map_maximalIdeal_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [EssFiniteType R S] : FormallyUnramified R S ↔ Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) ∧ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S

noncomputable instance Algebra.instResidueFieldOfLiesOver (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] : Algebra p.ResidueField q.ResidueField

theorem Algebra.isUnramifiedAt_iff_map_eq (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] : IsUnramifiedAt R q ↔ Algebra.IsSeparable p.ResidueField q.ResidueField ∧ Ideal.map (algebraMap R (Localization.AtPrime q)) p = IsLocalRing.maximalIdeal (Localization.AtPrime q)

Let A be an essentially of finite type R-algebra, q be a prime over p. Then A is unramified at p if and only if κ(q)/κ(p) is separable, and pS_q = qS_q.