Module

CartierStrictNormalizationEtale.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.CartierStrictNormalizationEtale

4 declarations indexed from sourceView source ↗

Module documentation

Strict generic triviality and the original normalization at a Cartier point

The actual strict generic pullback is compared to the iterated pullback via the local fraction field. Etaleness of its normalization is then transported through the actual Cartier square and the normalization-stalk comparison.

Imports4

Imported by2

instance

(anonymous instance)

L27 ↗

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry.FiniteEtale EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.StrictHenselian

Lean source · statement

instance (X : Scheme.{0}) :
    Category (MorphismProperty.Over (@IsFiniteEtale : MorphismProperty Scheme.{0}) ⊤ X)

instance

(anonymous instance)

L31 ↗

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry.FiniteEtale EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.StrictHenselian
local instance (X : Scheme.{0}) :
    Category (MorphismProperty.Over (@IsFiniteEtale : MorphismProperty Scheme.{0}) ⊤ X) :=
  AlgebraicGeometry.FiniteEtale.instCategory X

Lean source · statement

instance {X Y : Scheme.{0}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong (@IsFiniteEtale : MorphismProperty Scheme.{0}) f

instance

(anonymous instance)

L35 ↗

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry.FiniteEtale EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.StrictHenselian
local instance (X : Scheme.{0}) :
    Category (MorphismProperty.Over (@IsFiniteEtale : MorphismProperty Scheme.{0}) ⊤ X) :=
  AlgebraicGeometry.FiniteEtale.instCategory X
local instance {X Y : Scheme.{0}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong (@IsFiniteEtale : MorphismProperty Scheme.{0}) f :=
  ⟨fun _ _ ↦ inferInstance⟩

Lean source · statement

instance {X Y : Scheme.{0}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{0}) f

theorem

normalization_stalk_etale_of_strictGeneric_image_fixed

L42 ↗

EtaleFundamentalGroups.StrictHenselian.normalization_stalk_etale_of_strictGeneric_image_fixed

Documentation

Triviality of the actual strict generic action at a boundary DVR makes the base change of the original cover's normalization etale at that stalk.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry.FiniteEtale EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.StrictHenselian
local instance (X : Scheme.{0}) :
    Category (MorphismProperty.Over (@IsFiniteEtale : MorphismProperty Scheme.{0}) ⊤ X) :=
  AlgebraicGeometry.FiniteEtale.instCategory X
local instance {X Y : Scheme.{0}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong (@IsFiniteEtale : MorphismProperty Scheme.{0}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance {X Y : Scheme.{0}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{0}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback (P := @IsFiniteEtale) h hf⟩

Lean source · statement

theorem normalization_stalk_etale_of_strictGeneric_image_fixed
    {X : Scheme.{0}} [IsLocallyNoetherian X]
    (D : X.EffectiveCartierDivisor) (x : X) (hx : x ∈ D.1.support)
    [IsDomain (X.presheaf.stalk x)] [IsDiscreteValuationRing (X.presheaf.stalk x)]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (φ : X.presheaf.stalk x →+* Ω) [IsLocalHom φ]
    (W : FiniteEtale D.1.supportComplement)
    {Ω' : Type} [Field Ω'] [IsSepClosed Ω']
    (point : Spec (.of Ω') ⟶ Spec (.of
      (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))))))
    (hfixed : ∀ (g : Aut (fiber point))
      (w : (fiber (point ≫ geometricStalkFractionFieldToComplement D x φ)).obj W),
      fundamentalGroupHom (geometricStalkFractionFieldToComplement D x φ) point g • w = w) :
    Etale (Limits.pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
      (X.fromSpecStalk x))

Module documentation

Strict generic triviality and the original normalization at a Cartier point

Declarations

(anonymous instance)

(anonymous instance)

(anonymous instance)

normalization_stalk_etale_of_strictGeneric_image_fixed