NYLL
Module

ActualFiniteInertiaTowerRestriction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteInertiaTowerRestriction
5 declarations indexed from sourceView source ↗

Module documentation

Actual finite inertia restrictions

The actual surjective original-inertia maps and their proved kernel inclusion construct the canonical restriction between finite intrinsic inertia groups. Its computation law proves surjectivity and finite tower composition.

Imports9
Imported by5

Declarations

def

actualFiniteInertiaTowerRestriction

L41 ↗
EtaleFundamentalGroups.Inertia.actualFiniteInertiaTowerRestriction
Documentation

Restriction between the SAME intrinsic finite normalization inertia groups. The larger actual original-inertia restriction supplies the surjection used in the construction; its kernel inclusion is proved from coefficient maps.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 · full declaration
def actualFiniteInertiaTowerRestriction
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    GrpCat.Hom
      (commAlgIdealInertiaGroup A (finiteAbsoluteNormalizationAlgebra A K L F)
        (finiteAbsoluteNormalizationPrime A K L Q F))
      (commAlgIdealInertiaGroup A (finiteAbsoluteNormalizationAlgebra A K L E)
        (finiteAbsoluteNormalizationPrime A K L Q E)) where
  hom' := (actualFiniteInertiaRestriction A K L Q F).hom'.liftOfSurjective
    (actualFiniteInertiaRestriction_surjective (hQ := hQ) A K L Q F)
    ⟨(actualFiniteInertiaRestriction A K L Q E).hom',
      actualFiniteInertiaRestriction_ker_le_of_tower A K L Q E F h⟩
theorem

actualFiniteInertiaTowerRestriction_comp

L55 ↗
EtaleFundamentalGroups.Inertia.actualFiniteInertiaTowerRestriction_comp
Documentation

The finite restriction factors the actual original-inertia restriction.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualFiniteInertiaTowerRestriction_comp
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    (actualFiniteInertiaTowerRestriction A K L Q E F h).hom'.comp
        (actualFiniteInertiaRestriction A K L Q F).hom' =
      (actualFiniteInertiaRestriction A K L Q E).hom'
theorem

actualFiniteInertiaTowerRestriction_apply_restriction

L70 ↗
EtaleFundamentalGroups.Inertia.actualFiniteInertiaTowerRestriction_apply_restriction
Documentation

Computation of the finite restriction on an actual original inertia lift.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualFiniteInertiaTowerRestriction_apply_restriction
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    (actualFiniteInertiaTowerRestriction A K L Q E F h).hom'.toFun
        ((actualFiniteInertiaRestriction A K L Q F).hom'.toFun σ) =
      (actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ
theorem

actualFiniteInertiaTowerRestriction_surjective

L81 ↗
EtaleFundamentalGroups.Inertia.actualFiniteInertiaTowerRestriction_surjective
Documentation

The actual restriction between finite intrinsic inertia groups is onto.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualFiniteInertiaTowerRestriction_surjective
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    Function.Surjective (actualFiniteInertiaTowerRestriction A K L Q E F h).hom'.toFun
theorem

actualFiniteInertiaTowerRestriction_trans

L93 ↗
EtaleFundamentalGroups.Inertia.actualFiniteInertiaTowerRestriction_trans
Documentation

Restriction through a common larger finite stage agrees with direct restriction. Both maps are tested on actual original inertia lifts.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualFiniteInertiaTowerRestriction_trans
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F H : FiniteGaloisIntermediateField K L) (hEF : E ≤ F) (hFH : F ≤ H) :
    (actualFiniteInertiaTowerRestriction A K L Q E F hEF).hom'.comp
        (actualFiniteInertiaTowerRestriction A K L Q F H hFH).hom' =
      (actualFiniteInertiaTowerRestriction A K L Q E H (hEF.trans hFH)).hom'

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