Module

CoordinateStageProjection.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.CoordinateStageProjection

14 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — coordinate stage projection

The principal declarations in this module are:

zcFreeFoxCoordinatesStageMap

Coordinatewise finite-stage projection on completed Fox vectors, induced by a coefficient ring map \(\mathbb{Z}_C\llbracket H\rrbracket \to (\mathbb{Z}/n\mathbb{Z})[F/N]\).

freeProCZCCompletedFoxSemidirectStageMapOfCoeff

The semidirect finite-stage projection induced by a coefficient projection and a target quotient map.

zcFreeFoxCoordinatesStageMap_apply

The finite-stage map on completed Fox-coordinate vectors is computed coordinatewise by the underlying coefficient-stage map.

zcFreeFoxCoordinatesStageMap_single

The finite-stage coordinate map for completed free Fox coordinates has the stated value on a single generator.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.StageProjection

Imported by2

def

zcFreeFoxCoordinatesStageMap

L50 ↗

FoxDifferential.zcFreeFoxCoordinatesStageMap

Documentation

Coordinatewise finite-stage projection on completed Fox vectors, induced by a coefficient ring map \(\mathbb{Z}_C\llbracket H\rrbracket \to (\mathbb{Z}/n\mathbb{Z})[F/N]\).

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]

Lean source · full declaration

def zcFreeFoxCoordinatesStageMap
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n) :
    ZCFreeFoxCoordinates C (X := X) (H := H) →+
      foxAlgebraicStageCoordinateVector (X := X) N n where
  toFun v := fun i : X => stageCoeff (v i)
  map_zero' := by
    funext i
    exact map_zero stageCoeff
  map_add' v w := by
    funext i
    exact map_add stageCoeff (v i) (w i)

theorem

zcFreeFoxCoordinatesStageMap_apply

L70 ↗

FoxDifferential.zcFreeFoxCoordinatesStageMap_apply

Documentation

The finite-stage map on completed Fox-coordinate vectors is computed coordinatewise by the underlying coefficient-stage map.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem zcFreeFoxCoordinatesStageMap_apply
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H))
    (i : X) :
    zcFreeFoxCoordinatesStageMap (C := C) (X := X) (H := H) N n stageCoeff v i =
      stageCoeff (v i)

theorem

zcFreeFoxCoordinatesStageMap_single

L86 ↗

FoxDifferential.zcFreeFoxCoordinatesStageMap_single

Documentation

The finite-stage coordinate map for completed free Fox coordinates has the stated value on a single generator.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [Fact (0 < n)] in

Lean source · statement

theorem zcFreeFoxCoordinatesStageMap_single
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (i : X) :
    zcFreeFoxCoordinatesStageMap (C := C) (X := X) (H := H) N n stageCoeff
        (Pi.single i (1 : ZCCompletedGroupAlgebra C H)) =
      Pi.single i (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)

theorem

zcFreeFoxCoordinatesStageMap_smul_groupLike

L106 ↗

FoxDifferential.zcFreeFoxCoordinatesStageMap_smul_groupLike

Documentation

