Residue degree and ramification index over isomorphic base rings #
Let R → S → T be a tower of algebras in which algebraMap R S is bijective. Then an ideal of
T has the same residue degree over R as over S, and, under the flatness needed for
multiplicativity of ramification indices in towers, the same ramification index. This lets
statements about two presentations of the same base ring, such as ℤ and the ring of integers
of ℚ, be transported into each other.
Main results #
Ideal.inertiaDeg_eq_of_bijective:r.inertiaDeg S = r.inertiaDeg R.Ideal.ramificationIdx_eq_of_bijective:r.ramificationIdx S = r.ramificationIdx R.
theorem
Ideal.inertiaDeg_eq_of_bijective
{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]
(h : Function.Bijective ⇑(algebraMap R S))
(r : Ideal T)
:
An ideal has the same residue degree over S as over R when algebraMap R S is
bijective.
theorem
Ideal.ramificationIdx_eq_of_bijective
{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]
[Module.Flat S T]
(h : Function.Bijective ⇑(algebraMap R S))
(r : Ideal T)
:
An ideal has the same ramification index over S as over R when algebraMap R S is
bijective and T is flat over S.