NYLL
Module

FiniteLevelInertiaLocalization.lean

Nyll.SchemeTheory.RingTheory.Ramification.FiniteLevelInertiaLocalization
13 declarations indexed from sourceView source ↗

Module documentation

The actual localized finite-level invariant colimit

Every stage is localized at the literal contraction of the chosen upper prime. The maps are the existing Localization.localAlgHom; their composition and values on fractions use the existing local-ring homomorphism identities. Finite representatives of numerator and denominator give surjectivity, and the existing localization map-injectivity theorem detects equality.

Imports11
  • Nyll.SchemeTheory.RingTheory.Ramification.FiniteLevelInertiaDiagram
  • Mathlib.Algebra.Category.AlgCat.FilteredColimits
  • Mathlib.Algebra.Category.Ring.FilteredColimits
  • Mathlib.CategoryTheory.ConcreteCategory.Basic
  • Mathlib.CategoryTheory.Limits.Types.Filtered
  • Mathlib.Data.Finset.Insert
  • Mathlib.RingTheory.Ideal.Over
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.Localization.Basic
  • Mathlib.RingTheory.Localization.Defs
  • Mathlib.RingTheory.OreLocalization.Ring
Imported by5

Declarations

def

primeLocalizationAlgCat

L40 ↗
EtaleFundamentalGroups.Inertia.primeLocalizationAlgCat
Documentation

Expose the one native localization ring dictionary at the categorical object boundary. Its Ring projection is the native Ore localization Ring.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
def primeLocalizationAlgCat
    (B : Type u) (R : Type w) [CommRing B] [CommRing R] [Algebra B R]
    (p : Ideal R) [p.IsPrime] : AlgCat.{w} B
theorem

localRingHom_injective_of_injective

L49 ↗
EtaleFundamentalGroups.Inertia.localRingHom_injective_of_injective
Documentation

Apply the existing localization injectivity theorem before introducing normalization towers. This keeps the ring carriers fixed at its native API.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem localRingHom_injective_of_injective
    {R S : Type*} [CommRing R] [CommRing S] [IsDomain S]
    (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime]
    (f : R →+* S) (hpq : p = q.comap f) (hf : Function.Injective f) :
    Function.Injective (Localization.localRingHom p q f hpq)
def

inertiaInvariantPrime

L78 ↗
EtaleFundamentalGroups.Inertia.inertiaInvariantPrime
Documentation

The chosen prime contracted to the actual upper inertia-fixed algebra.

Source context 8 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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
Lean source · statement
def inertiaInvariantPrime : Ideal CI
instance

inertiaInvariantPrime_isPrime

L81 ↗
EtaleFundamentalGroups.Inertia.inertiaInvariantPrime_isPrime
Source context 8 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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
Lean source · statement
instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime
def

finiteLevelInertiaPrime

L85 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaPrime
Documentation

Its literal contraction to the finite invariant stage.

Source context 9 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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
local instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime :=
  Ideal.IsPrime.comap (FixedPoints.subalgebra A C (Q.inertia Gal(L/K))).val
Lean source · statement
def finiteLevelInertiaPrime (E : FiniteGaloisIntermediateField K L) :
    Ideal (finiteLevelInertiaSubalgebra A K L Q E)
instance

finiteLevelInertiaPrime_isPrime

L89 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaPrime_isPrime
Source context 9 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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
local instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime :=
  Ideal.IsPrime.comap (FixedPoints.subalgebra A C (Q.inertia Gal(L/K))).val
Lean source · statement
instance finiteLevelInertiaPrime_isPrime (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaPrime A K L Q E).IsPrime
def

finiteLevelInertiaLocalizationMap

L94 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaLocalizationMap
Documentation

The native localization map between the actual contracted-prime stages.

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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
local instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime :=
  Ideal.IsPrime.comap (FixedPoints.subalgebra A C (Q.inertia Gal(L/K))).val
