EtaleFundamentalGroups.Kummer.ramificationIdx_isUnit_of_splitStrictNormalCrossings_of_heightTwoSelectedBranchExponent
Height-two unitness of the selected exact-root exponent globalizes to unitness of a chosen normalization prime's ramification index.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe uA uK uLLean source · statement
theorem
ramificationIdx_isUnit_of_splitStrictNormalCrossings_of_heightTwoSelectedBranchExponent
{A : Type uA} {K : Type uK} {L : Type uL}
[CommRing A] [IsDomain A] [IsLocalRing 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]
[Module.Finite A (integralClosure A L)]
{d r : ℕ} {f : A} {t : Fin (d + 1) → A}
(hNC : IsSplitStrictNormalCrossingsAt f t r)
(i : Fin (d + 1)) (hi : i.1 < r)
[CharZero (A ⧸ Ideal.span ({t i} : Set A))]
(Q : Ideal (integralClosure A L)) [Q.IsPrime]
[Q.LiesOver (Ideal.span ({t i} : Set A))]
(hlocal : ∀ (P : Ideal A) [P.IsPrime],
Ideal.span ({t i} : Set A) < P → P.height = 2 →
IsUnit
((heightTwoSelectedBranchGaloisRamificationIndex
(K := K) (L := L) t hNC i : ℕ) :
Localization.AtPrime P)) :
IsUnit
((Q.ramificationIdx A : ℕ) :
A ⧸ Ideal.span ({t i} : Set A))