Module

ActualTameCoordinate.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCoordinate

2 declarations indexed from sourceView source ↗

Module documentation

Canonical tame coordinates indexed by the actual degrees

At an actual degree, choose a finite stage realizing that degree and apply the existing canonical e/n character. Its value is transported through the existing maximal-quotient residue equivalence. The evaluation theorem proves independence from the realizing stage.

Imports4

Imported by5

def

actualTameCoordinate

L38 ↗

EtaleFundamentalGroups.Inertia.actualTameCoordinate

Documentation

The actual quotient-valued coordinate at an actual tame degree.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
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 · statement

def actualTameCoordinate (n : Subtype (actualFiniteTameDegreeSet A K L Q)) :
    (actualNormalizationInertiaGroup A K L Q).carrier →*
      rootsOfUnity n.val.val ((normalizationCommAlgCat A L).carrier ⧸ Q)

theorem

actualTameCoordinate_eval

L47 ↗

EtaleFundamentalGroups.Inertia.actualTameCoordinate_eval