NYLL
Module

OriginalFiniteNormalizationInertia.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteNormalizationInertia
6 declarations indexed from sourceView source ↗

Module documentation

Finite-field and normalization inertia equivalence

Constructs the normalization restriction on original finite-field inertia. Proves injectivity and surjectivity and packages the resulting equivalence with intrinsic normalization inertia.

Imports11
Imported by7

Declarations

def

originalFiniteNormalizationInertiaMorphism

L36 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationInertiaMorphism
Documentation

The original field inertia acts on its actual normalization through the original normalization restriction, with its proved inertia condition.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
Lean source · full declaration
def originalFiniteNormalizationInertiaMorphism
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F).carrier) :
    GrpCat.Hom (actualNormalizationInertiaGroup A K F Q)
      (commAlgIdealInertiaGroup A (normalizationCommAlgCat A F) Q) where
  hom' :=
    { toFun := fun σ =>
        ⟨(normalizationGaloisGroupMap A K F).hom'.toFun
          (actualNormalizationInertiaElement A K F Q σ),
          actualNormalizationInertia_difference A K F Q σ⟩
      map_one' := Subtype.ext (normalizationGaloisGroupMap A K F).hom'.map_one'
      map_mul' := fun σ τ => Subtype.ext
        ((normalizationGaloisGroupMap A K F).hom'.map_mul' σ.val τ.val) }
theorem

originalFiniteNormalizationInertiaMorphism_ringHom

L54 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationInertiaMorphism_ringHom
Documentation

Its coefficient RingHom is exactly the original normalization action.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
Lean source · statement
theorem originalFiniteNormalizationInertiaMorphism_ringHom
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F).carrier)
    (σ : (actualNormalizationInertiaGroup A K F Q).carrier) :
    commAlgIdealInertiaRingHom A (normalizationCommAlgCat A F) Q
        ((originalFiniteNormalizationInertiaMorphism A K F Q).hom'.toFun σ) =
      normalizationGaloisRingHom A K F (actualNormalizationInertiaElement A K F Q σ)
theorem

normalizationGaloisRingHom_injective

L67 ↗
EtaleFundamentalGroups.Inertia.normalizationGaloisRingHom_injective
Documentation

Equality of actual normalization restrictions determines the original finite field automorphism by fraction-field uniqueness.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
Lean source · statement
theorem normalizationGaloisRingHom_injective
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F] :
    Function.Injective (normalizationGaloisRingHom A K F)
theorem

originalFiniteNormalizationInertiaMorphism_surjective

L94 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationInertiaMorphism_surjective
Documentation

The proved finite field lift is a preimage under this actual morphism.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
Lean source · statement
theorem originalFiniteNormalizationInertiaMorphism_surjective
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [IsGalois K F] [FiniteDimensional K F]
    (Q : Ideal (normalizationCommAlgCat A F).carrier) :
    Function.Surjective (originalFiniteNormalizationInertiaMorphism A K F Q).hom'.toFun
theorem

originalFiniteNormalizationInertiaMorphism_injective

L109 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationInertiaMorphism_injective
Documentation

No original finite inertia element is lost on the normalization.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
Lean source · statement
theorem originalFiniteNormalizationInertiaMorphism_injective
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [IsGalois K F] [FiniteDimensional K F]
    (Q : Ideal (normalizationCommAlgCat A F).carrier) :
    Function.Injective (originalFiniteNormalizationInertiaMorphism A K F Q).hom'.toFun
def

originalFiniteNormalizationInertiaEquiv

L127 ↗
EtaleFundamentalGroups.Inertia.originalFiniteNormalizationInertiaEquiv
Documentation

The actual original finite inertia and intrinsic normalization inertia are isomorphic through the prescribed normalization restriction.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w
Lean source · statement
def originalFiniteNormalizationInertiaEquiv
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [IsGalois K F] [FiniteDimensional K F]
    (Q : Ideal (normalizationCommAlgCat A F).carrier) :
    (actualNormalizationInertiaGroup A K F Q).carrier ≃*
      (commAlgIdealInertiaGroup A (normalizationCommAlgCat A F) Q).carrier

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