NYLL
Module

ActualNormalizationWildGroup.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationWildGroup
4 declarations indexed from sourceView source ↗

Module documentation

Native group owners for original and finite wild inertia

The maps are the restrictions of the already constructed original inertia maps to the independently defined subgroups. Their joint faithfulness is inherited from actual finite inertia separation.

Imports7
Imported by3

Declarations

def

actualNormalizationWildGroup

L38 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildGroup
Documentation

The SAME independent original wild subgroup as a native group object.

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]
Lean source · statement
def actualNormalizationWildGroup : GrpCat.{w}
def

actualFiniteWildFiniteGroup

L44 ↗
EtaleFundamentalGroups.Inertia.actualFiniteWildFiniteGroup
Documentation

The actual finite wild group with its proved finiteness.

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]
Lean source · statement
def actualFiniteWildFiniteGroup (E : FiniteGaloisIntermediateField K L) : FiniteGrp.{w}
def

actualNormalizationWildRestriction

L55 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildRestriction
Documentation

The literal finite restriction on the independently defined global wild group.

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]
Lean source · full declaration
def actualNormalizationWildRestriction (E : FiniteGaloisIntermediateField K L) :
    GrpCat.Hom (actualNormalizationWildGroup A K L Q) (actualFiniteWildGroup A K L Q E) where
  hom' :=
    { toFun := fun σ =>
        ⟨(actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ.val,
          (mem_actualNormalizationWildSubgroup A K L Q σ.val).mp σ.property E⟩
      map_one' := Subtype.ext (actualFiniteInertiaRestriction A K L Q E).hom'.map_one
      map_mul' := fun σ τ => Subtype.ext
        ((actualFiniteInertiaRestriction A K L Q E).hom'.map_mul σ.val τ.val) }
theorem

actualNormalizationWildRestriction_jointly_injective

L66 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildRestriction_jointly_injective
Documentation

The actual wild restrictions jointly determine an original wild element.

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]
Lean source · statement
theorem actualNormalizationWildRestriction_jointly_injective
    (σ τ : (actualNormalizationWildGroup A K L Q).carrier)
    (h : ∀ E : FiniteGaloisIntermediateField K L,
      (actualNormalizationWildRestriction A K L Q E).hom'.toFun σ =
        (actualNormalizationWildRestriction A K L Q E).hom'.toFun τ) : σ = τ

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