Module

Fundamental.lean

Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental

2 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — differential module — target quotient — fundamental

The principal declarations in this module are:

ppCompletedGAFoxDerivToTarget_of_fundFormula_map

The completed Fox derivative satisfies the fundamental formula after passage to the target quotient.

ppCompletedGAFoxDerivToTarget_of_mul_product_map

The completed Fox derivative of a product is computed by the crossed product rule after passage to the target quotient.

Imports3

Imported by2

theorem

ppCompletedGAFoxDerivToTarget_of_fundFormula_map

L44 ↗

FoxDifferential.ppCompletedGAFoxDerivToTarget_of_fundFormula_map

Documentation

The completed Fox derivative satisfies the fundamental formula after passage to the target quotient.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
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]

Lean source · statement

theorem ppCompletedGAFoxDerivToTarget_of_fundFormula_map
    [Fintype X]
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (w : FreeGroup X) :
    primePowerCompletedGroupAlgebraMap
        (ℓ := ℓ) (G := FreeGroup X)
        (H := foxAlgebraicStageTargetQuotient (X := X) N)
        (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) - 1 =
      ∑ i : X,
        primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
          (ℓ := ℓ) (X := X) N hfinite i
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) *
          (primePowerCompletedGroupAlgebraMap
            (ℓ := ℓ) (G := FreeGroup X)
            (H := foxAlgebraicStageTargetQuotient (X := X) N)
            (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
            (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X)
              (FreeGroup.of i)) - 1)