EtaleFundamentalGroups.normalizationInertia_natCard_eq_of_etaleBaseChangeProductMap_surjective
Inertia at compatible normalization primes has the same cardinality after an etale function-field base change whose canonical product map selects the target field.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uLean source · statement
theorem normalizationInertia_natCard_eq_of_etaleBaseChangeProductMap_surjective
{A C F KC L M : Type u}
[CommRing A] [IsDomain A] [IsNoetherianRing A]
[IsIntegrallyClosed A]
[CommRing C] [IsDomain C] [IsNoetherianRing C]
[IsIntegrallyClosed C] [Algebra A C] [Algebra.Etale A C]
[Field F] [Algebra A F] [IsFractionRing A F]
[Field KC] [Algebra C KC] [IsFractionRing C KC]
[Algebra A KC] [IsScalarTower A C KC]
[Field L] [Algebra F L] [Algebra A L] [IsScalarTower A F L]
[FiniteDimensional F L] [IsGalois F L]
[Field M] [Algebra KC M] [Algebra C M] [IsScalarTower C KC M]
[FiniteDimensional KC M] [IsGalois KC M]
[Algebra L M] [Algebra A M] [IsScalarTower A L M]
[IsScalarTower A C M]
(hproduct : Function.Surjective
(etaleBaseChangeProductMap (A := A) (C := C) (L := L) (M := M)))
(p : Ideal A) [p.IsPrime] (hpheight : p.height = 1)
(P : Ideal C) [P.IsPrime] (hPheight : P.height = 1)
(q : Ideal (integralClosure A L)) [q.IsPrime] [q.LiesOver p]
(Q : Ideal (integralClosure C M)) [Q.IsPrime] [Q.LiesOver P]
[CharZero (A ⧸ p)] [CharZero (C ⧸ P)]
(hQq : q = Q.comap
(integralClosureEtaleBaseChangeHom
(A := A) (C := C) (L := L) (M := M))) :
Nat.card (Q.toAddSubgroup.inertia Gal(M/KC)) =
Nat.card (q.toAddSubgroup.inertia Gal(L/F))