mathlib3 documentation

number_theory.ramification_inertia

Ramification index and inertia degree #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.ramification_idx f p P is the multiplicity of P in map f p, and the inertia degree ideal.inertia_deg 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:

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.

source
noncomputable def ideal.ramification_idx {R : Type u} [comm_ring R] {S : Type v} [comm_ring 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 ramification_idx is defined to be 0.

Equations
Instances for ideal.ramification_idx
source
theorem ideal.ramification_idx_eq_find {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} (h : ∃ (n : ℕ), ∀ (k : ℕ), ideal.map f p ≤ P ^ k → k ≤ n) :
ideal.ramification_idx f p P = nat.find h
source
theorem ideal.ramification_idx_eq_zero {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} (h : ∀ (n : ℕ), ∃ (k : ℕ), ideal.map f p ≤ P ^ k ∧ n < k) :
ideal.ramification_idx f p P = 0
source
theorem ideal.ramification_idx_spec {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} {n : ℕ} (hle : ideal.map f p ≤ P ^ n) (hgt : ¬ideal.map f p ≤ P ^ (n + 1)) :
ideal.ramification_idx f p P = n
source
theorem ideal.ramification_idx_lt {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} {n : ℕ} (hgt : ¬ideal.map f p ≤ P ^ n) :
ideal.ramification_idx f p P < n
source
@[simp]
theorem ideal.ramification_idx_bot {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {P : ideal S} :
ideal.ramification_idx f ⊥ P = 0
source
@[simp]
theorem ideal.ramification_idx_of_not_le {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} (h : ¬ideal.map f p ≤ P) :
ideal.ramification_idx f p P = 0
source
theorem ideal.ramification_idx_ne_zero {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} {e : ℕ} (he : e ≠ 0) (hle : ideal.map f p ≤ P ^ e) (hnle : ¬ideal.map f p ≤ P ^ (e + 1)) :
ideal.ramification_idx f p P ≠ 0
source
theorem ideal.le_pow_of_le_ramification_idx {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} {n : ℕ} (hn : n ≤ ideal.ramification_idx f p P) :
ideal.map f p ≤ P ^ n
source
theorem ideal.le_pow_ramification_idx {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} :
ideal.map f p ≤ P ^ ideal.ramification_idx f p P
source
theorem ideal.le_comap_pow_ramification_idx {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} :
p ≤ ideal.comap f (P ^ ideal.ramification_idx f p P)
source
theorem ideal.le_comap_of_ramification_idx_ne_zero {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} (h : ideal.ramification_idx f p P ≠ 0) :
p ≤ ideal.comap f P
source
theorem ideal.is_dedekind_domain.ramification_idx_eq_normalized_factors_count {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} [is_domain S] [is_dedekind_domain S] (hp0 : ideal.map f p ≠ ⊥) (hP : P.is_prime) (hP0 : P ≠ ⊥) :
ideal.ramification_idx f p P = multiset.count P (unique_factorization_monoid.normalized_factors (ideal.map f p))
source
theorem ideal.is_dedekind_domain.ramification_idx_eq_factors_count {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} [is_domain S] [is_dedekind_domain S] (hp0 : ideal.map f p ≠ ⊥) (hP : P.is_prime) (hP0 : P ≠ ⊥) :
ideal.ramification_idx f p P = multiset.count P (unique_factorization_monoid.factors (ideal.map f p))
source
theorem ideal.is_dedekind_domain.ramification_idx_ne_zero {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {f : R →+* S} {p : ideal R} {P : ideal S} [is_domain S] [is_dedekind_domain S] (hp0 : ideal.map f p ≠ ⊥) (hP : P.is_prime) (le : ideal.map f p ≤ P) :
ideal.ramification_idx f p P ≠ 0
source
noncomputable def ideal.inertia_deg {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hp : p.is_maximal] :
ℕ

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 inertia_deg_algebra_map for the common case where f = algebra_map R S and there is an algebra structure R / p → S / P.

Equations
source
@[simp]
theorem ideal.inertia_deg_of_subsingleton {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hp : p.is_maximal] [hQ : subsingleton (S ⧸ P)] :
ideal.inertia_deg f p P = 0
source
@[simp]
theorem ideal.inertia_deg_algebra_map {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) (P : ideal S) [algebra R S] [algebra (R ⧸ p) (S ⧸ P)] [is_scalar_tower R (R ⧸ p) (S ⧸ P)] [hp : p.is_maximal] :
ideal.inertia_deg (algebra_map R S) p P = finite_dimensional.finrank (R ⧸ p) (S ⧸ P)
source
theorem ideal.finrank_quotient_map.linear_independent_of_nontrivial {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] [algebra R S] (K : Type u_1) [field K] [algebra R K] [hRK : is_fraction_ring R K] {V : Type u_3} {V' : Type u_4} {V'' : Type u_5} [add_comm_group V] [module R V] [module K V] [is_scalar_tower R K V] [add_comm_group V'] [module R V'] [module S V'] [is_scalar_tower R S V'] [add_comm_group V''] [module R V''] [is_domain R] [is_dedekind_domain R] (hRS : ring_hom.ker (algebra_map R S) ≠ ⊤) (f : V'' →ₗ[R] V) (hf : function.injective ⇑f) (f' : V'' →ₗ[R] V') {ι : Type u_2} {b : ι → V''} (hb' : linear_independent S (⇑f' ∘ b)) :
linear_independent 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 algebra_map R S : R → S is nontrivial
  • the function f' : V'' → V' doesn't need to be injective
source
theorem ideal.finrank_quotient_map.span_eq_top {R : Type u} [comm_ring R] {S : Type v} [comm_ring 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] [is_fraction_ring S L] [is_domain R] [is_domain S] [algebra K L] [is_noetherian R S] [algebra R L] [is_scalar_tower R S L] [is_scalar_tower R K L] [is_integral_closure S R L] [no_zero_smul_divisors R K] (hp : p ≠ ⊤) (b : set S) (hb' : submodule.span R b ⊔ submodule.restrict_scalars R (ideal.map (algebra_map R S) p) = ⊤) :
submodule.span K (⇑(algebra_map 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.

source
theorem ideal.finrank_quotient_map {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [algebra R S] (K : Type u_1) [field K] [algebra R K] [hRK : is_fraction_ring R K] (L : Type u_2) [field L] [algebra S L] [is_fraction_ring S L] [is_domain R] [is_domain S] [is_dedekind_domain R] [algebra K L] [algebra R L] [is_scalar_tower R K L] [is_scalar_tower R S L] [is_integral_closure S R L] [hp : p.is_maximal] [is_noetherian R S] :
finite_dimensional.finrank (R ⧸ p) (S ⧸ ideal.map (algebra_map R S) p) = finite_dimensional.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)].

source
@[protected, instance]
noncomputable def ideal.quotient.algebra_quotient_pow_ramification_idx {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) :
algebra (R ⧸ p) (S ⧸ P ^ ideal.ramification_idx f p P)

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

Equations
source
@[simp]
theorem ideal.quotient.algebra_map_quotient_pow_ramification_idx {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) (x : R) :
⇑(algebra_map (R ⧸ p) (S ⧸ P ^ ideal.ramification_idx f p P)) (⇑(ideal.quotient.mk p) x) = ⇑(ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (⇑f x)
source
def ideal.quotient.algebra_quotient_of_ramification_idx_ne_zero {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hfp : ne_zero (ideal.ramification_idx f 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 inferrable.

Equations
source
@[simp]
theorem ideal.quotient.algebra_map_quotient_of_ramification_idx_ne_zero {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hfp : ne_zero (ideal.ramification_idx f p P)] (x : R) :
⇑(algebra_map (R ⧸ p) (S ⧸ P)) (⇑(ideal.quotient.mk p) x) = ⇑(ideal.quotient.mk P) (⇑f x)
source
def ideal.pow_quot_succ_inclusion {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) (i : ℕ) :
↥(ideal.map (ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (P ^ (i + 1))) →ₗ[R ⧸ p] ↥(ideal.map (ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (P ^ i))

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

Equations
source
@[simp]
theorem ideal.pow_quot_succ_inclusion_apply_coe {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) (i : ℕ) (x : ↥(ideal.map (ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (P ^ (i + 1)))) :
↑(⇑(ideal.pow_quot_succ_inclusion f p P i) x) = ↑x
source
theorem ideal.pow_quot_succ_inclusion_injective {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) (i : ℕ) :
function.injective ⇑(ideal.pow_quot_succ_inclusion f p P i)
source
noncomputable def ideal.quotient_to_quotient_range_pow_quot_succ_aux {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) :
S ⧸ P → ↥(ideal.map (ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (P ^ i)) ⧸ linear_map.range (ideal.pow_quot_succ_inclusion f p P i)

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

Equations
source
theorem ideal.quotient_to_quotient_range_pow_quot_succ_aux_mk {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) :
ideal.quotient_to_quotient_range_pow_quot_succ_aux f p P a_mem (submodule.quotient.mk x) = submodule.quotient.mk ⟨⇑(ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (x * a), _⟩
source
noncomputable def ideal.quotient_to_quotient_range_pow_quot_succ {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hfp : ne_zero (ideal.ramification_idx f p P)] {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) :
S ⧸ P →ₗ[R ⧸ p] ↥(ideal.map (ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (P ^ i)) ⧸ linear_map.range (ideal.pow_quot_succ_inclusion f p P i)

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

Equations
source
theorem ideal.quotient_to_quotient_range_pow_quot_succ_mk {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hfp : ne_zero (ideal.ramification_idx f p P)] {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) :
⇑(ideal.quotient_to_quotient_range_pow_quot_succ f p P a_mem) (submodule.quotient.mk x) = submodule.quotient.mk ⟨⇑(ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (x * a), _⟩
source
theorem ideal.quotient_to_quotient_range_pow_quot_succ_injective {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hfp : ne_zero (ideal.ramification_idx f p P)] [is_domain S] [is_dedekind_domain S] [P.is_prime] {i : ℕ} (hi : i < ideal.ramification_idx f p P) {a : S} (a_mem : a ∈ P ^ i) (a_not_mem : a ∉ P ^ (i + 1)) :
function.injective ⇑(ideal.quotient_to_quotient_range_pow_quot_succ f p P a_mem)
source
theorem ideal.quotient_to_quotient_range_pow_quot_succ_surjective {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hfp : ne_zero (ideal.ramification_idx f p P)] [is_domain S] [is_dedekind_domain S] (hP0 : P ≠ ⊥) [hP : P.is_prime] {i : ℕ} (hi : i < ideal.ramification_idx f p P) {a : S} (a_mem : a ∈ P ^ i) (a_not_mem : a ∉ P ^ (i + 1)) :
function.surjective ⇑(ideal.quotient_to_quotient_range_pow_quot_succ f p P a_mem)
source
noncomputable def ideal.quotient_range_pow_quot_succ_inclusion_equiv {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hfp : ne_zero (ideal.ramification_idx f p P)] [is_domain S] [is_dedekind_domain S] [P.is_prime] (hP : P ≠ ⊥) {i : ℕ} (hi : i < ideal.ramification_idx f p P) :
(↥(ideal.map (ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (P ^ i)) ⧸ linear_map.range (ideal.pow_quot_succ_inclusion f p 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
source
theorem ideal.rank_pow_quot_aux {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hfp : ne_zero (ideal.ramification_idx f p P)] [is_domain S] [is_dedekind_domain S] [p.is_maximal] [P.is_prime] (hP0 : P ≠ ⊥) {i : ℕ} (hi : i < ideal.ramification_idx f p P) :
module.rank (R ⧸ p) ↥(ideal.map (ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (P ^ i)) = module.rank (R ⧸ p) (S ⧸ P) + module.rank (R ⧸ p) ↥(ideal.map (ideal.quotient.mk (P ^ ideal.ramification_idx f 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]

source
theorem ideal.rank_pow_quot {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [hfp : ne_zero (ideal.ramification_idx f p P)] [is_domain S] [is_dedekind_domain S] [p.is_maximal] [P.is_prime] (hP0 : P ≠ ⊥) (i : ℕ) (hi : i ≤ ideal.ramification_idx f p P) :
module.rank (R ⧸ p) ↥(ideal.map (ideal.quotient.mk (P ^ ideal.ramification_idx f p P)) (P ^ i)) = (ideal.ramification_idx f p P - i) • module.rank (R ⧸ p) (S ⧸ P)
source
theorem ideal.rank_prime_pow_ramification_idx {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [is_domain S] [is_dedekind_domain S] [p.is_maximal] [P.is_prime] (hP0 : P ≠ ⊥) (he : ideal.ramification_idx f p P ≠ 0) :
module.rank (R ⧸ p) (S ⧸ P ^ ideal.ramification_idx f p P) = ideal.ramification_idx f 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].

source
theorem ideal.finrank_prime_pow_ramification_idx {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (p : ideal R) (P : ideal S) [is_domain S] [is_dedekind_domain S] (hP0 : P ≠ ⊥) [p.is_maximal] [P.is_prime] (he : ideal.ramification_idx f p P ≠ 0) :
finite_dimensional.finrank (R ⧸ p) (S ⧸ P ^ ideal.ramification_idx f p P) = ideal.ramification_idx f p P * finite_dimensional.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 (algebra_map R S) #

source
theorem ideal.factors.ne_bot {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)) :
↑P ≠ ⊥
source
@[protected, instance]
def ideal.factors.is_prime {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)) :
↑P.is_prime
source
theorem ideal.factors.ramification_idx_ne_zero {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)) :
ideal.ramification_idx (algebra_map R S) p ↑P ≠ 0
source
@[protected, instance]
def ideal.factors.fact_ramification_idx_ne_zero {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)) :
ne_zero (ideal.ramification_idx (algebra_map R S) p ↑P)
source
@[protected, instance]
def ideal.factors.is_scalar_tower {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)) :
is_scalar_tower R (R ⧸ p) (S ⧸ ↑P)
source
theorem ideal.factors.finrank_pow_ramification_idx {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] [p.is_maximal] (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)) :
finite_dimensional.finrank (R ⧸ p) (S ⧸ ↑P ^ ideal.ramification_idx (algebra_map R S) p ↑P) = ideal.ramification_idx (algebra_map R S) p ↑P * ideal.inertia_deg (algebra_map R S) p ↑P
source
@[protected, instance]
def ideal.factors.finite_dimensional_quotient {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] [is_noetherian R S] [p.is_maximal] (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)) :
finite_dimensional (R ⧸ p) (S ⧸ ↑P)
source
theorem ideal.factors.inertia_deg_ne_zero {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] [is_noetherian R S] [p.is_maximal] (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)) :
ideal.inertia_deg (algebra_map R S) p ↑P ≠ 0
source
@[protected, instance]
def ideal.factors.finite_dimensional_quotient_pow {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] [is_noetherian R S] [p.is_maximal] (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)) :
finite_dimensional (R ⧸ p) (S ⧸ ↑P ^ ideal.ramification_idx (algebra_map R S) p ↑P)
source
noncomputable def ideal.factors.pi_quotient_equiv {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] [is_domain S] [is_dedekind_domain S] [algebra R S] (p : ideal R) (hp : ideal.map (algebra_map R S) p ≠ ⊥) :
S ⧸ ideal.map (algebra_map R S) p ≃+* Π (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)), S ⧸ ↑P ^ ideal.ramification_idx (algebra_map 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
source
@[simp]
theorem ideal.factors.pi_quotient_equiv_mk {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] [is_domain S] [is_dedekind_domain S] [algebra R S] (p : ideal R) (hp : ideal.map (algebra_map R S) p ≠ ⊥) (x : S) :
⇑(ideal.factors.pi_quotient_equiv p hp) (⇑(ideal.quotient.mk (ideal.map (algebra_map R S) p)) x) = λ (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)), ⇑(ideal.quotient.mk (↑P ^ ideal.ramification_idx (algebra_map R S) p ↑P)) x
source
@[simp]
theorem ideal.factors.pi_quotient_equiv_map {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] [is_domain S] [is_dedekind_domain S] [algebra R S] (p : ideal R) (hp : ideal.map (algebra_map R S) p ≠ ⊥) (x : R) :
⇑(ideal.factors.pi_quotient_equiv p hp) (⇑(algebra_map R (S ⧸ ideal.map (algebra_map R S) p)) x) = λ (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)), ⇑(ideal.quotient.mk (↑P ^ ideal.ramification_idx (algebra_map R S) p ↑P)) (⇑(algebra_map R S) x)
source
noncomputable def ideal.factors.pi_quotient_linear_equiv {R : Type u} [comm_ring R] (S : Type v) [comm_ring S] [is_domain S] [is_dedekind_domain S] [algebra R S] (p : ideal R) (hp : ideal.map (algebra_map R S) p ≠ ⊥) :
(S ⧸ ideal.map (algebra_map R S) p) ≃ₗ[R ⧸ p] Π (P : ↥((unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset)), S ⧸ ↑P ^ ideal.ramification_idx (algebra_map 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
source
theorem ideal.sum_ramification_inertia {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (p : ideal R) [is_domain S] [is_dedekind_domain S] [algebra R S] (K : Type u_1) (L : Type u_2) [field K] [field L] [is_domain R] [is_dedekind_domain R] [algebra R K] [is_fraction_ring R K] [algebra S L] [is_fraction_ring S L] [algebra K L] [algebra R L] [is_scalar_tower R S L] [is_scalar_tower R K L] [is_noetherian R S] [is_integral_closure S R L] [p.is_maximal] (hp0 : p ≠ ⊥) :
(unique_factorization_monoid.factors (ideal.map (algebra_map R S) p)).to_finset.sum (λ (P : ideal S), ideal.ramification_idx (algebra_map R S) p P * ideal.inertia_deg (algebra_map R S) p P) = finite_dimensional.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.