ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.MulProjection

1 Theorem

The principal declarations in this module are:

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_mul_projection The finite-stage projection of the prime-power completed target derivative satisfies the Fox product rule.

import

ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental

Imported by

ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient

Theorem FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_mul_projection

theorem primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_mul_projection
    [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)))
    (i : X) (x y : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X))
    (j : PrimePowerCompletedGroupAlgebraIndex
      (foxAlgebraicStageTargetQuotient (X := X) N)) :
    primePowerCompletedGroupAlgebraProjection
        (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
        (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
          (ℓ := ℓ) (X := X) N hfinite i (x * y)) =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := FreeGroup X)
          (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex
            (ℓ := ℓ) (X := X) N hfinite j.1)
          (primePowerCompletedGroupAlgebraAugmentation
            (ℓ := ℓ) (G := FreeGroup X) y) •
        primePowerCompletedGroupAlgebraProjection
          (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
          (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
            (ℓ := ℓ) (X := X) N hfinite i x) +
      primePowerCompletedGroupAlgebraProjection
          (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
          (primePowerCompletedGroupAlgebraMap
            (ℓ := ℓ) (G := FreeGroup X)
            (H := foxAlgebraicStageTargetQuotient (X := X) N)
            (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N) x) *
        primePowerCompletedGroupAlgebraProjection
          (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
          (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
            (ℓ := ℓ) (X := X) N hfinite i y)

The finite-stage projection of the prime-power completed target derivative satisfies the Fox product rule.

Show Lean proof

ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.MulProjection

Declarations