Module

NormalizationPrimeInertia.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeInertia

5 declarations indexed from sourceView source ↗

Module documentation

Original normalization inertia on the literal prime localization

Use the already fixed integral-closure Galois action and its existing scalar commutation owner. An element of the original ideal inertia therefore gives the individual native localization automorphism, with the literal base and residue squares. No alternate action on the localization is installed. These are the actual inputs for the separately proved stalk rigidity result.

Imports5

Imported by4

def

normalizationCoefficientMap

L33 ↗

EtaleFundamentalGroups.StrictHenselian.normalizationCoefficientMap

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaCoefficientCommClass

Lean source · statement

def normalizationCoefficientMap
    (A : Type u) (L : Type w) [CommRing A] [Field L] [Algebra A L] :
    A →+* integralClosure A L

theorem

normalizationCoefficientMap_commutes

L43 ↗

EtaleFundamentalGroups.StrictHenselian.normalizationCoefficientMap_commutes

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
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]

Lean source · statement

theorem normalizationCoefficientMap_commutes (σ : Gal(L/K)) :
    (MulSemiringAction.toRingEquiv Gal(L/K) (integralClosure A L) σ).toRingHom.comp
        (normalizationCoefficientMap A L) = normalizationCoefficientMap A L

def

normalizationPrimeInertiaRingEquiv

L52 ↗

EtaleFundamentalGroups.StrictHenselian.normalizationPrimeInertiaRingEquiv

Documentation

An element of the original normalization-prime inertia acts on the literal localization, through the existing canonical normalization action.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
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]

Lean source · statement

def normalizationPrimeInertiaRingEquiv
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    (σ : Gal(L/K)) (hσ : σ ∈ Q.inertia Gal(L/K)) :
    Localization.AtPrime Q ≃+* Localization.AtPrime Q

theorem

normalizationPrimeInertiaRingEquiv_comp_baseMap

L61 ↗

EtaleFundamentalGroups.StrictHenselian.normalizationPrimeInertiaRingEquiv_comp_baseMap

Documentation

The original normalization inertia preserves the literal composite from the base into the prime localization.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
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]

Lean source · statement

theorem normalizationPrimeInertiaRingEquiv_comp_baseMap
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    (σ : Gal(L/K)) (hσ : σ ∈ Q.inertia Gal(L/K)) :
    (normalizationPrimeInertiaRingEquiv A K L Q σ hσ).toRingHom.comp
        (integralClosurePrimeBaseMap A L Q) = integralClosurePrimeBaseMap A L Q

theorem

normalizationPrimeInertiaRingEquiv_comp_residue

L72 ↗

EtaleFundamentalGroups.StrictHenselian.normalizationPrimeInertiaRingEquiv_comp_residue

Documentation

The original normalization inertia acts trivially on the actual residue field of the literal prime localization.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
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]

Lean source · statement

theorem normalizationPrimeInertiaRingEquiv_comp_residue
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    (σ : Gal(L/K)) (hσ : σ ∈ Q.inertia Gal(L/K)) :
    (IsLocalRing.residue (Localization.AtPrime Q)).comp
        (normalizationPrimeInertiaRingEquiv A K L Q σ hσ).toRingHom =
      IsLocalRing.residue (Localization.AtPrime Q)

Module documentation

Original normalization inertia on the literal prime localization

Declarations

normalizationCoefficientMap

normalizationCoefficientMap_commutes

normalizationPrimeInertiaRingEquiv

normalizationPrimeInertiaRingEquiv_comp_baseMap

normalizationPrimeInertiaRingEquiv_comp_residue