EtaleFundamentalGroups.Inertia.componentNormalizationInertia_isConj_inv
Every inertia element in a finite Galois extension of the local fraction field at a horizontal Cartier component is conjugate to its inverse when the component's generic fibre is geometrically integral over a rational field. All regularity and residue-field data are constructed from the component, without global integrality or normality of X.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open RamificationTheory.HilbertRamification
namespace EtaleFundamentalGroups.Inertia
universe uLean source · full declaration
theorem componentNormalizationInertia_isConj_inv
{X S : Scheme.{u}} [IsLocallyNoetherian X] [IsIntegral S]
(D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
(p : X ⟶ S) (ek : S.residueField (genericPoint S) ≃+* ℚ)
(Z : Set D.1.subscheme) (hZ : Z ∈ irreducibleComponents D.1.subscheme)
(hdominant : DenseRange (D.1.componentToBase p Z hZ))
(hgeo : GeometricallyIntegral
((D.1.componentToBase p Z hZ).fiberToSpecResidueField (genericPoint S))) :
let A := X.presheaf.stalk (D.1.componentGenericPoint Z hZ)
letI : IsDomain A := isDomain_stalk_componentGenericPoint D hreg Z hZ
∀ (L : Type u) [Field L] [Algebra (FractionRing A) L]
[FiniteDimensional (FractionRing A) L] [IsGalois (FractionRing A) L],
letI : Algebra A L :=
((algebraMap (FractionRing A) L).comp
(algebraMap A (FractionRing A))).toAlgebra
letI : IsScalarTower A (FractionRing A) L :=
IsScalarTower.of_algebraMap_eq' rfl
∀ (Q : Ideal (integralClosure A L)) [Q.IsPrime]
[Q.LiesOver (IsLocalRing.maximalIdeal A)],
letI : MulSemiringAction Gal(L/FractionRing A) (integralClosure A L) :=
IsIntegralClosure.MulSemiringAction A (FractionRing A) L
(integralClosure A L)
∀ sigma : Q.toAddSubgroup.inertia Gal(L/FractionRing A),
IsConj (sigma : Gal(L/FractionRing A))
((sigma⁻¹ : Q.toAddSubgroup.inertia Gal(L/FractionRing A)) :
Gal(L/FractionRing A)) := by
let x := D.1.componentGenericPoint Z hZ
let A := X.presheaf.stalk x
let : IsDomain A := isDomain_stalk_componentGenericPoint D hreg Z hZ
let : IsDiscreteValuationRing A :=
isDiscreteValuationRing_stalk_componentGenericPoint D hreg Z hZ
let k := S.residueField (genericPoint S)
obtain ⟨hAlg, hfield⟩ :=
D.1.componentGenericPoint_exists_geometricallyIntegralResidueAlgebra
p Z hZ hdominant hgeo
let : Algebra k (X.residueField x) := hAlg
let : Algebra k (IsLocalRing.ResidueField A) := by
change Algebra k (X.residueField x)
infer_instance
dsimp only
intro L instField instAlgebra instFinite instGalois
let : Algebra A L :=
((algebraMap (FractionRing A) L).comp
(algebraMap A (FractionRing A))).toAlgebra
let : IsScalarTower A (FractionRing A) L :=
IsScalarTower.of_algebraMap_eq' rfl
intro Q instPrime instLiesOver
exact
(open _root_.TameAbhyankar.SGA1 in
idealInertia_isConj_inv_of_geometricallyIntegral_dvrNormalizationResidue_of_ratEquiv
k ek (A := A) (K := FractionRing A) (L := L) Q hfield)