Module

ActualTameCharacterKernel.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacterKernel

1 declaration indexed from sourceView source ↗

Module documentation

The SAME canonical global tame character has the independent wild kernel

Both sides are evaluated through their already proved actual finite coordinates. No kernel or comparison assertion is an input.

Imports6

Imported by4

theorem

actualTameCharacter_ker

L29 ↗

EtaleFundamentalGroups.Inertia.actualTameCharacter_ker

Documentation

The kernel of the canonical root-limit character is precisely the original subgroup defined by all finite principal-unit conditions.

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 actualTameCharacter_ker
    (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] :
    (actualTameCharacter A K L Q).ker = actualNormalizationWildSubgroup A K L Q

Module documentation

The SAME canonical global tame character has the independent wild kernel

Declarations

actualTameCharacter_ker