NYLL
Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Basic
17 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — basic

The principal declarations in this module are:

  • foxCommutatorPowerRelatorSet

Relators defining the finite Fox source quotient: commutators in \(N\) and \(n\)-th powers in \(N\).

  • foxCommutatorPowerSubgroup

Normal subgroup generated by commutators in \(N\) and \(n\)-th powers in \(N\).

  • modNCompletedGroupAlgebraStageMap_algebraMap

The finite-stage completed group-algebra projection preserves coefficient algebra maps.

  • foxCommutatorPowerRelatorSet_subset

The finite Fox commutator-power relator set is contained in N.

Imports1
Imported by2

Declarations

theorem

modNCompletedGroupAlgebraStageMap_algebraMap

L46 ↗
FoxDifferential.modNCompletedGroupAlgebraStageMap_algebraMap
Documentation

The finite-stage completed group-algebra projection preserves coefficient algebra maps.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section ModNStageMapScalar
variable (n : ℕ) [Fact (0 < n)]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageMap_algebraMap
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (c : ModNCompletedCoeff n) :
    modNCompletedGroupAlgebraStageMap n G U
        (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) c) =
      algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupAlgebraStage n G U) c
def

foxCommutatorPowerRelatorSet

L64 ↗
FoxDifferential.foxCommutatorPowerRelatorSet
Documentation

Relators defining the finite Fox source quotient: commutators in \(N\) and \(n\)-th powers in \(N\).

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
def foxCommutatorPowerRelatorSet (N : Subgroup F) (n : ℕ) : Set F
def

foxCommutatorPowerSubgroup

L68 ↗
FoxDifferential.foxCommutatorPowerSubgroup
Documentation

Normal subgroup generated by commutators in \(N\) and \(n\)-th powers in \(N\).

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
def foxCommutatorPowerSubgroup (N : Subgroup F) (n : ℕ) : Subgroup F
instance

foxCommutatorPowerSubgroup_normal

L72 ↗
FoxDifferential.foxCommutatorPowerSubgroup_normal
Documentation

The finite Fox commutator-power subgroup is normal by construction.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
instance foxCommutatorPowerSubgroup_normal
    (N : Subgroup F) (n : ℕ) :
    (foxCommutatorPowerSubgroup (F := F) N n).Normal
theorem

foxCommutatorPowerRelatorSet_subset

L79 ↗
FoxDifferential.foxCommutatorPowerRelatorSet_subset
Documentation

The finite Fox commutator-power relator set is contained in N.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
theorem foxCommutatorPowerRelatorSet_subset
    (N : Subgroup F) (n : ℕ) :
    foxCommutatorPowerRelatorSet (F := F) N n ⊆ N
theorem

foxCommutatorPowerSubgroup_le_normal

L89 ↗
FoxDifferential.foxCommutatorPowerSubgroup_le_normal
Documentation

The finite Fox commutator-power subgroup is contained in \(N\) when \(N\) is normal.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
theorem foxCommutatorPowerSubgroup_le_normal
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    foxCommutatorPowerSubgroup (F := F) N n ≤ N
def

foxCommutatorPowerQuotientMapToNormalQuotient

L96 ↗
FoxDifferential.foxCommutatorPowerQuotientMapToNormalQuotient
Documentation

Natural quotient map \(F/[N,N]N^n \to F/N\).

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
def foxCommutatorPowerQuotientMapToNormalQuotient
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    F ⧸ foxCommutatorPowerSubgroup (F := F) N n →* F ⧸ N
theorem

foxCommutatorPowerQuotientMapToNormalQuotient_mk

L104 ↗
FoxDifferential.foxCommutatorPowerQuotientMapToNormalQuotient_mk
Documentation

Evaluation of the natural quotient map \(F/[N,N]N^n \to F/N\) on a representative.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
theorem foxCommutatorPowerQuotientMapToNormalQuotient_mk
    (N : Subgroup F) [N.Normal] (n : ℕ) (g : F) :
    foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := F) N n) g) =
      QuotientGroup.mk' N g
theorem

foxCommutatorPowerQuotientMapToNormalQuotient_surjective

L113 ↗
FoxDifferential.foxCommutatorPowerQuotientMapToNormalQuotient_surjective
Documentation

The natural quotient map \(F/[N,N]N^n \to F/N\) is surjective.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
theorem foxCommutatorPowerQuotientMapToNormalQuotient_surjective
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    Function.Surjective
      (foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n)
def