local instance finiteLevelInertiaPrime_isPrime (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaPrime A K L Q E).IsPrime :=
  Ideal.IsPrime.comap (finiteLevelInertiaSubalgebraInclusion A K L Q E)
Lean source · statement
def finiteLevelInertiaLocalizationMap {E F : FiniteGaloisIntermediateField K L} (h : E ≤ F) :
    Localization.AtPrime (finiteLevelInertiaPrime A K L Q E) →ₐ[A]
      Localization.AtPrime (finiteLevelInertiaPrime A K L Q F)
def

finiteLevelInertiaLocalizationInclusion

L102 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaLocalizationInclusion
Documentation

The native localization map into the chosen upper invariant local ring.

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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
local instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime :=
  Ideal.IsPrime.comap (FixedPoints.subalgebra A C (Q.inertia Gal(L/K))).val
local instance finiteLevelInertiaPrime_isPrime (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaPrime A K L Q E).IsPrime :=
  Ideal.IsPrime.comap (finiteLevelInertiaSubalgebraInclusion A K L Q E)
Lean source · statement
def finiteLevelInertiaLocalizationInclusion (E : FiniteGaloisIntermediateField K L) :
    Localization.AtPrime (finiteLevelInertiaPrime A K L Q E) →ₐ[A]
      Localization.AtPrime (inertiaInvariantPrime A K L Q)
def

finiteLevelInertiaLocalizationDiagram

L109 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaLocalizationDiagram
Documentation

The actual finite-Galois diagram of invariant local rings.

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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
local instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime :=
  Ideal.IsPrime.comap (FixedPoints.subalgebra A C (Q.inertia Gal(L/K))).val
local instance finiteLevelInertiaPrime_isPrime (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaPrime A K L Q E).IsPrime :=
  Ideal.IsPrime.comap (finiteLevelInertiaSubalgebraInclusion A K L Q E)
Lean source · full declaration
def finiteLevelInertiaLocalizationDiagram :
    FiniteGaloisIntermediateField K L ⥤ AlgCat.{w} A where
  obj E := primeLocalizationAlgCat A (finiteLevelInertiaSubalgebra A K L Q E)
    (finiteLevelInertiaPrime A K L Q E)
  map f := AlgCat.ofHom (finiteLevelInertiaLocalizationMap A K L Q f.le)
  map_id E := by
    apply AlgCat.hom_ext
    apply AlgHom.ext
    intro z
    exact congrArg
      (fun f : Localization.AtPrime (finiteLevelInertiaPrime A K L Q E) →+*
        Localization.AtPrime (finiteLevelInertiaPrime A K L Q E) => f z)
      (Localization.localRingHom_id (finiteLevelInertiaPrime A K L Q E))
  map_comp {E F G} f g := by
    apply AlgCat.hom_ext
    apply AlgHom.ext
    intro z
    exact congrArg
      (fun h : Localization.AtPrime (finiteLevelInertiaPrime A K L Q E) →+*
        Localization.AtPrime (finiteLevelInertiaPrime A K L Q G) => h z)
      (Localization.localRingHom_comp (finiteLevelInertiaPrime A K L Q E)
        (finiteLevelInertiaPrime A K L Q F) (finiteLevelInertiaPrime A K L Q G)
        (finiteLevelInertiaSubalgebraMap A K L Q f.le).toRingHom (by ext b; rfl)
        (finiteLevelInertiaSubalgebraMap A K L Q g.le).toRingHom (by ext b; rfl))
def

finiteLevelInertiaLocalizationCocone

L135 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaLocalizationCocone
Documentation

The cocone consists of the native maps to the actual upper local ring.

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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
local instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime :=
  Ideal.IsPrime.comap (FixedPoints.subalgebra A C (Q.inertia Gal(L/K))).val
local instance finiteLevelInertiaPrime_isPrime (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaPrime A K L Q E).IsPrime :=
  Ideal.IsPrime.comap (finiteLevelInertiaSubalgebraInclusion A K L Q E)
