NYLL
Module

InvariantPrimeLocalizationMap.lean

Nyll.EtaleFundamentalGroups.Inertia.InvariantPrimeLocalizationMap
7 declarations indexed from sourceView source ↗

Module documentation

The literal inertia-invariant prime localization maps to the normalization

The fixed subalgebra is computed using the original normalization inertia action. Its contracted-prime localization and native map to the normalization prime localization are the already constructed generic objects and RingHoms. The proved generic coefficient square gives the original base square directly.

The source computes the same actual localization used in 0BSU: the prime is the comap of Q under the inclusion of its original inertia-fixed subalgebra. No invariant/stalk comparison, alternate action, or compatibility premise is introduced. The finite-stage image and whole invariant-image results remain separate.

Imports9
Imported by4

Declarations

def

normalizationInertiaFixedSubalgebra

L50 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedSubalgebra
Documentation

The existing actual fixed subalgebra, with its original canonical normalization action. This closes its action data before taking localizations.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory EtaleFundamentalGroups.StrictHenselian
universe u v w
attribute [local instance] normalizationInertiaImageAction 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))
Lean source · statement
def normalizationInertiaFixedSubalgebra : Subalgebra A (integralClosure A L)
def

inertiaInvariantPrimeLocalization

L57 ↗
EtaleFundamentalGroups.Inertia.inertiaInvariantPrimeLocalization
Documentation

The literal localization of the original inertia-fixed subalgebra at the contraction of Q, with its native commutative ring.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory EtaleFundamentalGroups.StrictHenselian
universe u v w
attribute [local instance] normalizationInertiaImageAction 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))
variable [Q.IsPrime]
Lean source · statement
def inertiaInvariantPrimeLocalization : CommRingCat.{w}
def

inertiaInvariantPrimeLocalizationMap

L62 ↗
EtaleFundamentalGroups.Inertia.inertiaInvariantPrimeLocalizationMap
Documentation

The actual native localized inclusion into the original normalization prime localization.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory EtaleFundamentalGroups.StrictHenselian
universe u v w
attribute [local instance] normalizationInertiaImageAction 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))
variable [Q.IsPrime]
Lean source · statement
def inertiaInvariantPrimeLocalizationMap :
    inertiaInvariantPrimeLocalization A K L Q →+* Localization.AtPrime Q
def

inertiaInvariantPrimeLocalizationBaseMap

L68 ↗
EtaleFundamentalGroups.Inertia.inertiaInvariantPrimeLocalizationBaseMap
Documentation

The original base map to the actual inertia-invariant localization, computed through its genuine coefficient inclusion.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory EtaleFundamentalGroups.StrictHenselian
universe u v w
attribute [local instance] normalizationInertiaImageAction 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))
variable [Q.IsPrime]
Lean source · statement
def inertiaInvariantPrimeLocalizationBaseMap :
    A →+* inertiaInvariantPrimeLocalization A K L Q
theorem

inertiaInvariantPrimeLocalizationMap_comp_base

L74 ↗
EtaleFundamentalGroups.Inertia.inertiaInvariantPrimeLocalizationMap_comp_base
Documentation

The native localized invariant inclusion extends precisely the original base map to the normalization prime localization.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory EtaleFundamentalGroups.StrictHenselian
universe u v w
attribute [local instance] normalizationInertiaImageAction 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))
variable [Q.IsPrime]
Lean source · statement
theorem inertiaInvariantPrimeLocalizationMap_comp_base :
    (inertiaInvariantPrimeLocalizationMap A K L Q).comp
        (inertiaInvariantPrimeLocalizationBaseMap A K L Q) =
      integralClosurePrimeBaseMap A L Q
def

inertiaInvariantPrimeLocalizationAlgebra

L83 ↗
EtaleFundamentalGroups.Inertia.inertiaInvariantPrimeLocalizationAlgebra
Documentation

The actual invariant localization with the same native algebra used by its finite-level coefficient maps.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory EtaleFundamentalGroups.StrictHenselian
universe u v w
attribute [local instance] normalizationInertiaImageAction 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))
variable [Q.IsPrime]
Lean source · statement
def inertiaInvariantPrimeLocalizationAlgebra : CommAlgCat.{w} A
theorem

inertiaInvariantPrimeLocalizationBaseMap_eq_algebraMap

L88 ↗
EtaleFundamentalGroups.Inertia.inertiaInvariantPrimeLocalizationBaseMap_eq_algebraMap
Documentation

The previously constructed base RingHom is exactly the native algebra map on the actual invariant localization.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory EtaleFundamentalGroups.StrictHenselian
universe u v w
attribute [local instance] normalizationInertiaImageAction 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))
variable [Q.IsPrime]
Lean source · statement
theorem inertiaInvariantPrimeLocalizationBaseMap_eq_algebraMap :
    (inertiaInvariantPrimeLocalizationBaseMap A K L Q :
        A →+* inertiaInvariantPrimeLocalizationAlgebra A K L Q) =
      algebraMap A (inertiaInvariantPrimeLocalizationAlgebra 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.