EtaleFundamentalGroups.normalization_ramificationIdx_dvd_finrank_of_charZero
For a finite Galois extension, every characteristic-zero height-one ramification index divides the field degree.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe u v wLean source · statement
theorem normalization_ramificationIdx_dvd_finrank_of_charZero
{A : Type u} {K : Type v} {L : Type w}
[CommRing A] [IsDomain A] [IsRegularRing A] [Field K] [Field L]
[Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L]
[FiniteDimensional K L] [IsGalois K L]
(P : Ideal A) [P.IsPrime] (hP : P.height = 1)
(Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P]
[CharZero (A ⧸ P)] :
Q.ramificationIdx A ∣ Module.finrank K L