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.

Let S be an R algebra, p be a prime of R, and suppose q is the unique prime of S lying over R, then

• Localization.localRingHom_injective_of_primesOver_eq_singleton: If R ⊆ S is integral, then R_p → S_q is injective.
• Localization.localRingHom_surjective_of_primesOver_eq_singleton: Suppose S is R-finite and unramified at q. If κ(p) = κ(q) then R_p → S_q is surjective.
• Localization.exists_awayMap_bijective_of_residueField_surjective: Suppose R ⊆ S is finite and unramified at q. If κ(p) = κ(q) then there exists r ∉ p such that R[1/f] = S[1/f].

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

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.

instance Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt (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

instance Algebra.instFiniteResidueFieldOfIsUnramifiedAt (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] : Module.Finite p.ResidueField q.ResidueField

theorem Localization.localRingHom_injective_of_primesOver_eq_singleton {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] (hq : p.primesOver S = {q}) [Algebra.IsIntegral R S] [FaithfulSMul R S] : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)

theorem Localization.finite_of_primesOver_eq_singleton {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] (hq : p.primesOver S = {q}) [Module.Finite R S] [q.LiesOver p] : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)

theorem Localization.localRingHom_surjective_of_primesOver_eq_singleton {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] (hq : p.primesOver S = {q}) [Module.Finite R S] [q.LiesOver p] [Algebra.IsUnramifiedAt R q] (H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)) : Function.Surjective ⇑(localRingHom p q (algebraMap R S) ⋯)

theorem Localization.exists_awayMap_injective_of_localRingHom_injective {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] (hRS : (RingHom.ker (algebraMap R S)).FG) [q.LiesOver p] (H : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)) : ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')

theorem Localization.exists_awayMap_bijective_of_localRingHom_bijective {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] (hq : p.primesOver S = {q}) [Module.Finite R S] [q.LiesOver p] (hRS : (RingHom.ker (algebraMap R S)).FG) (H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)) : ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Bijective ⇑(awayMap (algebraMap R S) r')

theorem Localization.exists_awayMap_bijective_of_residueField_surjective {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] (hq : p.primesOver S = {q}) [Module.Finite R S] [FaithfulSMul R S] [q.LiesOver p] [Algebra.IsUnramifiedAt R q] (H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)) : ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Bijective ⇑(awayMap (algebraMap R S) r')