Module

ActualTameCharacter.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacter

2 declarations indexed from sourceView source ↗

Module documentation

The actual canonical tame character

Constructs the group homomorphism from the original inertia into the literal inverse limit of roots in the original normalization quotient. Evaluation at a degree is the stage-independent actual canonical finite coordinate.

Imports2

Imported by5

def

actualTameCharacter

L35 ↗

EtaleFundamentalGroups.Inertia.actualTameCharacter

Documentation

The canonical character into the SAME literal quotient-root limit.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory ProCGroups.InverseSystems
universe u v w
attribute [local instance] Ideal.Quotient.field
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 · full declaration

def actualTameCharacter :
    (actualNormalizationInertiaGroup A K L Q).carrier →*
      (actualFiniteTameRootsSystem A K L Q).inverseLimit where
  toFun := (actualFiniteTameRootsSystem A K L Q).inverseLimitLift
    (fun n => (actualTameCoordinate A K L Q n).toFun)
    (actualTameCoordinate_compatible A K L Q)
  map_one' := by
    apply (actualFiniteTameRootsSystem A K L Q).ext
    intro n
    exact (actualTameCoordinate A K L Q n).map_one'
  map_mul' σ τ := by
    apply (actualFiniteTameRootsSystem A K L Q).ext
    intro n
    exact (actualTameCoordinate A K L Q n).map_mul' σ τ

theorem

actualTameCharacter_projection

L51 ↗

EtaleFundamentalGroups.Inertia.actualTameCharacter_projection