Module

NativeMaximalResidue.lean

Nyll.SchemeTheory.RingTheory.Ramification.NativeMaximalResidue

6 declarations indexed from sourceView source ↗

Module documentation

Literal maximal-ideal residue identifications

The coefficient residue field is the native local-ring quotient. At a maximal ideal, the canonical quotient-to-prime-residue map is bijective; its actual map defines the equivalence below and preserves the original quotient coefficient map.

Imports3

Nyll.SchemeTheory.RingTheory.Ramification.NativeResidueAction
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.Algebra.Ring.Equiv

Imported by7

def

nativeResidueAutomorphismsOverResidueField

L27 ↗

EtaleFundamentalGroups.Inertia.nativeResidueAutomorphismsOverResidueField

Documentation

The literal quotient automorphisms over the native residue field of the base.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

def nativeResidueAutomorphismsOverResidueField
    (A : Type u) (B : Type v) [CommRing A] [IsLocalRing A]
    [CommRing B] [Algebra A B] (p : Ideal A) (q : Ideal B)
    [q.LiesOver p] (h : p = IsLocalRing.maximalIdeal A) : GrpCat.{v}

theorem

nativeResidueAutomorphisms_eq_overResidueField

L39 ↗

EtaleFundamentalGroups.Inertia.nativeResidueAutomorphisms_eq_overResidueField

Documentation

The computed quotient target is exactly the base-residue-field target when its actual contracted prime is the closed point.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem nativeResidueAutomorphisms_eq_overResidueField
    (A : Type u) (B : Type v) [CommRing A] [IsLocalRing A]
    [CommRing B] [Algebra A B] (p : Ideal A) (q : Ideal B)
    [q.LiesOver p] (h : p = IsLocalRing.maximalIdeal A) :
    nativeResidueAutomorphisms A B p q =
      nativeResidueAutomorphismsOverResidueField A B p q h

def

nativeResidueAutomorphismOverResidueFieldRingEquiv

L50 ↗

EtaleFundamentalGroups.Inertia.nativeResidueAutomorphismOverResidueFieldRingEquiv

Documentation

Forget coefficient linearity only after the native closed-point transport has installed its one residue algebra.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

def nativeResidueAutomorphismOverResidueFieldRingEquiv
    (A : Type u) (B : Type v) [CommRing A] [IsLocalRing A]
    [CommRing B] [Algebra A B] (p : Ideal A) (q : Ideal B)
    [q.LiesOver p] (h : p = IsLocalRing.maximalIdeal A)
    (σ : (nativeResidueAutomorphismsOverResidueField A B p q h).carrier) :
    (B ⧸ q) ≃+* (B ⧸ q)

theorem

nativeResidueAutomorphisms_eq_overResidueField_ringEquiv

L64 ↗

EtaleFundamentalGroups.Inertia.nativeResidueAutomorphisms_eq_overResidueField_ringEquiv

Documentation

The closed-point transport changes only the coefficient field label. Its underlying automorphism of the literal quotient is unchanged.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem nativeResidueAutomorphisms_eq_overResidueField_ringEquiv
    (A : Type u) (B : Type v) [CommRing A] [IsLocalRing A]
    [CommRing B] [Algebra A B] (p : Ideal A) (q : Ideal B)
    [q.LiesOver p] (h : p = IsLocalRing.maximalIdeal A)
    (σ : (nativeResidueAutomorphisms A B p q).carrier) :
    nativeResidueAutomorphismOverResidueFieldRingEquiv A B p q h
      ((CategoryTheory.eqToIso
        (nativeResidueAutomorphisms_eq_overResidueField A B p q h)).hom.hom'.toFun σ) =
      nativeResidueAutomorphismRingEquiv A B p q σ

def

maximalQuotientResidueEquiv

L77 ↗

EtaleFundamentalGroups.Inertia.maximalQuotientResidueEquiv

Documentation

The equivalence supplied by the actual canonical maximal residue map.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

def maximalQuotientResidueEquiv
    {B : Type v} [CommRing B] (q : Ideal B) [q.IsMaximal] :
    (B ⧸ q) ≃+* q.ResidueField

theorem

maximalQuotientResidueEquiv_comp_quotient

L84 ↗

EtaleFundamentalGroups.Inertia.maximalQuotientResidueEquiv_comp_quotient

Documentation

The equivalence retains the original quotient-to-residue coefficient map.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem maximalQuotientResidueEquiv_comp_quotient
    {B : Type v} [CommRing B] (q : Ideal B) [q.IsMaximal] :
    (maximalQuotientResidueEquiv q).toRingHom.comp (Ideal.Quotient.mk q) =
      algebraMap B q.ResidueField

Module documentation

Literal maximal-ideal residue identifications

Declarations

nativeResidueAutomorphismsOverResidueField

nativeResidueAutomorphisms_eq_overResidueField

nativeResidueAutomorphismOverResidueFieldRingEquiv

nativeResidueAutomorphisms_eq_overResidueField_ringEquiv

maximalQuotientResidueEquiv

maximalQuotientResidueEquiv_comp_quotient