Unramified and ramification index

We connect Ideal.ramificationIdx to the commutative algebra notion predicate of IsUnramifiedAt.

Main result

• Algebra.isUnramifiedAt_iff_of_isDedekindDomain: Let R be a domain of characteristic 0, finite rank over ℤ, S ⊇ R be a Dedekind domain that is a finite R-algebra. Let p be a prime of S, then p is unramified iff e(p) = 1.

theorem Ideal.ramificationIdx_eq_one_of_isUnramifiedAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {p : Ideal S} [p.IsPrime] [Algebra.IsUnramifiedAt R p] [Algebra.EssFiniteType R S] : p.ramificationIdx R = 1

theorem IsUnramifiedAt.of_liesOver_of_ne_bot (R : Type u_1) {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (p : Ideal S) (P : Ideal T) [P.LiesOver p] [p.IsPrime] [P.IsPrime] [Algebra.IsUnramifiedAt R P] [Algebra.EssFiniteType R S] [Algebra.EssFiniteType R T] [IsDedekindDomain S] (hP₁ : P.primeCompl ≤ nonZeroDivisors T) (hP₂ : p ≠ ⊥ → P ≠ ⊥) : Algebra.IsUnramifiedAt R p

theorem Algebra.IsUnramifiedAt.of_liesOver (R : Type u_1) {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (p : Ideal S) (P : Ideal T) [P.LiesOver p] [p.IsPrime] [P.IsPrime] [IsUnramifiedAt R P] [EssFiniteType R S] [EssFiniteType R T] [IsDedekindDomain S] [IsDomain T] [Module.IsTorsionFree S T] : IsUnramifiedAt R p

Up to technical conditions, If T/S/R is a tower of algebras, P is a prime of T unramified in R, then P ∩ S (as a prime of S) is also unramified in R.

@[deprecated "Use `Ideal.ramificationIdx'_eq_one_iff` instead." (since := "2026-06-30")]

theorem Algebra.isUnramifiedAt_iff_of_isDedekindDomain {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {p : Ideal S} [p.IsPrime] [EssFiniteType R S] [IsDomain R] [Module.Finite ℤ R] [CharZero R] [Algebra.IsIntegral R S] : IsUnramifiedAt R p ↔ p.ramificationIdx R = 1

Let R be a domain of characteristic 0, finite rank over ℤ, S be a Dedekind domain that is a finite R-algebra. Let p be a prime of S, then p is unramified iff e(p) = 1.

theorem Algebra.isUnramifiedAt_bot {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [Module.IsTorsionFree R S] [CharZero R] [Algebra.IsIntegral R S] : IsUnramifiedAt R ⊥

In characteristic zero the generic point is unramified: if S is a domain that is integral over a characteristic-zero domain R and R → S is injective, then S is unramified at the zero ideal.

theorem Algebra.isUnramifiedIn_bot {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [FaithfulSMul R S] [CharZero R] [Algebra.IsIntegral R S] : IsUnramifiedIn S ⊥

In characteristic zero, the zero ideal is unramified in an integral domain extension.

theorem Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDedekindDomain S] [Module.IsTorsionFree R S] {p : Ideal R} (hp : p ≠ ⊥) : IsUnramifiedIn S p ↔ ∀ (P : Ideal S) (x : P.IsMaximal), P.LiesOver p → IsUnramifiedAt R P

Let S be a Dedekind domain that is torsion-free over a domain R, and let p ≠ ⊥ be an ideal of R. Then p is unramified in S if and only if S is unramified at every maximal ideal P of S lying over p.

See Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain if R is of characteristic zero.

theorem Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDedekindDomain S] [Module.IsTorsionFree R S] [CharZero R] [Algebra.IsIntegral R S] {p : Ideal R} : IsUnramifiedIn S p ↔ ∀ (P : Ideal S) (x : P.IsMaximal), P.LiesOver p → IsUnramifiedAt R P

Let S be a Dedekind domain that is integral and torsion-free over a characteristic-zero domain R. Then an ideal p of R is unramified in S if and only if S is unramified at every maximal ideal P of S lying over p.

theorem Algebra.IsUnramifiedIn.ramificationIdx_eq_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [Module.Finite ℤ R] [CharZero R] [EssFiniteType R S] [Algebra.IsIntegral R S] {𝔭 : Ideal R} (hunr : IsUnramifiedIn S 𝔭) {𝔓 : Ideal S} [𝔓.IsPrime] (hP : 𝔓.LiesOver 𝔭) : 𝔓.ramificationIdx R = 1

For a prime 𝔓 of S lying over an unramified prime 𝔭 of R, the ramification index e(𝔓 ∣ 𝔭) equals 1.

theorem Algebra.isUnramifiedIn_iff_forall_ramificationIdx_eq_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [Module.Finite ℤ R] [CharZero R] [EssFiniteType R S] [Algebra.IsIntegral R S] {𝔭 : Ideal R} : IsUnramifiedIn S 𝔭 ↔ ∀ (𝔓 : Ideal S) [𝔓.IsPrime], 𝔓.LiesOver 𝔭 → 𝔓.ramificationIdx R = 1

A nonzero ideal of R is unramified in S if and only if every prime ideal of S lying over it has ramification index 1.