Ramification index #
Let S/R be an extension of rings, and let q be a prime ideal of S lying over a prime ideal
p of R. Let Sq be the localization of S and q, and let pSq be the image of p in Sq.
Then the ramification index of q over R is defined to be the length of the quotient Sq/pSq as
an Sq-module.
Main definitions #
Ideal.ramificationIdx' q R: The ramification index ofqoverR.
Main statements #
ramificationIdx_eq_ramificationIdx': The ramification index agrees with the usual definition in the case of Dedekind domains.ramificationIdx'_tower: Ramification index is multiplicative in towers.
noncomputable def
Ideal.ramificationIdx'
{S : Type u_1}
[CommRing S]
(q : Ideal S)
(R : Type u_2)
[CommRing R]
[Algebra R S]
:
Let S/R be an extension of rings, and let q be a prime ideal of S lying over a prime ideal
p of R. Let Sq be the localization of S and q, and let pSq be the image of p in Sq.
Then the ramification index of q over R is defined to be the length of the quotient Sq/pSq as
an Sq-module.
When q is not prime, we use a junk value of 0.
This will eventually replace the existing definition of Ideal.ramificationIdx.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Ideal.ramificationIdx'_def
{S : Type u_1}
[CommRing S]
(q : Ideal S)
(R : Type u_2)
[CommRing R]
[Algebra R S]
[q.IsPrime]
:
q.ramificationIdx' R = (Module.length (Localization.AtPrime q)
(Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat
theorem
Ideal.ramificationIdx'_pos
{S : Type u_1}
[CommRing S]
(q : Ideal S)
(R : Type u_2)
[CommRing R]
[Algebra R S]
[q.IsPrime]
[Module.Finite R S]
:
theorem
Ideal.ramificationIdx'_eq_one
{S : Type u_1}
[CommRing S]
(q : Ideal S)
(R : Type u_2)
[CommRing R]
[Algebra R S]
[q.IsPrime]
[Algebra.EssFiniteType R S]
[Algebra.IsUnramifiedAt R q]
:
theorem
Ideal.ramificationIdx'_eq_one_iff
{S : Type u_1}
[CommRing S]
{q : Ideal S}
{R : Type u_2}
[CommRing R]
[Algebra R S]
[q.IsPrime]
[Algebra.EssFiniteType R S]
[Algebra.IsIntegral R S]
[PerfectField (under R q).ResidueField]
:
theorem
Ideal.ramificationIdx'_eq
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(p : Ideal R)
(q : Ideal S)
[q.LiesOver p]
[q.IsPrime]
:
q.ramificationIdx' R = (Module.length (Localization.AtPrime q)
(Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) p)).toNat
theorem
Ideal.ramificationIdx_eq_ramificationIdx''
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(p : Ideal R)
(q : Ideal S)
[IsDedekindDomain S]
[q.LiesOver p]
[hq : q.IsPrime]
(hpS : map (algebraMap R S) p ≠ ⊥)
:
theorem
Ideal.ramificationIdx_eq_ramificationIdx'
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(p : Ideal R)
(q : Ideal S)
[IsDomain R]
[IsDedekindDomain S]
[Module.IsTorsionFree R S]
[q.LiesOver p]
[hq : q.IsPrime]
(hp : p ≠ ⊥)
:
theorem
Ideal.IsDedekindDomain.ramificationIdx'_eq_factors_count
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(p : Ideal R)
(q : Ideal S)
[IsDedekindDomain S]
[q.LiesOver p]
(hp0 : map (algebraMap R S) p ≠ ⊥)
:
q.ramificationIdx' R = Multiset.count q (UniqueFactorizationMonoid.factors (map (algebraMap R S) p))
theorem
Ideal.IsDedekindDomain.ramificationIdx'_eq_normalizedFactors_count
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(p : Ideal R)
(q : Ideal S)
[IsDedekindDomain S]
[q.LiesOver p]
(hp0 : map (algebraMap R S) p ≠ ⊥)
:
q.ramificationIdx' R = Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R S) p))
theorem
Ideal.IsDedekindDomain.ramificationIdx'_eq_multiplicity
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(p : Ideal R)
(q : Ideal S)
[IsDedekindDomain S]
[q.IsPrime]
[q.LiesOver p]
(hp : map (algebraMap R S) p ≠ ⊥)
:
theorem
Ideal.ramificationIdx'_tower'
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[CommRing R]
[CommRing S]
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
(q : Ideal S)
(r : Ideal T)
[q.IsPrime]
[r.IsPrime]
[r.LiesOver q]
[Algebra (Localization.AtPrime q) (Localization.AtPrime r)]
[Localization.AtPrime.IsLiesOverAlgebra q r]
[Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)]
:
See ramificationIdx'_tower for a version that does not assume primality.
theorem
Ideal.ramificationIdx'_tower
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[CommRing R]
[CommRing S]
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
(q : Ideal S)
(r : Ideal T)
[r.LiesOver q]
[Module.Flat S T]
:
See ramificationIdx'_tower' for a version that only assumes local flatness.
theorem
Ideal.ramificationIdx'_below_dvd
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[CommRing R]
[CommRing S]
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
(q : Ideal S)
(r : Ideal T)
[r.LiesOver q]
[Module.Flat S T]
:
theorem
Ideal.ramificationIdx'_above_dvd
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[CommRing R]
[CommRing S]
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
(q : Ideal S)
(r : Ideal T)
[r.LiesOver q]
[Module.Flat S T]
:
theorem
Ideal.ramificationIdx'_below_le
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[CommRing R]
[CommRing S]
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
(q : Ideal S)
(r : Ideal T)
[r.IsPrime]
[r.LiesOver q]
[Module.Finite R T]
[Module.Flat S T]
:
theorem
Ideal.ramificationIdx'_above_le
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[CommRing R]
[CommRing S]
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
(q : Ideal S)
(r : Ideal T)
[r.IsPrime]
[r.LiesOver q]
[Module.Finite R T]
[Module.Flat S T]
:
@[simp]
theorem
Ideal.ramificationIdx'_smul
(R : Type u_1)
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(q : Ideal S)
{G : Type u_4}
[Group G]
[MulSemiringAction G S]
[SMulCommClass G R S]
(g : G)
: