Module

NativeAbsoluteResidueFields.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeAbsoluteResidueFields

10 declarations indexed from sourceView source ↗

Module documentation

Native quotient residue fields and coefficient actions

Constructs bundled maximal quotient fields and their residue coefficient actions for integral algebras. Proves algebraicity of these actions and specializes them to normalization residue fields.

Imports6

Nyll.EtaleFundamentalGroups.Inertia.NormalizationResidueDVR
Nyll.SchemeTheory.RingTheory.Ramification.NativeAlgebraResidueCoefficient
Mathlib.CategoryTheory.ConcreteCategory.Bundled
Mathlib.Algebra.Category.CommAlgCat.Basic
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Imported by7

instance

bundledResidueField

L31 ↗

EtaleFundamentalGroups.Inertia.bundledResidueField

Documentation

A bundled field retains its own stored field structure.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

instance bundledResidueField (F : Bundled Field.{u}) : Field F.α

def

maximalQuotientFieldObject

L34 ↗

EtaleFundamentalGroups.Inertia.maximalQuotientFieldObject

Documentation

A literal maximal quotient, with the canonical maximal-ideal field structure.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

def maximalQuotientFieldObject (B : CommRingCat.{v}) (Q : Ideal B.carrier) [Q.IsMaximal] :
    Bundled Field.{v}

def

integralResidueFieldAlgebra

L40 ↗

EtaleFundamentalGroups.Inertia.integralResidueFieldAlgebra

Documentation

The actual quotient coefficient action over the local residue field. Integrality proves that the chosen maximal prime contracts to the closed point.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

def integralResidueFieldAlgebra
    (A : Type u) [CommRing A] [IsLocalRing A] (B : CommAlgCat.{v} A)
    [Algebra.IsIntegral A B.carrier] (Q : Ideal B.carrier) [Q.IsMaximal] :
    Algebra (IsLocalRing.ResidueField A)
      (maximalQuotientFieldObject (CommRingCat.of B.carrier) Q).α

theorem

quotient_isIntegral

L52 ↗

EtaleFundamentalGroups.Inertia.quotient_isIntegral

Documentation

Integrality descends through the literal quotient before either residue field or its coefficient action is introduced.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

theorem quotient_isIntegral
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [Algebra.IsIntegral A B] (Q : Ideal B) : Algebra.IsIntegral A (B ⧸ Q)

theorem

integralResidueFieldAlgebra_isAlgebraic

L59 ↗

EtaleFundamentalGroups.Inertia.integralResidueFieldAlgebra_isAlgebraic

Documentation

The computed residue coefficient action is algebraic, by descending the original integral extension to its actual quotients.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · full declaration

theorem integralResidueFieldAlgebra_isAlgebraic
    (A : Type u) [CommRing A] [IsLocalRing A] (B : CommAlgCat.{v} A)
    [Algebra.IsIntegral A B] (Q : Ideal B) [Q.IsMaximal] :
    letI := integralResidueFieldAlgebra A B Q
    Algebra.IsAlgebraic (IsLocalRing.ResidueField A)
      (maximalQuotientFieldObject (CommRingCat.of B) Q) := by
  have hmax : (Q.under A).IsMaximal := Ideal.isMaximal_under_of_isIntegral_of_isMaximal Q
  have hover : Q.LiesOver (IsLocalRing.maximalIdeal A) :=
    ⟨(IsLocalRing.eq_maximalIdeal hmax).symm⟩
  have hint : Algebra.IsIntegral A (B ⧸ Q) := quotient_isIntegral A B Q
  have hres : Algebra.IsIntegral (A ⧸ IsLocalRing.maximalIdeal A) (B ⧸ Q) :=
    ⟨fun x => (Algebra.IsIntegral.isIntegral (R := A) x).tower_top⟩
  change Algebra.IsAlgebraic (A ⧸ IsLocalRing.maximalIdeal A) (B ⧸ Q)
  infer_instance

def

normalizationResidueFieldObject

L75 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueFieldObject

Documentation

The literal quotient of the actual normalization as a native field object.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

def normalizationResidueFieldObject
    (A : Type u) (Ω : Type w) [CommRing A] [CommRing Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] : Bundled Field.{w}

def

normalizationResidueActionScalar

L82 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueActionScalar

Documentation

The actual native residue automorphism evaluated on the stored literal field carrier. Its quotient interface stays inside this field owner.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

def normalizationResidueActionScalar
    (A : Type u) (Ω : Type w) [CommRing A] [CommRing Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
    (σ : (normalizationResidueAutomorphisms A Ω Q).carrier)
    (z : (normalizationResidueFieldObject A Ω Q).α) :
    (normalizationResidueFieldObject A Ω Q).α

theorem

normalizationResidueActionScalar_apply

L93 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueActionScalar_apply

Documentation

The stored coefficient evaluation is the SAME underlying native quotient ring automorphism at every literal field element.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

theorem normalizationResidueActionScalar_apply
    (A : Type u) (Ω : Type w) [CommRing A] [CommRing Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
    (σ : (normalizationResidueAutomorphisms A Ω Q).carrier)
    (z : (normalizationResidueFieldObject A Ω Q).α) :
    normalizationResidueActionScalar A Ω Q σ z =
      (nativeAlgebraResidueAutomorphismRingEquiv (normalizationCommAlgCat A Ω) Q σ
        ).toRingHom.toFun z

def

normalizationResidueFieldAlgebra

L104 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueFieldAlgebra

Documentation

The actual coefficient field action on the literal normalization residue.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

def normalizationResidueFieldAlgebra
    (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
    [CommRing Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] :
    Algebra (IsLocalRing.ResidueField A) (normalizationResidueFieldObject A Ω Q)

theorem

normalizationResidueFieldAlgebra_isAlgebraic

L114 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueFieldAlgebra_isAlgebraic

Documentation

The two literal normalization residue fields form an algebraic extension.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · full declaration

theorem normalizationResidueFieldAlgebra_isAlgebraic
    (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
    [CommRing Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] :
    letI := normalizationResidueFieldAlgebra A Ω Q
    Algebra.IsAlgebraic (IsLocalRing.ResidueField A) (normalizationResidueFieldObject A Ω Q) := by
  have : Algebra.IsIntegral A (normalizationCommAlgCat A Ω) :=
    inferInstanceAs (Algebra.IsIntegral A (integralClosure A Ω))
  exact integralResidueFieldAlgebra_isAlgebraic A (normalizationCommAlgCat A Ω) Q

Module documentation

Native quotient residue fields and coefficient actions

Declarations