Module

ActualNormalizationWildProP.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationWildProP

1 declaration indexed from sourceView source ↗

Module documentation

The independently defined original wild group is pro-p

Its actual finite wild coordinates are p-groups, locally constant and jointly faithful. Closed-product permanence for pro-p groups therefore applies to the SAME original wild subgroup in its inherited topology.

Imports7

Imported by3

theorem

actualNormalizationWildGroup_hasPGroupOpenNormalBasis

L31 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationWildGroup_hasPGroupOpenNormalBasis

Documentation

Original wild inertia has a basis of open normal subgroups with finite p-group quotients in positive characteristic of the original base residue field.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w

Lean source · statement

theorem actualNormalizationWildGroup_hasPGroupOpenNormalBasis
    (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]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p] :
    ProCGroups.ProC.HasPGroupOpenNormalBasis p (actualNormalizationWildGroup A K L Q).carrier

Module documentation

The independently defined original wild group is pro-p

Declarations

actualNormalizationWildGroup_hasPGroupOpenNormalBasis