FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivative_generator_projection
The generator-value projection formula for the completed source Fox derivative.
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 [Fact (0 < ℓ)] inLean source · statement
theorem primePowerCompletedGroupAlgebraFreeFoxDerivative_generator_projection
[TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
[DiscreteTopology (FreeGroup X)]
(N : Subgroup (FreeGroup X)) [N.Normal]
(hfinite : ∀ a : ℕ,
Finite (FreeGroup X ⧸
foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
(i j : X) (a : ℕ) :
(foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
(primePowerCompletedGroupAlgebraFreeFoxDerivative
(ℓ := ℓ) (X := X) N hfinite i
(primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X)
(FreeGroup.of j))) =
((Pi.single j (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ a))) :
X → foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ a)) i