Module

PrimeToRootsCoefficientComparison.lean

Nyll.EtaleFundamentalGroups.Inertia.PrimeToRootsCoefficientComparison

3 declarations indexed from sourceView source ↗

Module documentation

Ordinary coefficient comparison of roots systems

The supplied map is a field-coefficient map. Bijectivity at finite roots stages is used once to construct the stage equivalences. Their transition square is proved from the actual power-map naturality theorem. No inverse limit comparison or action square is assumed.

Imports3

Nyll.EtaleFundamentalGroups.Inertia.PrimeToRootsInverseSystem
Nyll.ProCGroups.InverseSystems.StagewiseIso
Mathlib.Topology.Order

Imported by2

def

primeToRootsCoefficientLimitMap

L32 ↗

EtaleFundamentalGroups.Inertia.primeToRootsCoefficientLimitMap

Documentation

Apply the same coefficient homomorphism to every compatible root coordinate.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v
variable (k : Type u) (R S : Type v) [Field k] [Field R] [Field S]
  (f : R →* S)

Lean source · statement

def primeToRootsCoefficientLimitMap :
    (primeToRootsSystem k R).inverseLimit → (primeToRootsSystem k S).inverseLimit

theorem

primeToRootsCoefficientLimitMap_scalar

L40 ↗

EtaleFundamentalGroups.Inertia.primeToRootsCoefficientLimitMap_scalar

Documentation

The plain compatible-family map has the literal coefficient scalar at every stage.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v
variable (k : Type u) (R S : Type v) [Field k] [Field R] [Field S]
  (f : R →* S)

Lean source · statement

theorem primeToRootsCoefficientLimitMap_scalar
    (n : InvertibleExponent k) (x : (primeToRootsSystem k R).inverseLimit) :
    ((primeToRootsSystem k S).projection n
      (primeToRootsCoefficientLimitMap k R S f x)).val.val =
      f.toFun (((primeToRootsSystem k R).projection n x).val.val)

def

primeToRootsCoefficientSystemIso

L47 ↗

EtaleFundamentalGroups.Inertia.primeToRootsCoefficientSystemIso

Documentation

Finite-root bijectivity and the proved power square construct a stagewise system isomorphism.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v
variable (k : Type u) (R S : Type v) [Field k] [Field R] [Field S]
  (f : R →* S)

Lean source · full declaration

def primeToRootsCoefficientSystemIso
    (hf : ∀ n : InvertibleExponent k,
      Function.Bijective (restrictRootsOfUnity f n.val).toFun) :
    InverseSystem.InverseSystemIso (primeToRootsSystem k R) (primeToRootsSystem k S) where
  stageEquiv n :=
    { toMulEquiv := MulEquiv.ofBijective (restrictRootsOfUnity f n.val) (hf n)
      continuous_toFun := continuous_of_discreteTopology
      continuous_invFun := continuous_of_discreteTopology }
  comm := by
    intro m n h ξ
    exact restrictRootsOfUnity_powerTransition f h ξ

Module documentation

Ordinary coefficient comparison of roots systems

Declarations

primeToRootsCoefficientLimitMap

primeToRootsCoefficientLimitMap_scalar

primeToRootsCoefficientSystemIso