Module

OriginalNormalizationInertiaAction.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalNormalizationInertiaAction

4 declarations indexed from sourceView source ↗

Module documentation

Original Galois inertia on the normalization

Identifies the native normalization ring map with the original Galois action. Defines the original inertia group and derives its coefficient difference condition.

Imports4

Nyll.SchemeTheory.Normalization.AmbientNormalizationGroupMap
Nyll.SchemeTheory.Normalization.SubalgebraPreimage
Nyll.SchemeTheory.RingTheory.Ramification.FiniteLevelInertiaImage
Mathlib.Algebra.Category.Grp.Basic

Imported by38

theorem

normalizationGaloisRingHom_eq_original

L36 ↗

EtaleFundamentalGroups.Inertia.normalizationGaloisRingHom_eq_original

Documentation

The individual native normalization map is the original ramification action, as proved by their common injective coefficient inclusion.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
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 normalizationGaloisRingHom_eq_original (σ : Gal(L/K)) :
    normalizationGaloisRingHom A K L σ =
      MulSemiringAction.toRingHom Gal(L/K) (normalizationCommAlgCat A L).carrier σ

def

actualNormalizationInertiaGroup

L45 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationInertiaGroup

Documentation

The actual original ideal inertia, with its original Galois action.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
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 actualNormalizationInertiaGroup
    (Q : Ideal (normalizationCommAlgCat A L).carrier) : GrpCat.{w}

def

actualNormalizationInertiaElement

L50 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationInertiaElement

Documentation

The original automorphism underlying an actual ideal-inertia element.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
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 actualNormalizationInertiaElement (Q : Ideal (normalizationCommAlgCat A L).carrier)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) : Gal(L/K)

theorem

actualNormalizationInertia_difference

L55 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationInertia_difference

Documentation

Actual original ideal inertia gives the literal difference predicate for the canonically constructed normalization automorphism.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
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 actualNormalizationInertia_difference (Q : Ideal (normalizationCommAlgCat A L).carrier)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    ∀ b : (normalizationCommAlgCat A L).carrier,
      Sub.sub (α := (normalizationCommAlgCat A L).carrier)
        ((normalizationGaloisRingHom A K L (actualNormalizationInertiaElement A K L Q σ) :
          (normalizationCommAlgCat A L).carrier →+*
            (normalizationCommAlgCat A L).carrier).toFun b) b ∈ Q

Module documentation

Original Galois inertia on the normalization

Declarations

normalizationGaloisRingHom_eq_original

actualNormalizationInertiaGroup

actualNormalizationInertiaElement

actualNormalizationInertia_difference