Ramification index and inertia degree

Given P : Ideal S lying over p : Ideal R for the ring extension f : R →+* S (assuming P and p are prime or maximal where needed), the ramification index Ideal.ramificationIdx f p P is the multiplicity of P in map f p, and the inertia degree Ideal.inertiaDeg f p P is the degree of the field extension (S / P) : (R / p).

Main results

The main theorem Ideal.sum_ramification_inertia states that for all coprime P lying over p, Σ P, ramification_idx f p P * inertia_deg f p P equals the degree of the field extension Frac(S) : Frac(R).

Implementation notes

Often the above theory is set up in the case where:

• R is the ring of integers of a number field K,
• L is a finite separable extension of K,
• S is the integral closure of R in L,
• p and P are maximal ideals,
• P is an ideal lying over p We will try to relax the above hypotheses as much as possible.

Notation

In this file, e stands for the ramification index and f for the inertia degree of P over p, leaving p and P implicit.

noncomputable def Ideal.ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) (p : Ideal R) (P : Ideal S) : ℕ

The ramification index of P over p is the largest exponent n such that p is contained in P^n.

In particular, if p is not contained in P^n, then the ramification index is 0.

If there is no largest such n (e.g. because p = ⊥), then ramificationIdx is defined to be 0.

Equations

• Ideal.ramificationIdx f p P = sSup {n : ℕ | Ideal.map f p ≤ P ^ n}

theorem Ideal.ramificationIdx_eq_find {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} [DecidablePred fun (n : ℕ) => ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n] (h : ∃ (n : ℕ), ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n) : ramificationIdx f p P = Nat.find h

theorem Ideal.ramificationIdx_eq_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} (h : ∀ (n : ℕ), ∃ (k : ℕ), map f p ≤ P ^ k ∧ n < k) : ramificationIdx f p P = 0

theorem Ideal.ramificationIdx_spec {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} {n : ℕ} (hle : map f p ≤ P ^ n) (hgt : ¬map f p ≤ P ^ (n + 1)) : ramificationIdx f p P = n

theorem Ideal.ramificationIdx_lt {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} {n : ℕ} (hgt : ¬map f p ≤ P ^ n) : ramificationIdx f p P < n

@[simp]

theorem Ideal.ramificationIdx_bot {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {P : Ideal S} : ramificationIdx f ⊥ P = 0

@[simp]

theorem Ideal.ramificationIdx_of_not_le {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} (h : ¬map f p ≤ P) : ramificationIdx f p P = 0

theorem Ideal.ramificationIdx_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} {e : ℕ} (he : e ≠ 0) (hle : map f p ≤ P ^ e) (hnle : ¬map f p ≤ P ^ (e + 1)) : ramificationIdx f p P ≠ 0

theorem Ideal.le_pow_of_le_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} {n : ℕ} (hn : n ≤ ramificationIdx f p P) : map f p ≤ P ^ n

theorem Ideal.le_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} : map f p ≤ P ^ ramificationIdx f p P

theorem Ideal.le_comap_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} : p ≤ comap f (P ^ ramificationIdx f p P)

theorem Ideal.le_comap_of_ramificationIdx_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} (h : ramificationIdx f p P ≠ 0) : p ≤ comap f P

theorem Ideal.ramificationIdx_comap_eq {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) {S₁ : Type u_1} [CommRing S₁] [Algebra R S₁] [Algebra R S] (e : S ≃ₐ[R] S₁) (P : Ideal S₁) : ramificationIdx (algebraMap R S) p (comap e P) = ramificationIdx (algebraMap R S₁) p P

theorem Ideal.ramificationIdx_map_eq {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) {S₁ : Type u_1} [CommRing S₁] [Algebra R S₁] [Algebra R S] {E : Type u_2} [EquivLike E S S₁] [AlgEquivClass E R S S₁] (P : Ideal S) (e : E) : ramificationIdx (algebraMap R S₁) p (map e P) = ramificationIdx (algebraMap R S) p P

theorem Ideal.ramificationIdx_ne_one_iff {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} (hp : map f p ≤ P) : ramificationIdx f p P ≠ 1 ↔ map f p ≤ P ^ 2

