Module

CommAlgCanonicalTameCharacter.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgCanonicalTameCharacter

1 declaration indexed from sourceView source ↗

Module documentation

Canonical tame characters of coefficient algebras

Constructs the canonical finite tame character on intrinsic coefficient inertia with values in its full residue-root group.

Imports3

Imported by6

def

commAlgCanonicalTameCharacter

L27 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalTameCharacter

Documentation

The same canonical finite character on native coefficient inertia and its actual full residue-root group. This closes the localization action before the original field tower is introduced.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

def commAlgCanonicalTameCharacter (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥) :
    commAlgIdealInertiaGroup A B Q →* commAlgIdealTameRootsGroup A B Q hQ

Module documentation

Canonical tame characters of coefficient algebras

Declarations

commAlgCanonicalTameCharacter