NYLL
Module

FiniteLevelInertiaDiagram.lean

Nyll.SchemeTheory.RingTheory.Ramification.FiniteLevelInertiaDiagram
8 declarations indexed from sourceView source ↗

Module documentation

The actual finite-level diagram of inertia invariants

The stage at a finite Galois intermediate field is the preimage of the upper inertia-fixed subalgebra under the literal normalization inclusion. Transition maps are restrictions of the existing intermediate-field inclusions. The coefficient algebra is never replaced by an independently chosen action.

Imports16
  • Nyll.SchemeTheory.RingTheory.Ramification.FiniteLevelInertiaRepresentatives
  • Mathlib.Algebra.Algebra.Equiv
  • Mathlib.Algebra.Algebra.Subalgebra.Operations
  • Mathlib.Algebra.Category.AlgCat.Basic
  • Mathlib.Algebra.Category.AlgCat.FilteredColimits
  • Mathlib.Algebra.Category.Ring.FilteredColimits
  • Mathlib.Algebra.Group.Action.Defs
  • Mathlib.CategoryTheory.Category.Preorder
  • Mathlib.CategoryTheory.Filtered.Basic
  • Mathlib.CategoryTheory.Limits.Types.Filtered
  • Mathlib.Data.Finset.Insert
  • Mathlib.FieldTheory.Galois.GaloisClosure
  • Mathlib.FieldTheory.IntermediateField.Basic
  • Mathlib.FieldTheory.Normal.Basic
  • Mathlib.RingTheory.IntegralClosure.IntegralRestrict
  • Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Imported by6

Declarations

instance

normalizationInertiaCoefficientCommClass

L49 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaCoefficientCommClass
Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
variable (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]
Lean source · statement
instance normalizationInertiaCoefficientCommClass :
    SMulCommClass Gal(L/K) A (integralClosure A L)
def

finiteLevelInertiaSubalgebra

L62 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaSubalgebra
Documentation

The actual finite normalization elements whose images are fixed by the inertia of the chosen upper prime.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
variable (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]
local instance normalizationInertiaCoefficientCommClass :
    SMulCommClass Gal(L/K) A (integralClosure A L) :=
  SMul.comp.smulCommClass (α := integralClosure A L)
    (M := (integralClosure A L) ≃ₐ[A] (integralClosure A L)) (β := A)
    (galRestrict A K L (integralClosure A L))