theorem Ideal.ramificationIdx_eq_one_of_map_localization {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} [P.IsPrime] [IsNoetherianRing S] (hpP : map (algebraMap R S) p ≤ P) (hp : P ≠ ⊥) (hp' : P.primeCompl ≤ nonZeroDivisors S) (H : map (algebraMap R (Localization.AtPrime P)) p = IsLocalRing.maximalIdeal (Localization.AtPrime P)) : ramificationIdx (algebraMap R S) p P = 1

The converse is true when S is a Dedekind domain. See Ideal.ramificationIdx_eq_one_iff_of_isDedekindDomain.

theorem Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] [DecidableEq (Ideal S)] (hp0 : map f p ≠ ⊥) (hP : P.IsPrime) (hP0 : P ≠ ⊥) : ramificationIdx f p P = Multiset.count P (UniqueFactorizationMonoid.normalizedFactors (map f p))

theorem Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] (hp : map f p ≠ ⊥) (hP : P.IsPrime) : ramificationIdx f p P = multiplicity P (map f p)

theorem Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] [DecidableEq (Ideal S)] (hp0 : map f p ≠ ⊥) (hP : P.IsPrime) (hP0 : P ≠ ⊥) : ramificationIdx f p P = Multiset.count P (UniqueFactorizationMonoid.factors (map f p))

theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] (hp0 : map f p ≠ ⊥) (hP : P.IsPrime) (le : map f p ≤ P) : ramificationIdx f p P ≠ 0

theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver {R : Type u} [CommRing R] {S : Type v} [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (P : Ideal S) [hP : P.IsPrime] {p : Ideal R} (hp : p ≠ ⊥) [hPp : P.LiesOver p] : ramificationIdx (algebraMap R S) p P ≠ 0

theorem Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff {R : Type u} [CommRing R] {S : Type v} [CommRing S] [IsDedekindDomain S] [Algebra R S] {p : Ideal R} {P : Ideal S} [P.IsPrime] (hp : P ≠ ⊥) (hpP : map (algebraMap R S) p ≤ P) : ramificationIdx (algebraMap R S) p P = 1 ↔ map (algebraMap R (Localization.AtPrime P)) p = IsLocalRing.maximalIdeal (Localization.AtPrime P)

noncomputable def Ideal.inertiaDeg {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] : ℕ

The inertia degree of P : Ideal S lying over p : Ideal R is the degree of the extension (S / P) : (R / p).

We do not assume P lies over p in the definition; we return 0 instead.

See inertiaDeg_algebraMap for the common case where f = algebraMap R S and there is an algebra structure R / p → S / P.

Equations

• p.inertiaDeg P = if hPp : Ideal.comap (algebraMap R S) P = p then Module.finrank (R ⧸ p) (S ⧸ P) else 0

@[simp]

theorem Ideal.inertiaDeg_of_subsingleton {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [hp : p.IsMaximal] [hQ : Subsingleton (S ⧸ P)] : p.inertiaDeg P = 0

@[simp]

theorem Ideal.inertiaDeg_algebraMap {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [P.LiesOver p] [p.IsMaximal] : p.inertiaDeg P = Module.finrank (R ⧸ p) (S ⧸ P)

theorem Ideal.inertiaDeg_pos {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [p.IsMaximal] [Module.Finite R S] [P.LiesOver p] : 0 < p.inertiaDeg P

theorem Ideal.inertiaDeg_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [p.IsMaximal] [Module.Finite R S] [P.LiesOver p] : p.inertiaDeg P ≠ 0

theorem Ideal.inertiaDeg_comap_eq {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) {S₁ : Type u_1} [CommRing S₁] [Algebra R S₁] [Algebra R S] (e : S ≃ₐ[R] S₁) (P : Ideal S₁) [p.IsMaximal] : p.inertiaDeg (comap e P) = p.inertiaDeg P

theorem Ideal.inertiaDeg_map_eq {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) {S₁ : Type u_1} [CommRing S₁] [Algebra R S₁] [Algebra R S] [p.IsMaximal] (P : Ideal S) {E : Type u_2} [EquivLike E S S₁] [AlgEquivClass E R S S₁] (e : E) : p.inertiaDeg (map e P) = p.inertiaDeg P

theorem Ideal.absNorm_eq_pow_inertiaDeg {R : Type u} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {p : ℤ} (P : Ideal R) [P.LiesOver (span {p})] (hp : Prime p) : absNorm P = p.natAbs ^ (span {p}).inertiaDeg P

The absolute norm of an ideal P above a rational prime p is |p| ^ ((span {p}).inertiaDeg P). See absNorm_eq_pow_inertiaDeg' for a version with p of type ℕ.

theorem Ideal.absNorm_eq_pow_inertiaDeg' {R : Type u} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {p : ℕ} (P : Ideal R) [P.LiesOver (span {↑p})] (hp : Nat.Prime p) : absNorm P = p ^ (span {↑p}).inertiaDeg P

The absolute norm of an ideal P above a rational (positive) prime p is p ^ ((span {p}).inertiaDeg P). See absNorm_eq_pow_inertiaDeg for a version with p of type ℤ.

theorem Ideal.FinrankQuotientMap.span_eq_top {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [Algebra R S] {K : Type u_1} [Field K] [Algebra R K] {L : Type u_2} [Field L] [Algebra S L] [IsFractionRing S L] [IsDomain R] [IsDomain S] [Algebra K L] [Module.Finite R S] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Algebra.IsAlgebraic R S] [NoZeroSMulDivisors R K] (hp : p ≠ ⊤) (b : Set S) (hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤) : Submodule.span K (⇑(algebraMap S L) '' b) = ⊤

If b mod p spans S/p as R/p-space, then b itself spans Frac(S) as K-space.

Here,

• p is an ideal of R such that R / p is nontrivial
• K is a field that has an embedding of R (in particular we can take K = Frac(R))
• L is a field extension of K
• S is the integral closure of R in L

More precisely, we avoid quotients in this statement and instead require that b ∪ pS spans S.

theorem Ideal.FinrankQuotientMap.linearIndependent_of_nontrivial {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (K : Type u_1) [Field K] [Algebra R K] {V : Type u_3} {V' : Type u_4} {V'' : Type u_5} [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] [AddCommGroup V'] [Module R V'] [Module S V'] [IsScalarTower R S V'] [AddCommGroup V''] [Module R V''] [hRK : IsFractionRing R K] [IsDedekindDomain R] (hRS : RingHom.ker (algebraMap R S) ≠ ⊤) (f : V'' →ₗ[R] V) (hf : Function.Injective ⇑f) (f' : V'' →ₗ[R] V') {ι : Type u_6} {b : ι → V''} (hb' : LinearIndependent S (⇑f' ∘ b)) : LinearIndependent K (⇑f ∘ b)

Let V be a vector space over K = Frac(R), S / R a ring extension and V' a module over S. If b, in the intersection V'' of V and V', is linear independent over S in V', then it is linear independent over R in V.

The statement we prove is actually slightly more general:

• it suffices that the inclusion algebraMap R S : R → S is nontrivial
• the function f' : V'' → V' doesn't need to be injective

theorem Ideal.finrank_quotient_map {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [Algebra R S] (K : Type u_1) [Field K] [Algebra R K] (L : Type u_2) [Field L] [Algebra S L] [IsFractionRing S L] [hRK : IsFractionRing R K] [IsDomain S] [IsDedekindDomain R] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] [hp : p.IsMaximal] [Module.Finite R S] : Module.finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) = Module.finrank K L

If p is a maximal ideal of R, and S is the integral closure of R in L, then the dimension [S/pS : R/p] is equal to [Frac(S) : Frac(R)].

noncomputable instance Ideal.Quotient.algebraQuotientPowRamificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] : Algebra (R ⧸ p) (S ⧸ P ^ ramificationIdx (algebraMap R S) p P)

R / p has a canonical map to S / (P ^ e), where e is the ramification index of P over p.

Equations

• Ideal.Quotient.algebraQuotientPowRamificationIdx p P = Ideal.Quotient.algebraQuotientOfLEComap ⋯

@[simp]

theorem Ideal.Quotient.algebraMap_quotient_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] (x : R) : (algebraMap (R ⧸ p) (S ⧸ P ^ ramificationIdx (algebraMap R S) p P)) ((mk p) x) = (mk (P ^ ramificationIdx (algebraMap R S) p P)) ((algebraMap R S) x)

def Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [hfp : NeZero (ramificationIdx (algebraMap R S) p P)] : Algebra (R ⧸ p) (S ⧸ P)

If P lies over p, then R / p has a canonical map to S / P.

This can't be an instance since the map f : R → S is generally not inferable.

Equations

• Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero p P = Ideal.Quotient.algebraQuotientOfLEComap ⋯

@[simp]

theorem Ideal.Quotient.algebraMap_quotient_of_ramificationIdx_neZero {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [NeZero (ramificationIdx (algebraMap R S) p P)] (x : R) : (algebraMap (R ⧸ p) (S ⧸ P)) ((mk p) x) = (mk P) ((algebraMap R S) x)

noncomputable def Ideal.powQuotSuccInclusion {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] (i : ℕ) : ↥(map (Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (P ^ (i + 1))) →ₗ[R ⧸ p] ↥(map (Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (P ^ i))

The inclusion (P^(i + 1) / P^e) ⊂ (P^i / P^e).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ideal.powQuotSuccInclusion_apply_coe {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] (i : ℕ) (x : ↥(map (Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (P ^ (i + 1)))) : ↑((p.powQuotSuccInclusion P i) x) = ↑x

theorem Ideal.powQuotSuccInclusion_injective {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] (i : ℕ) : Function.Injective ⇑(p.powQuotSuccInclusion P i)

noncomputable def Ideal.quotientToQuotientRangePowQuotSuccAux {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) : S ⧸ P → ↥(map (Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)

S ⧸ P embeds into the quotient by P^(i+1) ⧸ P^e as a subspace of P^i ⧸ P^e. See quotientToQuotientRangePowQuotSucc for this as a linear map, and quotientRangePowQuotSuccInclusionEquiv for this as a linear equivalence.

Equations

• p.quotientToQuotientRangePowQuotSuccAux P a_mem = Quotient.map' (fun (x : S) => ⟨(Ideal.Quotient.mk (P ^ Ideal.ramificationIdx (algebraMap R S) p P)) (a * x), ⋯⟩) ⋯

theorem Ideal.quotientToQuotientRangePowQuotSuccAux_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) : p.quotientToQuotientRangePowQuotSuccAux P a_mem (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (a * x), ⋯⟩

noncomputable def Ideal.quotientToQuotientRangePowQuotSucc {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [hfp : NeZero (ramificationIdx (algebraMap R S) p P)] {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) : S ⧸ P →ₗ[R ⧸ p] ↥(map (Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)

S ⧸ P embeds into the quotient by P^(i+1) ⧸ P^e as a subspace of P^i ⧸ P^e.

Equations

• p.quotientToQuotientRangePowQuotSucc P a_mem = { toFun := p.quotientToQuotientRangePowQuotSuccAux P a_mem, map_add' := ⋯, map_smul' := ⋯ }

theorem Ideal.quotientToQuotientRangePowQuotSucc_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [hfp : NeZero (ramificationIdx (algebraMap R S) p P)] {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) : (p.quotientToQuotientRangePowQuotSucc P a_mem) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (a * x), ⋯⟩

theorem Ideal.quotientToQuotientRangePowQuotSucc_injective {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [hfp : NeZero (ramificationIdx (algebraMap R S) p P)] [IsDedekindDomain S] [P.IsPrime] {i : ℕ} (hi : i < ramificationIdx (algebraMap R S) p P) {a : S} (a_mem : a ∈ P ^ i) (a_notMem : a ∉ P ^ (i + 1)) : Function.Injective ⇑(p.quotientToQuotientRangePowQuotSucc P a_mem)

theorem Ideal.quotientToQuotientRangePowQuotSucc_surjective {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [hfp : NeZero (ramificationIdx (algebraMap R S) p P)] [IsDedekindDomain S] (hP0 : P ≠ ⊥) [hP : P.IsPrime] {i : ℕ} (hi : i < ramificationIdx (algebraMap R S) p P) {a : S} (a_mem : a ∈ P ^ i) (a_notMem : a ∉ P ^ (i + 1)) : Function.Surjective ⇑(p.quotientToQuotientRangePowQuotSucc P a_mem)

noncomputable def Ideal.quotientRangePowQuotSuccInclusionEquiv {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [hfp : NeZero (ramificationIdx (algebraMap R S) p P)] [IsDedekindDomain S] [P.IsPrime] (hP : P ≠ ⊥) {i : ℕ} (hi : i < ramificationIdx (algebraMap R S) p P) : (↥(map (Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)) ≃ₗ[R ⧸ p] S ⧸ P

Quotienting P^i / P^e by its subspace P^(i+1) ⧸ P^e is R ⧸ p-linearly isomorphic to S ⧸ P.

Equations

• One or more equations did not get rendered due to their size.

theorem Ideal.rank_pow_quot_aux {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [hfp : NeZero (ramificationIdx (algebraMap R S) p P)] [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥) {i : ℕ} (hi : i < ramificationIdx (algebraMap R S) p P) : Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (P ^ i)) = Module.rank (R ⧸ p) (S ⧸ P) + Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (P ^ (i + 1)))

Since the inclusion (P^(i + 1) / P^e) ⊂ (P^i / P^e) has a kernel isomorphic to P / S, [P^i / P^e : R / p] = [P^(i+1) / P^e : R / p] + [P / S : R / p]

theorem Ideal.rank_pow_quot {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [hfp : NeZero (ramificationIdx (algebraMap R S) p P)] [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥) (i : ℕ) (hi : i ≤ ramificationIdx (algebraMap R S) p P) : Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ ramificationIdx (algebraMap R S) p P)) (P ^ i)) = (ramificationIdx (algebraMap R S) p P - i) • Module.rank (R ⧸ p) (S ⧸ P)

theorem Ideal.rank_prime_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥) (he : ramificationIdx (algebraMap R S) p P ≠ 0) : Module.rank (R ⧸ p) (S ⧸ P ^ ramificationIdx (algebraMap R S) p P) = ramificationIdx (algebraMap R S) p P • Module.rank (R ⧸ p) (S ⧸ P)

If p is a maximal ideal of R, S extends R and P^e lies over p, then the dimension [S/(P^e) : R/p] is equal to e * [S/P : R/p].

theorem Ideal.finrank_prime_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) (P : Ideal S) [Algebra R S] [IsDedekindDomain S] (hP0 : P ≠ ⊥) [p.IsMaximal] [P.IsPrime] (he : ramificationIdx (algebraMap R S) p P ≠ 0) : Module.finrank (R ⧸ p) (S ⧸ P ^ ramificationIdx (algebraMap R S) p P) = ramificationIdx (algebraMap R S) p P * Module.finrank (R ⧸ p) (S ⧸ P)

If p is a maximal ideal of R, S extends R and P^e lies over p, then the dimension [S/(P^e) : R/p], as a natural number, is equal to e * [S/P : R/p].

Properties of the factors of p.map (algebraMap R S)

theorem Ideal.Factors.ne_bot {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [IsDedekindDomain S] [Algebra R S] (P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) : ↑P ≠ ⊥

instance Ideal.Factors.isPrime {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [IsDedekindDomain S] [Algebra R S] (P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) : (↑P).IsPrime

theorem Ideal.Factors.ramificationIdx_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [IsDedekindDomain S] [Algebra R S] (P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) : ramificationIdx (algebraMap R S) p ↑P ≠ 0

instance Ideal.Factors.fact_ramificationIdx_neZero {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [IsDedekindDomain S] [Algebra R S] (P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) : NeZero (ramificationIdx (algebraMap R S) p ↑P)

instance Ideal.Factors.isScalarTower {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [IsDedekindDomain S] [Algebra R S] (P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) : IsScalarTower R (R ⧸ p) (S ⧸ ↑P)

instance Ideal.Factors.liesOver {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [IsDedekindDomain S] [Algebra R S] [p.IsMaximal] (P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) : (↑P).LiesOver p

theorem Ideal.Factors.finrank_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [IsDedekindDomain S] [Algebra R S] [p.IsMaximal] (P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) : Module.finrank (R ⧸ p) (S ⧸ ↑P ^ ramificationIdx (algebraMap R S) p ↑P) = ramificationIdx (algebraMap R S) p ↑P * p.inertiaDeg ↑P

instance Ideal.Factors.finiteDimensional_quotient_pow {R : Type u} [CommRing R] {S : Type v} [CommRing S] (p : Ideal R) [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [p.IsMaximal] (P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) : FiniteDimensional (R ⧸ p) (S ⧸ ↑P ^ ramificationIdx (algebraMap R S) p ↑P)

noncomputable def Ideal.Factors.piQuotientEquiv {R : Type u} [CommRing R] {S : Type v} [CommRing S] [IsDedekindDomain S] [Algebra R S] (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) : S ⧸ map (algebraMap R S) p ≃+* ((P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) → S ⧸ ↑P ^ ramificationIdx (algebraMap R S) p ↑P)

Chinese remainder theorem for a ring of integers: if the prime ideal p : Ideal R factors in S as ∏ i, P i ^ e i, then S ⧸ I factors as Π i, R ⧸ (P i ^ e i).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ideal.Factors.piQuotientEquiv_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] [IsDedekindDomain S] [Algebra R S] (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) (x : S) : (piQuotientEquiv p hp) ((Quotient.mk (map (algebraMap R S) p)) x) = fun (x_1 : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) => (Quotient.mk (↑x_1 ^ ramificationIdx (algebraMap R S) p ↑x_1)) x

@[simp]

theorem Ideal.Factors.piQuotientEquiv_map {R : Type u} [CommRing R] {S : Type v} [CommRing S] [IsDedekindDomain S] [Algebra R S] (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) (x : R) : (piQuotientEquiv p hp) ((algebraMap R (S ⧸ map (algebraMap R S) p)) x) = fun (x_1 : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) => (Quotient.mk (↑x_1 ^ ramificationIdx (algebraMap R S) p ↑x_1)) ((algebraMap R S) x)

noncomputable def Ideal.Factors.piQuotientLinearEquiv {R : Type u} [CommRing R] (S : Type v) [CommRing S] [IsDedekindDomain S] [Algebra R S] (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) : (S ⧸ map (algebraMap R S) p) ≃ₗ[R ⧸ p] (P : ↥(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) → S ⧸ ↑P ^ ramificationIdx (algebraMap R S) p ↑P

Chinese remainder theorem for a ring of integers: if the prime ideal p : Ideal R factors in S as ∏ i, P i ^ e i, then S ⧸ I factors R ⧸ I-linearly as Π i, R ⧸ (P i ^ e i).

Equations

• One or more equations did not get rendered due to their size.

theorem Ideal.sum_ramification_inertia {R : Type u} [CommRing R] (S : Type v) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : ∑ P ∈ primesOverFinset p S, ramificationIdx (algebraMap R S) p P * p.inertiaDeg P = Module.finrank K L

The fundamental identity of ramification index e and inertia degree f: for P ranging over the primes lying over p, ∑ P, e P * f P = [Frac(S) : Frac(R)]; here S is a finite R-module (and thus Frac(S) : Frac(R) is a finite extension) and p is maximal.

theorem Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing {R : Type u} [CommRing R] (S : Type v) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [IsLocalRing S] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : ramificationIdx (algebraMap R S) p (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) = Module.finrank K L

Ideal.sum_ramification_inertia, in the local (DVR) case.

theorem Ideal.ramificationIdx_tower {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [IsDedekindDomain S] [IsDedekindDomain T] {f : R →+* S} {g : S →+* T} {p : Ideal R} {P : Ideal S} {Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime] (hg0 : map g P ≠ ⊥) (hfg : map (g.comp f) p ≠ ⊥) (hg : map g P ≤ Q) : ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

theorem Ideal.ramificationIdx_algebra_tower {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] [IsDedekindDomain S] [IsDedekindDomain T] {p : Ideal R} {P : Ideal S} {Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime] (hg0 : map (algebraMap S T) P ≠ ⊥) (hfg : map (algebraMap R T) p ≠ ⊥) (hg : map (algebraMap S T) P ≤ Q) : ramificationIdx (algebraMap R T) p Q = ramificationIdx (algebraMap R S) p P * ramificationIdx (algebraMap S T) P Q

Let T / S / R be a tower of algebras, p, P, Q be ideals in R, S, T respectively, and P and Q are prime. If P = Q ∩ S, then e (Q | p) = e (P | p) * e (Q | P).

theorem Ideal.inertiaDeg_algebra_tower {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 R) (P : Ideal S) (I : Ideal T) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p] [I.LiesOver P] : p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I

Let T / S / R be a tower of algebras, p, P, I be ideals in R, S, T, respectively, and p and P are maximal. If p = P ∩ S and P = I ∩ S, then f (I | p) = f (P | p) * f (I | P).