NYLL
Module

Basic.lean

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

Module documentation

Fox differential: prime-power completed group algebra — in class — system — basic

The principal declarations in this module are:

  • PrimePowerCompletedGroupAlgebraStageInClass

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

  • primePowerCompletedGroupAlgebraTransitionInClass

The combined transition map for class-restricted prime-power stage calculus.

  • finite_primePowerCompletedGroupAlgebraStageInClass

Each class-indexed prime-power finite stage is finite.

  • primePowerCompletedGroupAlgebraTransitionInClass_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
Imported by2

Declarations

abbrev

PrimePowerCompletedGroupAlgebraStageInClass

L44 ↗
FoxDifferential.PrimePowerCompletedGroupAlgebraStageInClass
Documentation

The class-restricted prime-power 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 PrimePowerCompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    Type _
theorem

finite_primePowerCompletedGroupAlgebraStageInClass

L50 ↗
FoxDifferential.finite_primePowerCompletedGroupAlgebraStageInClass
Documentation

Each class-indexed prime-power finite 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
theorem finite_primePowerCompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    Finite (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i)
def

primePowerCompletedGroupAlgebraTransitionInClass

L60 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass
Documentation

The combined transition map for class-restricted 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 primePowerCompletedGroupAlgebraTransitionInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j →+*
      PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i
theorem

primePowerCompletedGroupAlgebraTransitionInClass_of

L77 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_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 primePowerCompletedGroupAlgebraTransitionInClass_of
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j)
    (q : CompletedGroupAlgebraQuotientInClass G C j.2) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _ q) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
theorem

primePowerCompletedGroupAlgebraTransitionInClass_single

L115 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransitionInClass_single
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j)
    (q : CompletedGroupAlgebraQuotientInClass G C j.2)
    (a : ModNCompletedCoeff (ℓ ^ j.1)) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
        (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1) a)
theorem

primePowerCompletedGroupAlgebraTransitionInClass_eq

L156 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_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 primePowerCompletedGroupAlgebraTransitionInClass_eq
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij =
      (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
        (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hij.2)
theorem

primePowerCompletedGroupAlgebraTransitionInClass_eq'

L171 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_eq'
Documentation

The class-indexed prime-power transition agrees with the explicit coefficient-and-quotient transition formula.

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 primePowerCompletedGroupAlgebraTransitionInClass_eq'
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij =
      (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C hij.2).comp
        (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C j.2
          (primePow_dvd_primePow (ℓ := ℓ) hij.1))
theorem

primePowerCompletedGroupAlgebraTransitionInClass_id

L191 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_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 primePowerCompletedGroupAlgebraTransitionInClass_id
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
        (le_rfl : i ≤ i) =
      RingHom.id _
theorem

primePowerCompletedGroupAlgebraTransitionInClass_comp

L206 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_comp
Documentation

Class-indexed prime-power 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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransitionInClass_comp
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j k : PrimePowerCompletedGroupAlgebraIndexInClass G C}
    (hij : i ≤ j) (hjk : j ≤ k) :
    (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij).comp
        (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hjk) =
      primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
        (hij.trans hjk)
theorem

primePowerCompletedGroupAlgebraStageAugmentationInClass_comp_transition

L306 ↗
FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentationInClass_comp_transition
Documentation

Class-indexed finite-stage prime-power augmentation is compatible with transition maps and coefficient reduction.

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 primePowerCompletedGroupAlgebraStageAugmentationInClass_comp_transition
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2).comp
        (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij) =
      (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
        (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ j.1) G C j.2)
def

primePowerCompletedGroupAlgebraSystemInClass

L323 ↗
FoxDifferential.primePowerCompletedGroupAlgebraSystemInClass
Documentation

The class-restricted inverse system indexed by prime powers and \(C\)-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 primePowerCompletedGroupAlgebraSystemInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    InverseSystem (I := PrimePowerCompletedGroupAlgebraIndexInClass G C) where
  X := PrimePowerCompletedGroupAlgebraStageInClass ℓ G C
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij =>
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
  continuous_map := by
    intro i j hij
    let : TopologicalSpace (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := ⊥
    let : TopologicalSpace (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) := ⊥
    let : DiscreteTopology (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransitionInClass_id
          (ℓ := ℓ) (G := G) C i)) x
  map_comp := by
    intro i j k hij hjk
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransitionInClass_comp
          (ℓ := ℓ) (G := G) C hij hjk)) x
theorem

directed_primePowerCompletedGroupAlgebraIndexInClass

L356 ↗
FoxDifferential.directed_primePowerCompletedGroupAlgebraIndexInClass
Documentation

The class-restricted prime-power group-algebra index family is directed under componentwise order when \(C\) is a formation.

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_primePowerCompletedGroupAlgebraIndexInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (hForm : ProCGroups.FiniteGroupClass.Formation C) :
    Directed (· ≤ ·) (id : PrimePowerCompletedGroupAlgebraIndexInClass G C →
      PrimePowerCompletedGroupAlgebraIndexInClass G C)
theorem

primePowerCompletedGroupAlgebraTransitionInClass_surjective

L373 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_surjective
Documentation

Every transition in the class-restricted 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 primePowerCompletedGroupAlgebraTransitionInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij)
def

PrimePowerCompletedGroupAlgebraCompatibleInClass

L391 ↗
FoxDifferential.PrimePowerCompletedGroupAlgebraCompatibleInClass
Documentation

Compatibility for a class-restricted prime-power 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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
def PrimePowerCompletedGroupAlgebraCompatibleInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
      PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) : Prop
abbrev

PrimePowerCompletedGroupAlgebraInClass

L403 ↗
FoxDifferential.PrimePowerCompletedGroupAlgebraInClass
Documentation

The class-restricted prime-power completed group algebra as an inverse-limit subtype. The all-finite PrimePowerCompletedGroupAlgebra below remains the ringed concrete formulation; this type is the class-indexed completed object that later Fox layers should target.

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

primePowerCompletedGroupAlgebraProjectionInClass

L410 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass
Documentation

The projection from the class-restricted completed group algebra to a prime-power 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
def primePowerCompletedGroupAlgebraProjectionInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    PrimePowerCompletedGroupAlgebraInClass ℓ G C →
      PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i
theorem

primePowerCompletedGroupAlgebraProjectionInClass_surjective

L420 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_surjective
Documentation

Every finite-stage projection from the class-restricted prime-power completed group algebra is surjective when \(C\) is a formation of finite quotient groups.

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 primePowerCompletedGroupAlgebraProjectionInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{u})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i)

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