variable (Q : Ideal (integralClosure A L)) [Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
Lean source · statement
def finiteLevelInertiaSubalgebra (E : FiniteGaloisIntermediateField K L) :
    Subalgebra A (integralClosure A E)
def

finiteLevelInertiaSubalgebraInclusion

L69 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaSubalgebraInclusion
Documentation

The literal inclusion of a finite invariant stage into the upper inertia-fixed algebra.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
variable (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]
local instance normalizationInertiaCoefficientCommClass :
    SMulCommClass Gal(L/K) A (integralClosure A L) :=
  SMul.comp.smulCommClass (α := integralClosure A L)
    (M := (integralClosure A L) ≃ₐ[A] (integralClosure A L)) (β := A)
    (galRestrict A K L (integralClosure A L))
variable (Q : Ideal (integralClosure A L)) [Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
Lean source · statement
def finiteLevelInertiaSubalgebraInclusion (E : FiniteGaloisIntermediateField K L) :
    finiteLevelInertiaSubalgebra A K L Q E →ₐ[A] CI
theorem

finiteLevelInertiaSubalgebra_eq_fixedPoints

L77 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaSubalgebra_eq_fixedPoints
Documentation

The preimage stage is exactly the finite-level inertia-invariant subalgebra. Both directions use the literal normalization inclusion, and the reverse lifting of inertia is supplied by the actual profinite image theorem.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
variable (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]
local instance normalizationInertiaCoefficientCommClass :
    SMulCommClass Gal(L/K) A (integralClosure A L) :=
  SMul.comp.smulCommClass (α := integralClosure A L)
    (M := (integralClosure A L) ≃ₐ[A] (integralClosure A L)) (β := A)
    (galRestrict A K L (integralClosure A L))
variable (Q : Ideal (integralClosure A L)) [Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
Lean source · statement
theorem finiteLevelInertiaSubalgebra_eq_fixedPoints
    (E : FiniteGaloisIntermediateField K L) :
    finiteLevelInertiaSubalgebra A K L Q E =
      FixedPoints.subalgebra A (integralClosure A E)
        ((Q.comap (IsScalarTower.toAlgHom A E L).mapIntegralClosure).inertia Gal(E/K))
def

finiteLevelInertiaSubalgebraMap

L126 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaSubalgebraMap
Documentation

The actual map between finite invariant stages induced by an inclusion of finite Galois intermediate fields.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
variable (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]
local instance normalizationInertiaCoefficientCommClass :
    SMulCommClass Gal(L/K) A (integralClosure A L) :=
  SMul.comp.smulCommClass (α := integralClosure A L)
    (M := (integralClosure A L) ≃ₐ[A] (integralClosure A L)) (β := A)
    (galRestrict A K L (integralClosure A L))
variable (Q : Ideal (integralClosure A L)) [Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
Lean source · statement
def finiteLevelInertiaSubalgebraMap {E F : FiniteGaloisIntermediateField K L}
    (h : E ≤ F) :
    finiteLevelInertiaSubalgebra A K L Q E →ₐ[A]
      finiteLevelInertiaSubalgebra A K L Q F
def

finiteLevelInertiaDiagram

L145 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaDiagram
Documentation

The actual filtered diagram, retaining the original base algebra.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
variable (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]
local instance normalizationInertiaCoefficientCommClass :
    SMulCommClass Gal(L/K) A (integralClosure A L) :=
  SMul.comp.smulCommClass (α := integralClosure A L)
    (M := (integralClosure A L) ≃ₐ[A] (integralClosure A L)) (β := A)
    (galRestrict A K L (integralClosure A L))
variable (Q : Ideal (integralClosure A L)) [Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
Lean source · full declaration
def finiteLevelInertiaDiagram : FiniteGaloisIntermediateField K L ⥤ AlgCat.{w} A where
  obj E := AlgCat.of A (finiteLevelInertiaSubalgebra A K L Q E)
  map f := AlgCat.ofHom (finiteLevelInertiaSubalgebraMap A K L Q f.le)
  map_id E := by
    ext b
    rfl
  map_comp f g := by
    ext b
    rfl
def

finiteLevelInertiaCocone

L156 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaCocone
Documentation

The literal normalization inclusions form the invariant cocone.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
variable (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]
local instance normalizationInertiaCoefficientCommClass :
    SMulCommClass Gal(L/K) A (integralClosure A L) :=
  SMul.comp.smulCommClass (α := integralClosure A L)
    (M := (integralClosure A L) ≃ₐ[A] (integralClosure A L)) (β := A)
    (galRestrict A K L (integralClosure A L))
variable (Q : Ideal (integralClosure A L)) [Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
Lean source · full declaration
def finiteLevelInertiaCocone : Cocone (finiteLevelInertiaDiagram A K L Q) where
  pt := AlgCat.of A CI
  ι.app E := AlgCat.ofHom (finiteLevelInertiaSubalgebraInclusion A K L Q E)
  ι.naturality E F f := by
    ext b
    rfl
def

finiteLevelInertiaCoconeIsColimit

L166 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaCoconeIsColimit
Documentation

The upper inertia-fixed algebra is the filtered colimit of its actual finite invariant stages. Finite representatives supply the cocone surjectivity; literal field inclusions detect equality already at each stage.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
variable (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]
local instance normalizationInertiaCoefficientCommClass :
    SMulCommClass Gal(L/K) A (integralClosure A L) :=
  SMul.comp.smulCommClass (α := integralClosure A L)
    (M := (integralClosure A L) ≃ₐ[A] (integralClosure A L)) (β := A)
    (galRestrict A K L (integralClosure A L))
variable (Q : Ideal (integralClosure A L)) [Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
Lean source · statement
def finiteLevelInertiaCoconeIsColimit :
    IsColimit (finiteLevelInertiaCocone A K L Q)

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