LeanPool.Neukirch.ExtensionOfDedekindDomains #
Imported Lean Pool material for LeanPool.Neukirch.ExtensionOfDedekindDomains.
theorem
Ideal.ramificationIdx_algebra_tower_of_eq
{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]
(_hf0 : map (algebraMap R S) p ≠ ⊥)
(hg0 : map (algebraMap S T) P ≠ ⊥)
(hfg : map (algebraMap R T) p ≠ ⊥)
(_hp0 : P ≠ ⊥)
(_hq0 : Q ≠ 0)
(hg : P = comap (algebraMap S T) Q)
:
Multiplicativity of the ramification index in a tower of Dedekind domains, stated with the hypotheses used by the Hilbert ramification development.
theorem
Ideal.quotient_finrank_algebra_tower_of_eq
{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]
(hp : p = comap (algebraMap R S) P)
(hP : P = comap (algebraMap S T) I)
:
have this := ⋯;
have this_1 := ⋯;
have this_2 := ⋯;
Module.finrank (R ⧸ p) (T ⧸ I) = Module.finrank (R ⧸ p) (S ⧸ P) * Module.finrank (S ⧸ P) (T ⧸ I)
The quotient-dimension tower law retains the former inertia-degree formula even when the ideal upstairs is not prime, where the residue-field inertia degree is zero.
theorem
Ideal.inertiaDeg_algebra_tower_of_eq
(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}
{I : Ideal T}
(hP : P = comap (algebraMap S T) I)
:
Multiplicativity of the inertia degree in a tower of Dedekind domains, stated with the hypotheses used by the Hilbert ramification development.
class
Ideal.Nonsplit
{R : Type u_4}
{S : Type u_5}
[CommRing R]
[CommRing S]
(f : R →+* S)
(p : Ideal R)
:
The decomposition of a prime in a tower is Nonsplit when there is a unique prime above.
- nonsplit (P : Ideal S) : P.IsMaximal → p = comap f P → ∀ (Q : Ideal S), Q.IsMaximal → p = comap f Q → P = Q
There is at most one maximal ideal lying over
p.