Yamaguchi26SolvableCoverings.exists_componentNormalizationPoint_strictImage_le_inertia
The actual strict-Henselian generic finite image is contained in the stabilizer of a geometric point over the original component geometric point. The point and the fixed action are constructed from the pointed cover.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]Lean source · statement
theorem exists_componentNormalizationPoint_strictImage_le_inertia
(D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
[ConnectedSpace D.1.supportComplement] (E : Component D)
{Ξ : Type} [Field Ξ] [IsSepClosed Ξ]
(xi : Spec (.of Ξ) ⟶ Spec (.of (boundaryStrictFractionField D E)))
(W : FiniteEtale D.1.supportComplement) (hW : IsGalois W)
(w : (FiniteEtale.fiber (xi ≫ boundaryStrictGenericMorphism D hreg E)).obj W) :
∃ z : Spec (.of (AlgebraicClosure (X.residueField (componentPoint D E)))) ⟶
(W.hom ≫ D.1.supportComplement.ι).normalization,
z ≫ (W.hom ≫ D.1.supportComplement.ι).fromNormalization = componentGeometricPoint D E ∧
(finiteEtaleGaloisCoverQuotientOfMorphism
(boundaryStrictGenericMorphism D hreg E) xi W hW w).range ≤
(finiteCoverInertia D W E z).op