Module

ActualFiniteWildSubgroup.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteWildSubgroup

6 declarations indexed from sourceView source ↗

Module documentation

The actual intrinsic finite wild subgroup and group

The original DVR, Galois extension and chosen prime supply the same native principal-unit subgroup at every finite stage. Its cardinality and index remain the previously constructed wild and tame orders.

Imports10

Imported by9

def

actualFiniteWildSubgroup

L41 ↗

EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup

Documentation

The actual intrinsic wild subgroup at a finite Galois stage.

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 actualFiniteWildSubgroup (E : FiniteGaloisIntermediateField K L) :
    Subgroup (actualFiniteStageInertiaGroup A K L Q E).carrier

def

actualFiniteWildGroup

L52 ↗

EtaleFundamentalGroups.Inertia.actualFiniteWildGroup

Documentation

The same subgroup as a native group object, for its induced restrictions.

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 actualFiniteWildGroup (E : FiniteGaloisIntermediateField K L) : GrpCat.{w}

theorem

actualFiniteWildSubgroup_card

L56 ↗

EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_card

Documentation

Cardinality of the same subgroup is its existing actual wild order.

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 actualFiniteWildSubgroup_card (E : FiniteGaloisIntermediateField K L) :
    Nat.card (actualFiniteWildSubgroup A K L Q E) = actualFiniteStageWildOrder A K L Q E

theorem

actualFiniteWildSubgroup_index

L67 ↗

EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_index

Documentation

The same subgroup's index is the existing actual tame order.

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 actualFiniteWildSubgroup_index (E : FiniteGaloisIntermediateField K L) :
    (actualFiniteWildSubgroup A K L Q E).index = actualFiniteStageTameOrder A K L Q E

theorem

actualFiniteStageInertiaGroup_finite

L79 ↗

EtaleFundamentalGroups.Inertia.actualFiniteStageInertiaGroup_finite

Documentation

Its intrinsic ambient inertia group is finite.

Source context 6 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]
omit [Q.IsMaximal] in

Lean source · statement

theorem actualFiniteStageInertiaGroup_finite (E : FiniteGaloisIntermediateField K L) :
    Finite (actualFiniteStageInertiaGroup A K L Q E).carrier

theorem

actualFiniteWildSubgroup_normal

L88 ↗

EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_normal

Documentation

The same actual finite wild subgroup is normal in intrinsic finite inertia.

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 actualFiniteWildSubgroup_normal (E : FiniteGaloisIntermediateField K L) :
    (actualFiniteWildSubgroup A K L Q E).Normal

Module documentation

The actual intrinsic finite wild subgroup and group

Declarations

actualFiniteWildSubgroup

actualFiniteWildGroup

actualFiniteWildSubgroup_card

actualFiniteWildSubgroup_index

actualFiniteStageInertiaGroup_finite

actualFiniteWildSubgroup_normal