NYLL
Module

EtaleNormalizationInertia.lean

Nyll.EtaleFundamentalGroups.Inertia.EtaleNormalizationInertia
1 declaration indexed from sourceView source ↗

Module documentation

Original inertia of an etale normalization

Prime rigidity makes the intrinsic coefficient inertia trivial. The proved normalization-restriction equivalence transfers this result to the original finite-Galois inertia group, with its original action and original prime. This is the affine implication from etaleness to condition (9) in Tag 0BTF. No Noetherian, DVR, or henselian hypothesis is imposed.

Reference: https://stacks.math.columbia.edu/tag/0BTF

Imports5
Imported by2

Declarations

theorem

actualNormalizationInertia_subsingleton_of_etale

L35 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationInertia_subsingleton_of_etale
Documentation

In an actual finite Galois normalization which is etale over its base, the original ideal inertia at every prime is trivial.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem actualNormalizationInertia_subsingleton_of_etale
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [IsGalois K L] [FiniteDimensional K L]
    [Algebra.Etale A (normalizationCommAlgCat A L).carrier]
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsPrime] :
    Subsingleton (actualNormalizationInertiaGroup A K L Q).carrier

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