If the coefficient projection sends completed group-like elements to finite quotient basis terms, then the coordinate projection respects the scalar action used in the Fox semidirect product.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem zcFreeFoxCoordinatesStageMap_smul_groupLike
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hgroupLike : ∀ h : H,
      stageCoeff (zcGroupLike C H h) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h))
    (h : H)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcFreeFoxCoordinatesStageMap (C := C) (X := X) (H := H) N n stageCoeff
        (zcGroupLike C H h • v) =
      (MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
        zcFreeFoxCoordinatesStageMap
          (C := C) (X := X) (H := H) N n stageCoeff v

theorem

finiteStageRight_comp_lift_eq_quotientMk

L134 ↗

FoxDifferential.finiteStageRight_comp_lift_eq_quotientMk

Documentation

Generator-level target compatibility implies word-level compatibility of the right finite quotient map with the free-group quotient map.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [DecidableEq X] [TopologicalSpace H] [IsTopologicalGroup H] in

Lean source · statement

theorem finiteStageRight_comp_lift_eq_quotientMk
    (φ : X → H)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hright_generators : ∀ i : X,
      stageRight (φ i) = QuotientGroup.mk' N (FreeGroup.of i))
    (w : FreeGroup X) :
    stageRight (FreeGroup.lift φ w) = QuotientGroup.mk' N w

theorem

foxAlgebraicStageFoxBoundary_zcFreeFoxCoordinatesStageMap

L156 ↗

FoxDifferential.foxAlgebraicStageFoxBoundary_zcFreeFoxCoordinatesStageMap

Documentation

Boundary compatibility from a coefficient projection whose group-like values agree with the finite quotient generators.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem foxAlgebraicStageFoxBoundary_zcFreeFoxCoordinatesStageMap
    [Fintype X]
    (φ : X → H)
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (hgroupLike_generators : ∀ i : X,
      stageCoeff (zcGroupLike C H (φ i)) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N)
          (QuotientGroup.mk' N (FreeGroup.of i)))
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    foxAlgebraicStageFoxBoundary (X := X) N n
        (zcFreeFoxCoordinatesStageMap (C := C) (X := X) (H := H) N n stageCoeff v) =
      stageCoeff
        (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v)

theorem

foxAlgebraicStageFoxBoundary_zcFreeFoxCoordinatesStageMap_of_groupLike

L190 ↗

FoxDifferential.foxAlgebraicStageFoxBoundary_zcFreeFoxCoordinatesStageMap_of_groupLike

Documentation

Boundary compatibility in the right-quotient form used by the semidirect stage maps.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem foxAlgebraicStageFoxBoundary_zcFreeFoxCoordinatesStageMap_of_groupLike
    [Fintype X]
    (φ : X → H)
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hgroupLike : ∀ h : H,
      stageCoeff (zcGroupLike C H h) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h))
    (hright_generators : ∀ i : X,
      stageRight (φ i) = QuotientGroup.mk' N (FreeGroup.of i))
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    foxAlgebraicStageFoxBoundary (X := X) N n
        (zcFreeFoxCoordinatesStageMap (C := C) (X := X) (H := H) N n stageCoeff v) =
      stageCoeff
        (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v)

theorem

zcFreeFoxCoordinatesStageMap_derivativeVector

L217 ↗

FoxDifferential.zcFreeFoxCoordinatesStageMap_derivativeVector

Documentation

The coordinate projection sends the completed free Fox derivative vector to the finite-stage Fox derivative vector.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [Fact (0 < n)] in

Lean source · statement

theorem zcFreeFoxCoordinatesStageMap_derivativeVector
    (φ : X → H)
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hgroupLike : ∀ h : H,
      stageCoeff (zcGroupLike C H h) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h))
    (hright_word : ∀ w : FreeGroup X,
      stageRight (FreeGroup.lift φ w) = QuotientGroup.mk' N w)
    (w : FreeGroup X) :
    zcFreeFoxCoordinatesStageMap (C := C) (X := X) (H := H) N n stageCoeff
        (zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w) =
      foxAlgebraicStageDerivativeVector (X := X) N n w

theorem

zcFreeFoxCoordinatesStageMap_derivativeVector_of_generators

L279 ↗

FoxDifferential.zcFreeFoxCoordinatesStageMap_derivativeVector_of_generators

Documentation

Generator-level right compatibility is enough for the derivative-vector projection formula.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [Fact (0 < n)] in

Lean source · statement

theorem zcFreeFoxCoordinatesStageMap_derivativeVector_of_generators
    (φ : X → H)
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hgroupLike : ∀ h : H,
      stageCoeff (zcGroupLike C H h) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h))
    (hright_generators : ∀ i : X,
      stageRight (φ i) = QuotientGroup.mk' N (FreeGroup.of i))
    (w : FreeGroup X) :
    zcFreeFoxCoordinatesStageMap (C := C) (X := X) (H := H) N n stageCoeff
        (zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w) =
      foxAlgebraicStageDerivativeVector (X := X) N n w

def

freeProCZCCompletedFoxSemidirectStageMapOfCoeff

L304 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectStageMapOfCoeff

Documentation

The semidirect finite-stage projection induced by a coefficient projection and a target quotient map.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]

