Module

ActualFiniteWildRestriction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteWildRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Surjective actual finite wild restrictions

The induced map uses the literal actual inertia restriction. Its image equality was proved from the original data, so preservation and surjectivity are conclusions, with no comparison premise supplied by a caller.

Imports6

Imported by1

Nyll.EtaleFundamentalGroups.Inertia.All

def

actualFiniteWildTowerRestriction

L38 ↗

EtaleFundamentalGroups.Inertia.actualFiniteWildTowerRestriction

Documentation

The actual induced restriction on the SAME intrinsic finite wild groups.

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] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]
  (E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)

Lean source · full declaration

def actualFiniteWildTowerRestriction :
    GrpCat.Hom (actualFiniteWildGroup A K L Q F) (actualFiniteWildGroup A K L Q E) where
  hom' := subgroupRestrictionOfImage
    (actualFiniteInertiaTowerRestriction A K L Q E F hEF).hom'
    (actualFiniteWildSubgroup A K L Q F) (actualFiniteWildSubgroup A K L Q E)
    (actualFiniteWildSubgroup_map A K L Q E F hEF)

theorem

actualFiniteWildTowerRestriction_val

L46 ↗

EtaleFundamentalGroups.Inertia.actualFiniteWildTowerRestriction_val

Documentation

On its underlying inertia element this is precisely the actual rho.

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] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]
  (E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)

Lean source · statement

theorem actualFiniteWildTowerRestriction_val
    (sigma : (actualFiniteWildGroup A K L Q F).carrier) :
    ((actualFiniteWildTowerRestriction A K L Q E F hEF).hom'.toFun sigma).val =
      (actualFiniteInertiaTowerRestriction A K L Q E F hEF).hom'.toFun sigma.val

theorem

actualFiniteWildTowerRestriction_surjective

L56 ↗

EtaleFundamentalGroups.Inertia.actualFiniteWildTowerRestriction_surjective

Documentation

The same induced actual wild restriction is surjective.

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] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]
  (E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)

Lean source · statement

theorem actualFiniteWildTowerRestriction_surjective :
    Function.Surjective (actualFiniteWildTowerRestriction A K L Q E F hEF).hom'.toFun

Module documentation

Surjective actual finite wild restrictions

Declarations

actualFiniteWildTowerRestriction

actualFiniteWildTowerRestriction_val

actualFiniteWildTowerRestriction_surjective