foxCommutatorPowerGroupAlgebraMap

L123 ↗
FoxDifferential.foxCommutatorPowerGroupAlgebraMap
Documentation

Group-algebra map induced by the natural quotient \(F/[N,N]N^n \to F/N\).

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
def foxCommutatorPowerGroupAlgebraMap
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) →+*
      MonoidAlgebra (ModNCompletedCoeff n) (F ⧸ N)
def

foxCommutatorPowerGroupAlgebraAlgHom

L132 ↗
FoxDifferential.foxCommutatorPowerGroupAlgebraAlgHom
Documentation

Algebra-hom version of the group-algebra map induced by \(F/[N,N]N^n \to F/N\).

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
def foxCommutatorPowerGroupAlgebraAlgHom
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) →ₐ[
      ModNCompletedCoeff n]
      MonoidAlgebra (ModNCompletedCoeff n) (F ⧸ N)
theorem

foxCommutatorPowerGroupAlgebraAlgHom_apply

L143 ↗
FoxDifferential.foxCommutatorPowerGroupAlgebraAlgHom_apply
Documentation

The algebra-hom and ring-hom versions of the finite Fox quotient map agree on values.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
theorem foxCommutatorPowerGroupAlgebraAlgHom_apply
    (N : Subgroup F) [N.Normal] (n : ℕ)
    (x : MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ foxCommutatorPowerSubgroup (F := F) N n)) :
    foxCommutatorPowerGroupAlgebraAlgHom (F := F) N n x =
      foxCommutatorPowerGroupAlgebraMap (F := F) N n x
def

foxCommutatorPowerSourceGroupAlgebraAugmentation

L151 ↗
FoxDifferential.foxCommutatorPowerSourceGroupAlgebraAugmentation
Documentation

Augmentation map on the finite Fox source group algebra.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
def foxCommutatorPowerSourceGroupAlgebraAugmentation
    (N : Subgroup F) (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) →ₐ[
      ModNCompletedCoeff n] ModNCompletedCoeff n
theorem

foxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient

L163 ↗
FoxDifferential.foxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient
Documentation

The source augmentation sends every quotient group basis element to \(1\).

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
theorem foxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient
    (N : Subgroup F) (n : ℕ)
    (q : F ⧸ foxCommutatorPowerSubgroup (F := F) N n) :
    foxCommutatorPowerSourceGroupAlgebraAugmentation (F := F) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) q) =
      1
theorem

foxCommutatorPowerGroupAlgebraMap_of

L175 ↗
FoxDifferential.foxCommutatorPowerGroupAlgebraMap_of
Documentation

The finite Fox source-to-target group-algebra map evaluated on a represented word.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
theorem foxCommutatorPowerGroupAlgebraMap_of
    (N : Subgroup F) [N.Normal] (n : ℕ) (g : F) :
    foxCommutatorPowerGroupAlgebraMap (F := F) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (F ⧸ foxCommutatorPowerSubgroup (F := F) N n)
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := F) N n) g)) =
      MonoidAlgebra.of (ModNCompletedCoeff n) (F ⧸ N) (QuotientGroup.mk' N g)
theorem

foxCommutatorPowerGroupAlgebraMap_of_quotient

L194 ↗
FoxDifferential.foxCommutatorPowerGroupAlgebraMap_of_quotient
Documentation

The finite Fox source-to-target group-algebra map evaluated on a quotient basis element.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
Lean source · statement
theorem foxCommutatorPowerGroupAlgebraMap_of_quotient
    (N : Subgroup F) [N.Normal] (n : ℕ)
    (q : F ⧸ foxCommutatorPowerSubgroup (F := F) N n) :
    foxCommutatorPowerGroupAlgebraMap (F := F) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n) (F ⧸ N)
        (foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n q)
theorem

foxCommutatorPowerGroupAlgebraMap_single_apply

L212 ↗
FoxDifferential.foxCommutatorPowerGroupAlgebraMap_single_apply
Documentation

The finite Fox source-to-target group-algebra map evaluated on a single coefficient basis term.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FoxCommutatorPowerQuotient
variable {F : Type u} [Group F]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem foxCommutatorPowerGroupAlgebraMap_single_apply
    (N : Subgroup F) [N.Normal] (n : ℕ)
    (q : F ⧸ foxCommutatorPowerSubgroup (F := F) N n)
    (a : ModNCompletedCoeff n) :
    foxCommutatorPowerGroupAlgebraMap (F := F) N n
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        (foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n q) a

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