NYLL
Module

ActualFiniteDecompositionTowerRestriction.lean

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

Module documentation

Actual finite decomposition restrictions

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

Imports9
Imported by2

Declarations

def

actualFiniteDecompositionTowerRestriction

L41 ↗
EtaleFundamentalGroups.Inertia.actualFiniteDecompositionTowerRestriction
Documentation

Restriction between the SAME intrinsic finite normalization decomposition groups. The larger actual original-decomposition 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 actualFiniteDecompositionTowerRestriction
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    GrpCat.Hom
      (commAlgIdealDecompositionGroup A (finiteAbsoluteNormalizationAlgebra A K L F)
        (finiteAbsoluteNormalizationPrime A K L Q F))
      (commAlgIdealDecompositionGroup A (finiteAbsoluteNormalizationAlgebra A K L E)
        (finiteAbsoluteNormalizationPrime A K L Q E)) where
  hom' := (actualFiniteDecompositionRestriction A K L Q F).hom'.liftOfSurjective
    (actualFiniteDecompositionRestriction_surjective (hQ := hQ) A K L Q F)
    ⟨(actualFiniteDecompositionRestriction A K L Q E).hom',
      actualFiniteDecompositionRestriction_ker_le_of_tower A K L Q E F h⟩
theorem

actualFiniteDecompositionTowerRestriction_comp

L55 ↗
EtaleFundamentalGroups.Inertia.actualFiniteDecompositionTowerRestriction_comp
Documentation

The finite restriction factors the actual original-decomposition 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 actualFiniteDecompositionTowerRestriction_comp
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    (actualFiniteDecompositionTowerRestriction A K L Q E F h).hom'.comp
        (actualFiniteDecompositionRestriction A K L Q F).hom' =
      (actualFiniteDecompositionRestriction A K L Q E).hom'
theorem

actualFiniteDecompositionTowerRestriction_apply_restriction

L70 ↗
EtaleFundamentalGroups.Inertia.actualFiniteDecompositionTowerRestriction_apply_restriction
Documentation

Computation of the finite restriction on an actual original decomposition 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 actualFiniteDecompositionTowerRestriction_apply_restriction
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F)
    (σ : (normalizationDecompositionGroup A K L Q).carrier) :
    (actualFiniteDecompositionTowerRestriction A K L Q E F h).hom'.toFun
        ((actualFiniteDecompositionRestriction A K L Q F).hom'.toFun σ) =
      (actualFiniteDecompositionRestriction A K L Q E).hom'.toFun σ
theorem

actualFiniteDecompositionTowerRestriction_surjective

L81 ↗
EtaleFundamentalGroups.Inertia.actualFiniteDecompositionTowerRestriction_surjective
Documentation

The actual restriction between finite intrinsic decomposition 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 actualFiniteDecompositionTowerRestriction_surjective
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    Function.Surjective (actualFiniteDecompositionTowerRestriction A K L Q E F h).hom'.toFun
theorem

actualFiniteDecompositionTowerRestriction_trans

L93 ↗
EtaleFundamentalGroups.Inertia.actualFiniteDecompositionTowerRestriction_trans
Documentation

Restriction through a common larger finite stage agrees with direct restriction. Both maps are tested on actual original decomposition 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 actualFiniteDecompositionTowerRestriction_trans
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E F H : FiniteGaloisIntermediateField K L) (hEF : E ≤ F) (hFH : F ≤ H) :
    (actualFiniteDecompositionTowerRestriction A K L Q E F hEF).hom'.comp
        (actualFiniteDecompositionTowerRestriction A K L Q F H hFH).hom' =
      (actualFiniteDecompositionTowerRestriction 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.