NYLL
Module

NormalizationResidueDVR.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationResidueDVR
6 declarations indexed from sourceView source ↗

Module documentation

The residue exact sequence for an actual DVR normalization

A maximal prime of the literal normalization contracts to the closed point by the existing integral-closure prime theorem. Thus the already constructed residue-action target is exactly the quotient automorphism group over the native base residue field. The canonical quotient-to-prime-residue equivalence identifies the other field and preserves its coefficient map. The final endpoint retains the same native decomposition map and inertia.

Imports6
Imported by8

Declarations

theorem

normalizationResidueBaseIdeal_eq_maximalIdeal

L34 ↗
EtaleFundamentalGroups.Inertia.normalizationResidueBaseIdeal_eq_maximalIdeal
Documentation

The actual contracted normalization prime is the closed point, by integrality.

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 normalizationResidueBaseIdeal_eq_maximalIdeal
    (A : Type u) (L : Type w) [CommRing A] [IsLocalRing A]
    [Field L] [Algebra A L] (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal] :
    nativeAlgebraResidueBaseIdeal (normalizationCommAlgCat A L) Q =
      IsLocalRing.maximalIdeal A
def

normalizationResidueAutomorphismsOverResidueField

L47 ↗
EtaleFundamentalGroups.Inertia.normalizationResidueAutomorphismsOverResidueField
Documentation

The actual quotient automorphism group over the native base residue field.

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
def normalizationResidueAutomorphismsOverResidueField
    (A : Type u) (L : Type w) [CommRing A] [IsLocalRing A]
    [Field L] [Algebra A L] (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal] :
    GrpCat.{w}
theorem

normalizationResidueAutomorphisms_eq_overResidueField

L59 ↗
EtaleFundamentalGroups.Inertia.normalizationResidueAutomorphisms_eq_overResidueField
Documentation

The already constructed target is exactly the actual base residue target.

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 normalizationResidueAutomorphisms_eq_overResidueField
    (A : Type u) (L : Type w) [CommRing A] [IsLocalRing A]
    [Field L] [Algebra A L] (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal] :
    normalizationResidueAutomorphisms A L Q =
      normalizationResidueAutomorphismsOverResidueField A L Q
def

normalizationMaximalQuotientResidueEquiv

L72 ↗
EtaleFundamentalGroups.Inertia.normalizationMaximalQuotientResidueEquiv
Documentation

The literal normalization quotient is canonically its prime residue field.

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
def normalizationMaximalQuotientResidueEquiv
    (A : Type u) (L : Type w) [CommRing A] [CommRing L] [Algebra A L]
    (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal] :
    ((normalizationCommAlgCat A L) ⧸ Q) ≃+* Q.ResidueField
theorem

normalizationMaximalQuotientResidueEquiv_comp_quotient

L79 ↗
EtaleFundamentalGroups.Inertia.normalizationMaximalQuotientResidueEquiv_comp_quotient
Documentation

The canonical identification preserves the original normalization coefficients.

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 normalizationMaximalQuotientResidueEquiv_comp_quotient
    (A : Type u) (L : Type w) [CommRing A] [CommRing L] [Algebra A L]
    (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal] :
    (normalizationMaximalQuotientResidueEquiv A L Q).toRingHom.comp (Ideal.Quotient.mk Q) =
      algebraMap (normalizationCommAlgCat A L) Q.ResidueField
theorem

normalizationResidueDVR_exact

L93 ↗
EtaleFundamentalGroups.Inertia.normalizationResidueDVR_exact
Documentation

The original DVR normalization residue sequence: the native target is identified over the base residue field, the actual decomposition map is surjective, and its kernel included in the Galois group is exactly inertia. The canonical source-field identification is normalizationMaximalQuotientResidueEquiv.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
Lean source · statement
theorem normalizationResidueDVR_exact
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal] :
    nativeAlgebraResidueBaseIdeal (normalizationCommAlgCat A L) Q =
        IsLocalRing.maximalIdeal A ∧
      normalizationResidueAutomorphisms A L Q =
        normalizationResidueAutomorphismsOverResidueField A L Q ∧
      Function.Surjective (normalizationResidueMorphism A K L Q).hom'.toFun ∧
      (normalizationResidueMorphism A K L Q).hom'.ker.map
        (normalizationDecompositionInclusion A K L Q) = Q.inertia Gal(L/K)

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