NYLL
Module

Formula.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Fundamental.Formula
3 declarations indexed from sourceView source ↗

Module documentation

Fox differential: finite stage — stage — fundamental — formula

The principal declarations in this module are:

  • foxAlgebraicStageGroupAlgebraDerivative_of_quotient_fundamental_formula

Finite-stage Fox fundamental formula on a source quotient basis element after mapping to the target group algebra.

  • foxAlgebraicStageGroupAlgebraDerivative_groupAlgebra_fundamental_formula_algHom

Algebra-homomorphism form of the finite-stage Fox fundamental formula on the source group algebra.

  • foxAlgebraicStageGroupAlgebraDerivative_groupAlgebra_fundamental_formula

Ring-hom form of the finite-stage Fox fundamental formula on the source group algebra.

Imports1
Imported by2

Declarations

theorem

foxAlgebraicStageGroupAlgebraDerivative_of_quotient_fundamental_formula

L44 ↗
FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_of_quotient_fundamental_formula
Documentation

Finite-stage Fox fundamental formula on a source quotient basis element after mapping to the target group algebra.

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 foxAlgebraicStageGroupAlgebraDerivative_of_quotient_fundamental_formula
    [Fintype X]
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q) - 1 =
      ∑ i : X,
        foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q) *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1)
theorem

foxAlgebraicStageGroupAlgebraDerivative_groupAlgebra_fundamental_formula_algHom

L67 ↗
FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_groupAlgebra_fundamental_formula_algHom
Documentation

Algebra-homomorphism form of the finite-stage Fox fundamental formula on the source group algebra.

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 foxAlgebraicStageGroupAlgebraDerivative_groupAlgebra_fundamental_formula_algHom
    [Fintype X]
    (x : MonoidAlgebra (ModNCompletedCoeff n)
      (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)) :
    foxCommutatorPowerGroupAlgebraAlgHom (F := FreeGroup X) N n x -
        algebraMap (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
          (foxCommutatorPowerSourceGroupAlgebraAugmentation
            (F := FreeGroup X) N n x) =
      ∑ i : X,
        foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i x *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1)
theorem

foxAlgebraicStageGroupAlgebraDerivative_groupAlgebra_fundamental_formula

L189 ↗
FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_groupAlgebra_fundamental_formula
Documentation

Ring-hom form of the finite-stage Fox fundamental formula on the source group algebra.

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 foxAlgebraicStageGroupAlgebraDerivative_groupAlgebra_fundamental_formula
    [Fintype X]
    (x : MonoidAlgebra (ModNCompletedCoeff n)
      (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)) :
    foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x -
        algebraMap (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
          (foxCommutatorPowerSourceGroupAlgebraAugmentation
            (F := FreeGroup X) N n x) =
      ∑ i : X,
        foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i x *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1)

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