Lean source · full declaration
def finiteLevelInertiaLocalizationCocone :
    Cocone (finiteLevelInertiaLocalizationDiagram A K L Q) where
  pt := primeLocalizationAlgCat A CI (inertiaInvariantPrime A K L Q)
  ι.app E := AlgCat.ofHom (finiteLevelInertiaLocalizationInclusion A K L Q E)
  ι.naturality E F f := by
    apply AlgCat.hom_ext
    apply AlgHom.ext
    intro z
    exact congrArg
      (fun h : Localization.AtPrime (finiteLevelInertiaPrime A K L Q E) →+*
        Localization.AtPrime (inertiaInvariantPrime A K L Q) => h z)
      (Localization.localRingHom_comp (finiteLevelInertiaPrime A K L Q E)
        (finiteLevelInertiaPrime A K L Q F) (inertiaInvariantPrime A K L Q)
        (finiteLevelInertiaSubalgebraMap A K L Q f.le).toRingHom (by ext b; rfl)
        (finiteLevelInertiaSubalgebraInclusion A K L Q F).toRingHom rfl).symm
theorem

finiteLevelInertiaSubalgebraInclusion_injective

L154 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaSubalgebraInclusion_injective
Documentation

The literal finite invariant-stage inclusion is injective, as witnessed by its underlying inclusion into the ambient Galois field.

Source context 11 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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
local instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime :=
  Ideal.IsPrime.comap (FixedPoints.subalgebra A C (Q.inertia Gal(L/K))).val
local instance finiteLevelInertiaPrime_isPrime (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaPrime A K L Q E).IsPrime :=
  Ideal.IsPrime.comap (finiteLevelInertiaSubalgebraInclusion A K L Q E)
omit hQ in
Lean source · statement
theorem finiteLevelInertiaSubalgebraInclusion_injective (E : FiniteGaloisIntermediateField K L) :
    Function.Injective (finiteLevelInertiaSubalgebraInclusion A K L Q E)
theorem

finiteLevelInertiaLocalizationInclusion_injective

L162 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaLocalizationInclusion_injective
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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
local instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime :=
  Ideal.IsPrime.comap (FixedPoints.subalgebra A C (Q.inertia Gal(L/K))).val
local instance finiteLevelInertiaPrime_isPrime (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaPrime A K L Q E).IsPrime :=
  Ideal.IsPrime.comap (finiteLevelInertiaSubalgebraInclusion A K L Q E)
Lean source · statement
theorem finiteLevelInertiaLocalizationInclusion_injective
    (E : FiniteGaloisIntermediateField K L) :
    Function.Injective
      ((finiteLevelInertiaLocalizationInclusion A K L Q E).toRingHom :
        Localization.AtPrime (finiteLevelInertiaPrime A K L Q E) →+*
          Localization.AtPrime (inertiaInvariantPrime A K L Q))
def

finiteLevelInertiaLocalizationCoconeIsColimit

L181 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaLocalizationCoconeIsColimit
Documentation

The localization of the upper inertia invariants is the actual filtered colimit of the localizations of its finite invariant stages. The denominator belongs to a finite stage simultaneously with the numerator and stays outside its contracted prime by the literal inclusion equation.

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
  normalizationInertiaCoefficientCommClass
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]
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))
local instance inertiaInvariantPrime_isPrime : (inertiaInvariantPrime A K L Q).IsPrime :=
  Ideal.IsPrime.comap (FixedPoints.subalgebra A C (Q.inertia Gal(L/K))).val
local instance finiteLevelInertiaPrime_isPrime (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaPrime A K L Q E).IsPrime :=
  Ideal.IsPrime.comap (finiteLevelInertiaSubalgebraInclusion A K L Q E)
Lean source · statement
def finiteLevelInertiaLocalizationCoconeIsColimit :
    IsColimit (finiteLevelInertiaLocalizationCocone 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.