NYLL
Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic
14 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — prime-power completed group algebra — system — basic

The principal declarations in this module are:

  • PrimePowerCompletedGroupAlgebraStage

The stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[G/U]\).

  • primePowerCompletedGroupAlgebraTransition

The combined transition map for the two-parameter prime-power stage calculus.

  • primePowerCompletedGroupAlgebraTransition_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.

  • primePowerCompletedGroupAlgebraTransition_eq

The transition map for the prime-power completed group algebra commutes with the finite-stage coordinate maps.

Imports2
Imported by2

Declarations

abbrev

PrimePowerCompletedGroupAlgebraStage

L41 ↗
FoxDifferential.PrimePowerCompletedGroupAlgebraStage
Documentation

The stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
abbrev PrimePowerCompletedGroupAlgebraStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) : Type _
instance

instFinitePrimePowerCompletedGroupAlgebraStage

L46 ↗
FoxDifferential.instFinitePrimePowerCompletedGroupAlgebraStage
Documentation

Each prime-power 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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance instFinitePrimePowerCompletedGroupAlgebraStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    Finite (PrimePowerCompletedGroupAlgebraStage ℓ G i)
def

primePowerCompletedGroupAlgebraTransition

L54 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransition
Documentation

The combined transition map for the two-parameter prime-power stage calculus.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
def primePowerCompletedGroupAlgebraTransition
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    PrimePowerCompletedGroupAlgebraStage ℓ G j →+* PrimePowerCompletedGroupAlgebraStage ℓ G i
theorem

primePowerCompletedGroupAlgebraTransition_of

L69 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransition_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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransition_of
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
    (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G j.2) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _ q) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
        ((OpenNormalSubgroupInClass.map
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
          (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
theorem

primePowerCompletedGroupAlgebraTransition_eq

L105 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransition_eq
Documentation

The transition map for the prime-power completed group algebra commutes with the finite-stage coordinate maps.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransition_eq
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij =
      (modNCompletedGroupAlgebraStageCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
        (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2)
theorem

primePowerCompletedGroupAlgebraTransition_eq'

L119 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransition_eq'
Documentation

The same combined transition can also be read as coefficient reduction at the source stage followed by the quotient-direction transition at the smaller modulus.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransition_eq'
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij =
      (modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G hij.2).comp
        (modNCompletedGroupAlgebraStageCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) j.2
          (primePow_dvd_primePow (ℓ := ℓ) hij.1))
theorem

primePowerCompletedGroupAlgebraTransition_id

L137 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransition_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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransition_id
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (le_rfl : i ≤ i) =
      RingHom.id _
theorem

primePowerCompletedGroupAlgebraTransition_comp

L150 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransition_comp
Documentation

Prime-power completed group-algebra transitions compose along a chain of 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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransition_comp
    {i j k : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) (hjk : j ≤ k) :
    (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij).comp
        (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hjk) =
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (hij.trans hjk)
def

primePowerCompletedGroupAlgebraSystem

L236 ↗
FoxDifferential.primePowerCompletedGroupAlgebraSystem
Documentation

The inverse system indexed by prime powers and finite quotients.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · full declaration
def primePowerCompletedGroupAlgebraSystem :
    InverseSystem (I := PrimePowerCompletedGroupAlgebraIndex G) where
  X := PrimePowerCompletedGroupAlgebraStage ℓ G
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij => primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
  continuous_map := by
    intro i j hij
    let : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G i) := ⊥
    let : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G j) := ⊥
    let : DiscreteTopology (PrimePowerCompletedGroupAlgebraStage ℓ G j) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransition_id (ℓ := ℓ) (G := G) i)) x
  map_comp := by
    intro i j k hij hjk
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransition_comp (ℓ := ℓ) (G := G) hij hjk)) x
abbrev

PrimePowerCompletedGroupAlgebra

L262 ↗
FoxDifferential.PrimePowerCompletedGroupAlgebra
Documentation

The inverse-limit object of the prime-power finite-stage system.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
abbrev PrimePowerCompletedGroupAlgebra
abbrev

primePowerCompletedGroupAlgebraProjection

L267 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection
Documentation

The projection from the prime-power completed group algebra 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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
abbrev primePowerCompletedGroupAlgebraProjection (i : PrimePowerCompletedGroupAlgebraIndex G) :
    PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedGroupAlgebraStage ℓ G i
theorem

directed_primePowerCompletedGroupAlgebraIndex

L273 ↗
FoxDifferential.directed_primePowerCompletedGroupAlgebraIndex
Documentation

The prime-power group-algebra index family is directed under the componentwise order.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem directed_primePowerCompletedGroupAlgebraIndex :
    Directed (· ≤ ·) (id : PrimePowerCompletedGroupAlgebraIndex G →
      PrimePowerCompletedGroupAlgebraIndex G)
theorem

primePowerCompletedGroupAlgebraTransition_surjective

L286 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransition_surjective
Documentation

Every transition in the prime-power completed group-algebra system is surjective.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransition_surjective
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij)
theorem

primePowerCompletedGroupAlgebraProjection_surjective

L302 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection_surjective
Documentation

Every finite-stage projection from the prime-power completed group algebra is surjective.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjection_surjective
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    Function.Surjective (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.