NYLL
Module

NormalizationResidueCharacteristic.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationResidueCharacteristic
3 declarations indexed from sourceView source ↗

Module documentation

Base and normalization residue characteristic

The actual coefficient map descends from the base local ring to its residue field at every prime lying over its maximal ideal. Its field-domain injectivity identifies the two residue characteristics, including mixed-characteristic bases.

Imports4
Imported by4

Declarations

def

baseResidueToIdealResidue

L30 ↗
EtaleFundamentalGroups.Inertia.baseResidueToIdealResidue
Documentation

The actual coefficient map on residue fields at a prime lying over the closed point of the local base.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
Lean source · statement
def baseResidueToIdealResidue
    (A : Type u) (B : Type v) [CommRing A] [IsLocalRing A]
    [CommRing B] [Algebra A B]
    (Q : Ideal B) [Q.IsPrime] [Q.LiesOver (IsLocalRing.maximalIdeal A)] :
    IsLocalRing.ResidueField A →+* Q.ResidueField
theorem

idealResidue_ringExpChar_eq_baseResidue

L46 ↗
EtaleFundamentalGroups.Inertia.idealResidue_ringExpChar_eq_baseResidue
Documentation

The actual prime residue field has the same exponential characteristic as the base residue field, through the injective coefficient residue map.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
Lean source · statement
theorem idealResidue_ringExpChar_eq_baseResidue
    (A : Type u) (B : Type v) [CommRing A] [IsLocalRing A]
    [CommRing B] [Algebra A B]
    (Q : Ideal B) [Q.IsPrime] [Q.LiesOver (IsLocalRing.maximalIdeal A)] :
    ringExpChar Q.ResidueField = ringExpChar (IsLocalRing.ResidueField A)
theorem

normalizationResidue_ringExpChar_eq_baseResidue

L59 ↗
EtaleFundamentalGroups.Inertia.normalizationResidue_ringExpChar_eq_baseResidue
Documentation

At an actual maximal normalization prime, the residue characteristic is the base residue characteristic; its contraction is constructed.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
Lean source · statement
theorem normalizationResidue_ringExpChar_eq_baseResidue
    (A : Type u) (F : Type v) [CommRing A] [IsLocalRing A]
    [CommRing F] [Algebra A F]
    (Q : Ideal (normalizationCommAlgCat A F)) [Q.IsMaximal] :
    ringExpChar Q.ResidueField = ringExpChar (IsLocalRing.ResidueField A)

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