NYLL
Module

DVRGeometricInertiaEtale.lean

Nyll.EtaleFundamentalGroups.Inertia.DVRGeometricInertiaEtale
2 declarations indexed from sourceView source ↗

Module documentation

Fixed geometric-point inertia implies étaleness over a DVR

Every prime over the closed point is represented in the fixed algebraic closure of the base residue field. The actual affine normalization comparison then turns geometric fixed-point triviality into the ideal inertia condition.

Imports3
Imported by2

Declarations

theorem

specNormalizationIso_hom_base

L29 ↗
EtaleFundamentalGroups.Inertia.specNormalizationIso_hom_base
Documentation

The actual affine normalization isomorphism commutes with its base map.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
Lean source · statement
theorem specNormalizationIso_hom_base
    (R B : Type u) [CommRing R] [CommRing B] [Algebra R B] :
    (specNormalizationIso R B).hom ≫
        Spec.map (CommRingCat.ofHom (algebraMap R (integralClosure R B))) =
      (Spec.map (CommRingCat.ofHom (algebraMap R B))).fromNormalization
theorem

integralClosure_etale_of_dvr_of_geometricInertia_trivial

L41 ↗
EtaleFundamentalGroups.Inertia.integralClosure_etale_of_dvr_of_geometricInertia_trivial
Documentation

Triviality at all actual normalized geometric points over the fixed algebraic closure of the closed residue field makes the normalization étale.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
Lean source · statement
theorem integralClosure_etale_of_dvr_of_geometricInertia_trivial
    (R K L : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L]
    [FiniteDimensional K L] [IsGalois K L]
    (hfix : ∀ (z : Spec (.of (AlgebraicClosure (IsLocalRing.ResidueField R))) ⟶
        (Spec.map (CommRingCat.ofHom (algebraMap R L))).normalization),
      z ≫ (Spec.map (CommRingCat.ofHom (algebraMap R L))).fromNormalization =
          Spec.map (CommRingCat.ofHom
            ((algebraMap (IsLocalRing.ResidueField R)
              (AlgebraicClosure (IsLocalRing.ResidueField R))).comp
                (IsLocalRing.residue R))) →
      ∀ σ : Gal(L/K),
        z ≫ affineNormalizationDeck R L (σ.restrictScalars R) = z → σ = 1) :
    Algebra.Etale R (integralClosure R L)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.