Lean source · statement

def freeProCZCCompletedFoxSemidirectStageMapOfCoeff
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hgroupLike : ∀ h : H,
      stageCoeff (zcGroupLike C H h) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) :
    ZCCompletedFoxSemidirect C X H →*
      FoxAlgebraicStageSemidirect (X := X) N n

theorem

freeProCZCCompletedFoxSemidirectStageMapOfCoeff_left

L328 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectStageMapOfCoeff_left

Documentation

The left component of the semidirect finite-stage projection is obtained by applying the coefficient homomorphism stagewise while leaving the quotient support fixed.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem freeProCZCCompletedFoxSemidirectStageMapOfCoeff_left
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hgroupLike : ∀ h : H,
      stageCoeff (zcGroupLike C H h) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h))
    (y : ZCCompletedFoxSemidirect C X H) :
    (freeProCZCCompletedFoxSemidirectStageMapOfCoeff
      (C := C) (X := X) (H := H) N n stageCoeff stageRight hgroupLike y).left =
      zcFreeFoxCoordinatesStageMap (C := C) (X := X) (H := H) N n stageCoeff y.left

theorem

freeProCZCCompletedFoxSemidirectStageMapOfCoeff_right

L349 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectStageMapOfCoeff_right

Documentation

The right component of the semidirect finite-stage projection is the chosen target quotient map, independent of the coefficient projection.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem freeProCZCCompletedFoxSemidirectStageMapOfCoeff_right
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hgroupLike : ∀ h : H,
      stageCoeff (zcGroupLike C H h) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h))
    (y : ZCCompletedFoxSemidirect C X H) :
    (freeProCZCCompletedFoxSemidirectStageMapOfCoeff
      (C := C) (X := X) (H := H) N n stageCoeff stageRight hgroupLike y).right =
      stageRight y.right

theorem

freeProCZCCompletedFoxSemidirectStageMapOfCoeff_mem_finiteBoundaryCycleSet

L366 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectStageMapOfCoeff_mem_finiteBoundaryCycleSet

Documentation

Boundary-cycle preservation for the semidirect map built from a coefficient projection.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem freeProCZCCompletedFoxSemidirectStageMapOfCoeff_mem_finiteBoundaryCycleSet
    [Fintype X]
    (φ : X → H)
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hgroupLike : ∀ h : H,
      stageCoeff (zcGroupLike C H h) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h))
    (hright_generators : ∀ i : X,
      stageRight (φ i) = QuotientGroup.mk' N (FreeGroup.of i))
    {y : ZCCompletedFoxSemidirect C X H}
    (hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ) :
    freeProCZCCompletedFoxSemidirectStageMapOfCoeff
        (C := C) (X := X) (H := H) N n stageCoeff stageRight hgroupLike y ∈
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n

theorem

freeProCZCCompletedFoxSemidirectStageMapOfCoeff_kernelWordPoint

L399 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectStageMapOfCoeff_kernelWordPoint

Documentation

Kernel-word preservation for the semidirect map built from a coefficient projection.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
open ProCGroups.ProC
universe u
section CoordinateStageMap
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
omit [Fact (0 < n)] in

Lean source · statement

theorem freeProCZCCompletedFoxSemidirectStageMapOfCoeff_kernelWordPoint
    (φ : X → H)
    (stageCoeff :
      ZCCompletedGroupAlgebra C H →+*
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hgroupLike : ∀ h : H,
      stageCoeff (zcGroupLike C H h) =
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h))
    (hright_generators : ∀ i : X,
      stageRight (φ i) = QuotientGroup.mk' N (FreeGroup.of i))
    (w : FreeGroup X) :
    freeProCZCCompletedFoxSemidirectStageMapOfCoeff
        (C := C) (X := X) (H := H) N n stageCoeff stageRight hgroupLike
        (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
      foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w

Module documentation

Fox differential: completed — free pro-\(C\) — coordinate stage projection

Declarations