Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.Basic

14 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — mod-\(n\) completed group algebra — system — basic

The principal declarations in this module are:

ModNCompletedGroupAlgebraStage

The mod-\(N\) completed group-algebra stage combines the finite group quotient with the coefficient quotient modulo \(N\).

modNCompletedGroupAlgebraTransition

The mod-\(n\) group-algebra transition from a finer finite quotient stage to a coarser stage.

modNCompletedGroupAlgebraTransition_of

The transition map sends a group-like basis element to the basis element supported at its image in the coarser quotient in the Fox differential construction.

modNCompletedGroupAlgebraTransition_id

The transition map attached to the identity refinement is the identity homomorphism in the Fox differential construction.

Imports2

Imported by2

abbrev

ModNCompletedGroupAlgebraStage

L46 ↗

FoxDifferential.ModNCompletedGroupAlgebraStage

Documentation

The mod-\(N\) completed group-algebra stage combines the finite group quotient with the coefficient quotient modulo \(N\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

abbrev ModNCompletedGroupAlgebraStage (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) : Type _

instance

instFiniteModNCompletedGroupAlgebraStage

L51 ↗

FoxDifferential.instFiniteModNCompletedGroupAlgebraStage

Documentation

Each mod-\(n\) completed group-algebra stage is finite.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instFiniteModNCompletedGroupAlgebraStage (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    Finite (ModNCompletedGroupAlgebraStage n G U)

def

modNCompletedGroupAlgebraTransition

L79 ↗

FoxDifferential.modNCompletedGroupAlgebraTransition

Documentation

The mod-\(n\) group-algebra transition from a finer finite quotient stage to a coarser stage.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

def modNCompletedGroupAlgebraTransition
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    ModNCompletedGroupAlgebraStage n G V →+* ModNCompletedGroupAlgebraStage n G U

theorem

modNCompletedGroupAlgebraTransition_of

L93 ↗

FoxDifferential.modNCompletedGroupAlgebraTransition_of

Documentation

The transition map sends a group-like basis element to the basis element supported at its image in the coarser quotient in the Fox differential construction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraTransition_of
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
    (g : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V) :
    modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
      MonoidAlgebra.single ((OpenNormalSubgroupInClass.map
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
        (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1

theorem

modNCompletedGroupAlgebraTransition_id

L119 ↗

FoxDifferential.modNCompletedGroupAlgebraTransition_id

Documentation

The transition map attached to the identity refinement is the identity homomorphism in the Fox differential construction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraTransition_id (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    modNCompletedGroupAlgebraTransition n G (le_rfl : U ≤ U) = RingHom.id _

theorem

modNCompletedGroupAlgebraTransition_comp

L130 ↗

FoxDifferential.modNCompletedGroupAlgebraTransition_comp

Documentation

Mod-\(n\) completed group-algebra transitions compose along quotient refinements.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraTransition_comp
    {U V W : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hVW : V ≤
        W) :
    (modNCompletedGroupAlgebraTransition n G hUV).comp
        (modNCompletedGroupAlgebraTransition n G hVW) =
      modNCompletedGroupAlgebraTransition n G (hUV.trans hVW)

theorem

modNCompletedGroupAlgebraTransition_single_apply

L149 ↗

FoxDifferential.modNCompletedGroupAlgebraTransition_single_apply

Documentation

The \(n\)-modular completed group-algebra transition sends a singleton to the singleton supported at the induced quotient class with the same coefficient.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraTransition_single_apply
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
    (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V)
    (a : ModNCompletedCoeff n) :
    modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a

theorem

modNCompletedGroupAlgebraTransition_surjective

L175 ↗

FoxDifferential.modNCompletedGroupAlgebraTransition_surjective

Documentation

The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraTransition_surjective
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    Function.Surjective (modNCompletedGroupAlgebraTransition n G hUV)

def

modNCompletedGroupAlgebraStageMap

L211 ↗

FoxDifferential.modNCompletedGroupAlgebraStageMap

Documentation

The quotient map \((\mathbb{Z}/n\mathbb{Z})[G] \to (\mathbb{Z}/n\mathbb{Z})[G/U]\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

def modNCompletedGroupAlgebraStageMap (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStage n G U

theorem

modNCompletedGroupAlgebraStageMap_of

L224 ↗

FoxDifferential.modNCompletedGroupAlgebraStageMap_of

Documentation

The finite-stage group-like map sends a group element to the corresponding singleton basis element in the quotient group algebra in the Fox differential construction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraStageMap_of
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (g : G) :
    modNCompletedGroupAlgebraStageMap n G U (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1

theorem

modNCompletedGroupAlgebraStageMap_compatible

L243 ↗

FoxDifferential.modNCompletedGroupAlgebraStageMap_compatible

Documentation

The mod-\(n\) completed group-algebra stage maps are compatible with quotient refinement.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraStageMap_compatible
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (modNCompletedGroupAlgebraTransition n G hUV).comp
        (modNCompletedGroupAlgebraStageMap n G V) =
      modNCompletedGroupAlgebraStageMap n G U

def

modNCompletedGroupAlgebraSystem

L254 ↗

FoxDifferential.modNCompletedGroupAlgebraSystem

Documentation

The inverse system \(U \mapsto (\mathbb{Z}/n\mathbb{Z})[G/U]\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · full declaration

def modNCompletedGroupAlgebraSystem :
    InverseSystem (I := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) where
  X := ModNCompletedGroupAlgebraStage n G
  topologicalSpace := fun _ => ⊥
  map := fun {U V} hUV => modNCompletedGroupAlgebraTransition n G hUV
  continuous_map := by
    intro U V hUV
    let : TopologicalSpace (ModNCompletedGroupAlgebraStage n G U) := ⊥
    let : TopologicalSpace (ModNCompletedGroupAlgebraStage n G V) := ⊥
    let : DiscreteTopology (ModNCompletedGroupAlgebraStage n G V) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro U
    funext x
    exact congrFun
      (congrArg DFunLike.coe (modNCompletedGroupAlgebraTransition_id (n := n) (G := G) U)) x
  map_comp := by
    intro U V W hUV hVW
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (modNCompletedGroupAlgebraTransition_comp (n := n) (G := G) hUV hVW)) x

abbrev

ModNCompletedGroupAlgebra

L279 ↗

FoxDifferential.ModNCompletedGroupAlgebra

Documentation

The inverse-limit object of the residue-coefficient stage tower.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

abbrev ModNCompletedGroupAlgebra

abbrev

modNCompletedGroupAlgebraProjection

L284 ↗

FoxDifferential.modNCompletedGroupAlgebraProjection

Documentation

The projection from the residue-coefficient inverse limit to one finite stage.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in

Lean source · statement

abbrev modNCompletedGroupAlgebraProjection (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ModNCompletedGroupAlgebra n G → ModNCompletedGroupAlgebraStage n G U

Module documentation

Fox differential: coefficient rings — mod-\(n\) completed group algebra — system — basic

Declarations