FoxDifferential.foxCommutatorPowerSourceGAAugmentation_powerSourceGAMap
Source augmentation commutes with finite-stage coefficient/source reduction.
Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] inLean source · statement
theorem foxCommutatorPowerSourceGAAugmentation_powerSourceGAMap
(N : Subgroup (FreeGroup X)) (hnm : n₀ ∣ m₀)
(x : foxAlgebraicStageSourceGroupAlgebra (X := X) N m₀) :
foxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n₀
(foxAlgebraicStagePowerSourceGroupAlgebraMap (X := X) N hnm x) =
modNCompletedCoeffMap (n := n₀) (m := m₀) hnm
(foxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N m₀ x)