Module

Basic.lean

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

17 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

ModNCompletedCoeff

The coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) used in one residue-coefficient stage.

ModNCompletedGroupRing

The group ring \((\mathbb{Z}/n\mathbb{Z})[H]\) used in the residue-coefficient tower.

finite_modNCompletedGroupAlgebraStageInClass

Each \(C\)-indexed finite stage of the mod-\(n\) completed group algebra is finite.

modNCompletedGroupAlgebraTransitionInClass_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.

Imports2

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra
Mathlib.Data.ZMod.Basic

Imported by3

abbrev

ModNCompletedGroupAlgebraStageInClass

L50 ↗

FoxDifferential.ModNCompletedGroupAlgebraStageInClass

Documentation

The residue-coefficient stage over a class-restricted finite quotient \(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

abbrev ModNCompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _

theorem

finite_modNCompletedGroupAlgebraStageInClass

L55 ↗

FoxDifferential.finite_modNCompletedGroupAlgebraStageInClass

Documentation

Each \(C\)-indexed finite stage of the mod-\(n\) completed group algebra 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

theorem finite_modNCompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Finite (ModNCompletedGroupAlgebraStageInClass n G C U)

def

modNCompletedGroupAlgebraTransitionInClass

L83 ↗

FoxDifferential.modNCompletedGroupAlgebraTransitionInClass

Documentation

The transition map between class-restricted residue-coefficient stages.

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 modNCompletedGroupAlgebraTransitionInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    ModNCompletedGroupAlgebraStageInClass n G C V →+*
      ModNCompletedGroupAlgebraStageInClass n G C U

theorem

modNCompletedGroupAlgebraTransitionInClass_of

L99 ↗

FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_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 modNCompletedGroupAlgebraTransitionInClass_of
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (g : CompletedGroupAlgebraQuotientInClass G C V) :
    modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1

theorem

modNCompletedGroupAlgebraTransitionInClass_single

L129 ↗

FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_single

Documentation

The \(C\)-indexed transition map between finite stages sends a singleton supported at a class of the finer quotient to the singleton supported at its image in the coarser quotient, preserving the 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 modNCompletedGroupAlgebraTransitionInClass_single
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (q : CompletedGroupAlgebraQuotientInClass G C V)
    (a : ModNCompletedCoeff n) :
    modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a

theorem

modNCompletedGroupAlgebraTransitionInClass_id

L159 ↗

FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_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 modNCompletedGroupAlgebraTransitionInClass_id
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    modNCompletedGroupAlgebraTransitionInClass n G C (le_rfl : U ≤ U) = RingHom.id _

theorem

modNCompletedGroupAlgebraTransitionInClass_comp

L171 ↗

FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_comp

Documentation

Class-indexed 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 modNCompletedGroupAlgebraTransitionInClass_comp
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
    (modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
        (modNCompletedGroupAlgebraTransitionInClass n G C hVW) =
      modNCompletedGroupAlgebraTransitionInClass n G C (hUV.trans hVW)

def

modNCompletedGroupAlgebraSystemInClass

L194 ↗

FoxDifferential.modNCompletedGroupAlgebraSystemInClass

Documentation

The class-restricted 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 modNCompletedGroupAlgebraSystemInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
  X := ModNCompletedGroupAlgebraStageInClass n G C
  topologicalSpace := fun _ => ⊥
  map := fun {U V} hUV => modNCompletedGroupAlgebraTransitionInClass n G C hUV
  continuous_map := by
    intro U V hUV
    let : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C U) := ⊥
    let : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C V) := ⊥
    let : DiscreteTopology (ModNCompletedGroupAlgebraStageInClass n G C V) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro U
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (modNCompletedGroupAlgebraTransitionInClass_id n G C U)) x
  map_comp := by
    intro U V W hUV hVW
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (modNCompletedGroupAlgebraTransitionInClass_comp n G C hUV hVW)) x

theorem

modNCompletedGroupAlgebraTransitionInClass_surjective

L224 ↗

FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_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 modNCompletedGroupAlgebraTransitionInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    Function.Surjective (modNCompletedGroupAlgebraTransitionInClass n G C hUV)

def

modNCompletedGroupAlgebraStageMapInClass

L272 ↗

FoxDifferential.modNCompletedGroupAlgebraStageMapInClass

Documentation

The quotient map \((\mathbb{Z}/n\mathbb{Z})[G] \to (\mathbb{Z}/n\mathbb{Z})[G/U]\) for a class-restricted 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 modNCompletedGroupAlgebraStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStageInClass n G C U

theorem

modNCompletedGroupAlgebraStageMapInClass_of

L284 ↗

FoxDifferential.modNCompletedGroupAlgebraStageMapInClass_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 modNCompletedGroupAlgebraStageMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
    modNCompletedGroupAlgebraStageMapInClass n G C U
        (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1

theorem

modNCompletedGroupAlgebraStageMapInClass_compatible

L304 ↗

FoxDifferential.modNCompletedGroupAlgebraStageMapInClass_compatible

Documentation

The class-restricted 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 modNCompletedGroupAlgebraStageMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
        (modNCompletedGroupAlgebraStageMapInClass n G C V) =
      modNCompletedGroupAlgebraStageMapInClass n G C U

def

ModNCompletedGroupAlgebraCompatibleInClass

L331 ↗

FoxDifferential.ModNCompletedGroupAlgebraCompatibleInClass

Documentation

Compatibility for a class-restricted residue-coefficient completed group algebra family.

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 ModNCompletedGroupAlgebraCompatibleInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
      ModNCompletedGroupAlgebraStageInClass n G C U) : Prop

abbrev

ModNCompletedGroupAlgebraInClass

L339 ↗

FoxDifferential.ModNCompletedGroupAlgebraInClass

Documentation

The class-restricted residue-coefficient completed group algebra as an inverse-limit subtype.

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 ModNCompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _

def

modNCompletedGroupAlgebraProjectionInClass

L348 ↗

FoxDifferential.modNCompletedGroupAlgebraProjectionInClass

Documentation

The projection from the class-restricted residue-coefficient completed group algebra to a 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 modNCompletedGroupAlgebraProjectionInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    ModNCompletedGroupAlgebraInClass n G C →
      ModNCompletedGroupAlgebraStageInClass n G C U

Module documentation

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

Declarations