FoxDifferential.foxAlgebraicStagePrimePowerTargetStageMap_coeffMap
Compatibility of target stage maps with coefficient reduction in the completed target group algebra.
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 (ℓ : ℕ)
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 [DecidableEq X] inLean source · statement
theorem foxAlgebraicStagePrimePowerTargetStageMap_coeffMap
(N : Subgroup (FreeGroup X)) [N.Normal]
[TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
[IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
{a b : ℕ} (hab : a ≤ b)
(U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex
(foxAlgebraicStageTargetQuotient (X := X) N))
(x : foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b) :
modNCompletedGroupAlgebraStageCoeffMap
(n := ℓ ^ a) (m := ℓ ^ b)
(G := foxAlgebraicStageTargetQuotient (X := X) N) U
(primePow_dvd_primePow (ℓ := ℓ) hab)
(modNCompletedGroupAlgebraStageMap (ℓ ^ b)
(foxAlgebraicStageTargetQuotient (X := X) N) U x) =
modNCompletedGroupAlgebraStageMap (ℓ ^ a)
(foxAlgebraicStageTargetQuotient (X := X) N) U
(foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab x)