FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_mul_projection
The finite-stage projection of the prime-power completed target derivative satisfies the Fox product rule.
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 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)