Module

PrimeToRootsResidueAction.lean

Nyll.EtaleFundamentalGroups.Inertia.PrimeToRootsResidueAction

6 declarations indexed from sourceView source ↗

Module documentation

The literal coefficient action on the full roots limit

Every coordinate is sent through the specified ring map. Compatibility is the proved coefficient/power transition square, and continuity follows from the existing inverse-limit topology and discrete root stages.

Imports4

Nyll.ProCGroups.InverseSystems.Basic
Nyll.EtaleFundamentalGroups.Inertia.PrimeToRootsInverseSystem
Mathlib.GroupTheory.Perm.Basic
Mathlib.Topology.Constructions

Imported by2

def

primeToRootsCoefficientMap

L29 ↗

EtaleFundamentalGroups.Inertia.primeToRootsCoefficientMap

Documentation

Apply the same ring map at every full roots coordinate.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v
variable (k : Type u) (E : Type v) [Field k] [Field E]

Lean source · statement

def primeToRootsCoefficientMap (f : E →+* E) :
    (primeToRootsSystem k E).inverseLimit →
      (primeToRootsSystem k E).inverseLimit

theorem

primeToRootsCoefficientMap_scalar

L38 ↗

EtaleFundamentalGroups.Inertia.primeToRootsCoefficientMap_scalar

Documentation

Literal scalar evaluation of the coefficient map.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v
variable (k : Type u) (E : Type v) [Field k] [Field E]

Lean source · statement

theorem primeToRootsCoefficientMap_scalar (f : E →+* E)
    (n : InvertibleExponent k) (x : (primeToRootsSystem k E).inverseLimit) :
    ((primeToRootsSystem k E).projection n
      (primeToRootsCoefficientMap k E f x)).val.val =
      f.toFun (((primeToRootsSystem k E).projection n x).val.val)

theorem

primeToRootsCoefficientMap_continuous

L45 ↗

EtaleFundamentalGroups.Inertia.primeToRootsCoefficientMap_continuous

Documentation

The coordinatewise map is continuous in the original limit topology.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v
variable (k : Type u) (E : Type v) [Field k] [Field E]

Lean source · statement

theorem primeToRootsCoefficientMap_continuous (f : E →+* E) :
    Continuous (primeToRootsCoefficientMap k E f)

def

primeToRootsResidueEquiv

L65 ↗

EtaleFundamentalGroups.Inertia.primeToRootsResidueEquiv

Documentation

A coefficient automorphism and its inverse act coordinatewise.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v
variable (k : Type u) (E : Type v) [Field k] [Field E]

Lean source · full declaration

def primeToRootsResidueEquiv (f : E ≃+* E) :
    Equiv.Perm (primeToRootsSystem k E).inverseLimit where
  toFun := primeToRootsCoefficientMap k E f.toRingHom
  invFun := primeToRootsCoefficientMap k E f.symm.toRingHom
  left_inv x := by
    apply (primeToRootsSystem k E).ext
    intro n
    apply rootsOfUnity.coe_injective
    exact f.symm_apply_apply (x.val n).val.val
  right_inv x := by
    apply (primeToRootsSystem k E).ext
    intro n
    apply rootsOfUnity.coe_injective
    exact f.apply_symm_apply (x.val n).val.val

def