Module

RestrictedRootsCoefficientAction.lean

Nyll.EtaleFundamentalGroups.Inertia.RestrictedRootsCoefficientAction

6 declarations indexed from sourceView source ↗

Module documentation

Coefficient automorphisms on the literal restricted roots limit

The original power transitions commute with coefficient maps. Therefore every coefficient automorphism acts coordinatewise on this SAME limit.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.PrimeToRootsInverseSystem
Nyll.ProCGroups.InverseSystems.CofinalityAndDensity
Nyll.EtaleFundamentalGroups.Inertia.RestrictedPrimeToRootsGroupSystem
Mathlib.GroupTheory.Perm.Basic

Imported by2

def

restrictedRootsCoefficientMap

EtaleFundamentalGroups.Inertia.restrictedRootsCoefficientMap

Documentation

Apply a coefficient homomorphism to every coordinate of the existing limit.

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) (R : Type v) [Field k] [Field R]
  (J : Set (InvertibleExponent k))

Lean source · statement

def restrictedRootsCoefficientMap (f : R →+* R) :
    ((primeToRootsSystem k R).restrict J).inverseLimit →
      ((primeToRootsSystem k R).restrict J).inverseLimit

def

restrictedRootsCoefficientEquiv

EtaleFundamentalGroups.Inertia.restrictedRootsCoefficientEquiv

Documentation

The coordinatewise action of a coefficient automorphism is invertible.

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) (R : Type v) [Field k] [Field R]
  (J : Set (InvertibleExponent k))

Lean source · full declaration

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

def

restrictedRootsCoefficientAction

EtaleFundamentalGroups.Inertia.restrictedRootsCoefficientAction

Documentation

Ring automorphisms act on the SAME restricted inverse limit.

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) (R : Type v) [Field k] [Field R]
  (J : Set (InvertibleExponent k))

Lean source · full declaration

def restrictedRootsCoefficientAction :
    (R ≃+* R) →* Equiv.Perm (((primeToRootsSystem k R).restrict J).inverseLimit) where
  toFun := restrictedRootsCoefficientEquiv k R J
  map_one' := by
    apply Equiv.ext
    intro x
    apply ((primeToRootsSystem k R).restrict J).ext
    intro n
    apply rootsOfUnity.coe_injective
    rfl
  map_mul' f g := by
    apply Equiv.ext
    intro x
    apply ((primeToRootsSystem k R).restrict J).ext
    intro n
    apply rootsOfUnity.coe_injective
    rfl

theorem

restrictedRootsCoefficientAction_projection

EtaleFundamentalGroups.Inertia.restrictedRootsCoefficientAction_projection

Documentation

A scalar projection of the action is the actual coefficient action.

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) (R : Type v) [Field k] [Field R]
  (J : Set (InvertibleExponent k))

Lean source · statement

theorem restrictedRootsCoefficientAction_projection
    (f : R ≃+* R) (x : ((primeToRootsSystem k R).restrict J).inverseLimit)
    (n : Subtype J) :
    (((primeToRootsSystem k R).restrict J).projection n
      (((restrictedRootsCoefficientAction k R J).toFun f).toFun x)).val.val =
      f.toFun ((((primeToRootsSystem k R).restrict J).projection n x).val.val)

theorem

restrictedRootsCoefficientMap_one

EtaleFundamentalGroups.Inertia.restrictedRootsCoefficientMap_one

Documentation

Coefficient maps preserve the identity of the SAME coordinatewise limit group.

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) (R : Type v) [Field k] [Field R]
  (J : Set (InvertibleExponent k))

Lean source · full declaration

theorem restrictedRootsCoefficientMap_one (f : R →+* R) :
    let : ∀ n : Subtype J,
        Group (((primeToRootsSystem k R).restrict J).X n) :=
      fun n => primeToRootsSystem_group k R n.val
    let : IsGroupSystem ((primeToRootsSystem k R).restrict J) :=
      primeToRootsSystem_restrict_isGroupSystem k R J
    restrictedRootsCoefficientMap k R J f 1 = 1 := by
  intro stageGroups groupSystem
  apply ((primeToRootsSystem k R).restrict J).ext
  intro n
  apply rootsOfUnity.coe_injective
  exact f.map_one'

theorem

restrictedRootsCoefficientMap_mul

EtaleFundamentalGroups.Inertia.restrictedRootsCoefficientMap_mul

Documentation

Coefficient maps preserve multiplication in the SAME coordinatewise group.

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) (R : Type v) [Field k] [Field R]
  (J : Set (InvertibleExponent k))

Lean source · full declaration

theorem restrictedRootsCoefficientMap_mul (f : R →+* R)
    (x y : ((primeToRootsSystem k R).restrict J).inverseLimit) :
    let : ∀ n : Subtype J,
        Group (((primeToRootsSystem k R).restrict J).X n) :=
      fun n => primeToRootsSystem_group k R n.val
    let : IsGroupSystem ((primeToRootsSystem k R).restrict J) :=
      primeToRootsSystem_restrict_isGroupSystem k R J
    restrictedRootsCoefficientMap k R J f (x * y) =
      restrictedRootsCoefficientMap k R J f x * restrictedRootsCoefficientMap k R J f y := by
  intro stageGroups groupSystem
  apply ((primeToRootsSystem k R).restrict J).ext
  intro n
  apply rootsOfUnity.coe_injective
  exact f.map_mul' (x.val n).val.val (y.val n).val.val