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 unramifed 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] [IsNoetherianRing S] [Algebra.IsUnramifiedAt R p] (hp : p ≠ ⊥) [IsDomain S] [Algebra.EssFiniteType R S] : ramificationIdx (algebraMap R S) (under R p) p = 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] [NoZeroSMulDivisors 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.

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] [IsDedekindDomain S] [EssFiniteType R S] [IsDomain R] [Module.Finite ℤ R] [CharZero R] [Algebra.IsIntegral R S] (hp : p ≠ ⊥) : IsUnramifiedAt R p ↔ Ideal.ramificationIdx (algebraMap R S) (Ideal.under R p) p = 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 unramifed iff e(p) = 1.