Module

Source.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Source

10 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — stage — source

The principal declarations in this module are:

foxAlgebraicStageSourceRepresentative

A chosen free-group representative of a finite Fox source quotient element, supplying source-valued coefficients without a canonicality requirement.

foxAlgebraicStageSourceQuotientDerivative

Source-valued finite Fox coefficient attached to a source quotient element, using a chosen free-group representative.

foxAlgebraicStageSourceRepresentative_mk

The chosen representative maps back to the original source quotient element.

foxAlgebraicStageSourceGroupAlgebraDerivative_of_quotient

Evaluation of the source-valued finite Fox derivative on a source quotient basis element.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Naturality

Imported by4

def

foxAlgebraicStageSourceRepresentative

L47 ↗

FoxDifferential.foxAlgebraicStageSourceRepresentative

Documentation

A chosen free-group representative of a finite Fox source quotient element, supplying source-valued coefficients without a canonicality requirement.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSourceRepresentative
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    FreeGroup X

theorem

foxAlgebraicStageSourceRepresentative_mk

L57 ↗

FoxDifferential.foxAlgebraicStageSourceRepresentative_mk

Documentation

The chosen representative maps back to the original source quotient 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
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] [N.Normal] in

Lean source · statement

theorem foxAlgebraicStageSourceRepresentative_mk
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    QuotientGroup.mk'
        (foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
        (foxAlgebraicStageSourceRepresentative (X := X) N n q) = q

def

foxAlgebraicStageSourceQuotientDerivative

L71 ↗

FoxDifferential.foxAlgebraicStageSourceQuotientDerivative

Documentation

Source-valued finite Fox coefficient attached to a source quotient element, using a chosen free-group representative.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSourceQuotientDerivative
    (i : X)
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSourceGroupAlgebra (X := X) N n

def

foxAlgebraicStageSourceGroupAlgebraDerivative

L84 ↗

FoxDifferential.foxAlgebraicStageSourceGroupAlgebraDerivative

Documentation

Source-valued finite Fox derivative on the source group algebra. It is defined by extending the representative-based source coefficients linearly.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSourceGroupAlgebraDerivative (i : X) :
    foxAlgebraicStageSourceGroupAlgebra (X := X) N n →ₗ[ModNCompletedCoeff n]
      foxAlgebraicStageSourceGroupAlgebra (X := X) N n

theorem

foxAlgebraicStageSourceGroupAlgebraDerivative_of_quotient

L94 ↗

FoxDifferential.foxAlgebraicStageSourceGroupAlgebraDerivative_of_quotient

Documentation

Evaluation of the source-valued finite Fox derivative on a source 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
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [N.Normal] in

Lean source · statement

theorem foxAlgebraicStageSourceGroupAlgebraDerivative_of_quotient
    (i : X)
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSourceGroupAlgebraDerivative (X := X) N n i
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q) =
      foxAlgebraicStageSourceQuotientDerivative (X := X) N n i q

theorem

foxAlgebraicStageSourceGroupAlgebraDerivative_of_quotient_fundamental_formula

L110 ↗

FoxDifferential.foxAlgebraicStageSourceGroupAlgebraDerivative_of_quotient_fundamental_formula

Documentation

The source-valued finite Fox fundamental formula on a source 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
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [N.Normal] in

Lean source · statement

theorem foxAlgebraicStageSourceGroupAlgebraDerivative_of_quotient_fundamental_formula
    [Fintype X]
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    MonoidAlgebra.of (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q - 1 =
      ∑ i : X,
        foxAlgebraicStageSourceGroupAlgebraDerivative (X := X) N n i
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q) *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
            (QuotientGroup.mk'
              (foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
              (FreeGroup.of i)) - 1)

theorem

foxAlgebraicStageSourceGroupAlgebraDerivative_groupAlgebra_fundamental_formula

L172 ↗

FoxDifferential.foxAlgebraicStageSourceGroupAlgebraDerivative_groupAlgebra_fundamental_formula

Documentation

Source-valued finite Fox fundamental formula on the full 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
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [N.Normal] in

Lean source · statement

theorem foxAlgebraicStageSourceGroupAlgebraDerivative_groupAlgebra_fundamental_formula
    [Fintype X]
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    x -
        algebraMap (ModNCompletedCoeff n)
          (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
          (foxCommutatorPowerSourceGroupAlgebraAugmentation
            (F := FreeGroup X) N n x) =
      ∑ i : X,
        foxAlgebraicStageSourceGroupAlgebraDerivative (X := X) N n i x *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
            (QuotientGroup.mk'
              (foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
              (FreeGroup.of i)) - 1)

theorem

foxCommutatorPowerGroupAlgebraMap_smul

L353 ↗

FoxDifferential.foxCommutatorPowerGroupAlgebraMap_smul

Documentation

The source-to-target group-algebra map commutes with scalar multiplication by \(\mathbb{Z}/n\mathbb{Z}\) coefficients.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxCommutatorPowerGroupAlgebraMap_smul
    (a : ModNCompletedCoeff n)
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (a • x) =
      a • foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x

theorem

foxAlgebraicStageSourceGroupAlgebraDerivative_map_of_quotient

L368 ↗

FoxDifferential.foxAlgebraicStageSourceGroupAlgebraDerivative_map_of_quotient

Documentation

Applying the source-to-target finite group-algebra map to the source-valued derivative gives the existing target-valued finite Fox derivative.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSourceGroupAlgebraDerivative_map_of_quotient
    (i : X)
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
        (foxAlgebraicStageSourceGroupAlgebraDerivative (X := X) N n i
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q)) =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q)

theorem

foxAlgebraicStageSourceGroupAlgebraDerivative_map

L400 ↗

FoxDifferential.foxAlgebraicStageSourceGroupAlgebraDerivative_map

Documentation

Applying the source-to-target finite group-algebra map to the source-valued derivative agrees with the target-valued finite Fox derivative on all source group-algebra elements.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
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]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSourceGroupAlgebraDerivative_map
    (i : X) (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
        (foxAlgebraicStageSourceGroupAlgebraDerivative (X := X) N n i x) =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i x

Module documentation

Fox differential: completed — finite stage — stage — source

Declarations