NYLL
Module

ActualNormalizationWildSubgroup.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationWildSubgroup
3 declarations indexed from sourceView source ↗

Module documentation

Wild inertia of the original normalization

An original inertia element is wild exactly when all its actual finite restrictions are in the existing principal-unit wild subgroups. This construction does not use the tame character or a kernel definition.

Imports6
Imported by10

Declarations

def

actualNormalizationWildSubgroup

L38 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildSubgroup
Documentation

The original wild subgroup, independently defined by all actual finite principal-unit conditions.

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 actualNormalizationWildSubgroup :
    Subgroup (actualNormalizationInertiaGroup A K L Q).carrier
theorem

mem_actualNormalizationWildSubgroup

L45 ↗
EtaleFundamentalGroups.Inertia.mem_actualNormalizationWildSubgroup
Documentation

Membership is the literal family of finite wild conditions.

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 mem_actualNormalizationWildSubgroup
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    σ ∈ actualNormalizationWildSubgroup A K L Q ↔
      ∀ E : FiniteGaloisIntermediateField K L,
        (actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ ∈
          actualFiniteWildSubgroup A K L Q E
theorem

actualNormalizationWildSubgroup_normal

L56 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildSubgroup_normal
Documentation

Normality inside original inertia follows from the actual finite normal subgroups and their literal 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
theorem actualNormalizationWildSubgroup_normal :
    (actualNormalizationWildSubgroup A K L Q).Normal

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