Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.FreeProC.StageProjection
ProCGroups/FoxDifferential/Completed/FreeProC/StageProjection

ProCGroups.FoxDifferential.Completed.FreeProC.StageProjection

15 Theorems | 1 Definition

The principal declarations in this module are:

  • freeProCZCCompletedFoxSemidirectStageMap A semidirect projection from the completed Fox semidirect product to a finite Fox stage, constructed from a left coordinate map and a right target quotient map. The only compatibility required is that the left coordinate map respects the scalar action used in semidirect multiplication. This is the abstract form of the finite quotient map \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H \to ((\mathbb{Z}/n\mathbb{Z})[F/N])^X \rtimes F/N\). - freeProCZCCompletedFoxSemidirectStageMap_left The left component of the completed-to-finite semidirect stage map is the prescribed finite Fox coordinate projection. - freeProCZCCompletedFoxSemidirectStageMap_right The right coordinate of the completed Fox semidirect stage map is the selected target quotient map. - freeProCZCCompletedFoxSemidirectStageMap_mem_ker_iff Membership in the kernel of the completed Fox semidirect stage map is equivalent to vanishing of the corresponding finite-stage coordinate.
imports
Imported by

Declarations

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectStageMap 
def freeProCZCCompletedFoxSemidirectStageMap
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v) :
    ZCCompletedFoxSemidirect C X H →*
      FoxAlgebraicStageSemidirect (X := X) N n where
  toFun y :=
    { left := stageLeft y.left
      right := stageRight y.right }
  map_one' := by
    apply FoxAlgebraicStageSemidirect.ext
    · change stageLeft 0 = 0
      exact map_zero stageLeft
    · exact map_one stageRight
  map_mul' a b := by
    apply FoxAlgebraicStageSemidirect.ext
    · change
        stageLeft (a.left + zcGroupLike C H a.right • b.left) =
          stageLeft a.left +
            (MonoidAlgebra.of (ModNCompletedCoeff n)
              (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight a.right)) •
              stageLeft b.left
      rw [map_add, hscalar]
    · change stageRight (a.right * b.right) = stageRight a.right * stageRight b.right
      exact map_mul stageRight a.right b.right

A semidirect projection from the completed Fox semidirect product to a finite Fox stage, constructed from a left coordinate map and a right target quotient map. The only compatibility required is that the left coordinate map respects the scalar action used in semidirect multiplication. This is the abstract form of the finite quotient map \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H \to ((\mathbb{Z}/n\mathbb{Z})[F/N])^X \rtimes F/N\).

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectStageMap_left 
omit [DecidableEq X] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectStageMap_left
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (y : ZCCompletedFoxSemidirect C X H) :
    (freeProCZCCompletedFoxSemidirectStageMap
      (C := C) (X := X) (H := H) N n stageLeft stageRight hscalar y).left =
      stageLeft y.left

The left component of the completed-to-finite semidirect stage map is the prescribed finite Fox coordinate projection.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectStageMap_right 
omit [DecidableEq X] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectStageMap_right
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (y : ZCCompletedFoxSemidirect C X H) :
    (freeProCZCCompletedFoxSemidirectStageMap
      (C := C) (X := X) (H := H) N n stageLeft stageRight hscalar y).right =
      stageRight y.right

The right coordinate of the completed Fox semidirect stage map is the selected target quotient map.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectStageMap_mem_ker_iff 
omit [DecidableEq X] in
theorem freeProCZCCompletedFoxSemidirectStageMap_mem_ker_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N n}
    {stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N}
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    {y : ZCCompletedFoxSemidirect C X H} :
    y ∈ (freeProCZCCompletedFoxSemidirectStageMap
        (C := C) (X := X) (H := H) N n stageLeft stageRight hscalar).ker ↔
      stageLeft y.left = 0 ∧ stageRight y.right = 1

Membership in the kernel of the completed Fox semidirect stage map is equivalent to vanishing of the corresponding finite-stage coordinate.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectStageMap_mem_finiteBoundaryCycleSet 
omit [DecidableEq X] in
theorem freeProCZCCompletedFoxSemidirectStageMap_mem_finiteBoundaryCycleSet
    [Fintype X]
    (φ : X → H)
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (stageBoundary :
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    (hboundary :
      ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
        foxAlgebraicStageFoxBoundary (X := X) N n (stageLeft v) =
          stageBoundary
            (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    {y : ZCCompletedFoxSemidirect C X H}
    (hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ) :
    freeProCZCCompletedFoxSemidirectStageMap
        (C := C) (X := X) (H := H) N n stageLeft stageRight hscalar y ∈
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n

A completed boundary-cycle point projects to a finite boundary-cycle point once the left coordinate projection commutes with the source-shaped Fox boundary.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectStageMap_kernelWordPoint 
theorem freeProCZCCompletedFoxSemidirectStageMap_kernelWordPoint
    (φ : X → H)
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (hderivative :
      ∀ w : FreeGroup X,
        stageLeft
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) N n w)
    (w : FreeGroup X) :
    freeProCZCCompletedFoxSemidirectStageMap
        (C := C) (X := X) (H := H) N n stageLeft stageRight hscalar
        (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
      foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w

The stage map sends the completed kernel-word point \((D w, 1)\) to the corresponding finite kernel-word point, provided the left coordinate projection commutes with Fox derivatives.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint 
theorem freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint
    (φ : X → H)
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (hderivative :
      ∀ w : FreeGroup X,
        stageLeft
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) N n w)
    (w : FreeGroup X) :
    freeProCZCCompletedFoxSemidirectStageMap
        (C := C) (X := X) (H := H) N n stageLeft stageRight hscalar
        (freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w) =
      ({ left := foxAlgebraicStageDerivativeVector (X := X) N n w,
         right := stageRight (FreeGroup.lift φ w) } :
        FoxAlgebraicStageSemidirect (X := X) N n)

The stage map sends a completed graph-word point \((D w,\varphi(w))\) to the corresponding finite stage graph point.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint_of_stage_kernel 
theorem freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint_of_stage_kernel
    (φ : X → H)
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N n)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (hderivative :
      ∀ w : FreeGroup X,
        stageLeft
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) N n w)
    (hright_word :
      ∀ w : FreeGroup X, stageRight (FreeGroup.lift φ w) = QuotientGroup.mk' N w)
    (w : FreeGroup X) (hw : w ∈ N) :
    freeProCZCCompletedFoxSemidirectStageMap
        (C := C) (X := X) (H := H) N n stageLeft stageRight hscalar
        (freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w) =
      foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w

If a word is in the finite-stage relation subgroup, the stage image of its completed graph point is the finite kernel-word point.

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stageMaps_relDeriv 
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stageMaps_relDeriv
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (stageLeft : ∀ j : J,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
    (stageRight : ∀ j : J,
      H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
    (hscalar :
      ∀ j : J, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft j (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
            (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
            stageLeft j v)
    (hquotient_basis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun j : J =>
          freeProCZCCompletedFoxSemidirectStageMap
            (C := C) (X := X) (H := H) (Nstage j) (nstage j)
            (stageLeft j) (stageRight j) (hscalar j)))
    (stageBoundary : ∀ j : J,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
    (hboundary :
      ∀ j : J,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
            stageBoundary j
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hderivative :
      ∀ j : J, ∀ w : FreeGroup X,
        stageLeft j
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)

Completed Fox density from concrete completed-to-finite semidirect stage maps, using finite-stage relation-ideal derivative exactness and the boundary and derivative projection formulas.

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_stageMaps_relDeriv 
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_stageMaps_relDeriv
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (stageLeft : ∀ j : J,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
    (stageRight : ∀ j : J,
      H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
    (hscalar :
      ∀ j : J, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft j (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
            (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
            stageLeft j v)
    (hquotient_basis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun j : J =>
          freeProCZCCompletedFoxSemidirectStageMap
            (C := C) (X := X) (H := H) (Nstage j) (nstage j)
            (stageLeft j) (stageRight j) (hscalar j)))
    (stageBoundary : ∀ j : J,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
    (hboundary :
      ∀ j : J,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
            stageBoundary j
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hright_word :
      ∀ j : J, ∀ w : FreeGroup X,
        stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)
    (hderivative :
      ∀ j : J, ∀ w : FreeGroup X,
        stageLeft j
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ)

Completed graph-word density for concrete completed-to-finite semidirect stage maps, without requiring finite-stage relation words to be genuine kernel words for \(\varphi\).

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_graphRelDeriv 
theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_graphRelDeriv
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (stageLeft : ∀ j : J,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
    (stageRight : ∀ j : J,
      H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
    (hscalar :
      ∀ j : J, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft j (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
            (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
            stageLeft j v)
    (hquotient_basis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun j : J =>
          freeProCZCCompletedFoxSemidirectStageMap
            (C := C) (X := X) (H := H) (Nstage j) (nstage j)
            (stageLeft j) (stageRight j) (hscalar j)))
    (stageBoundary : ∀ j : J,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
    (hboundary :
      ∀ j : J,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
            stageBoundary j
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hright_word :
      ∀ j : J, ∀ w : FreeGroup X,
        stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)
    (hderivative :
      ∀ j : J, ∀ w : FreeGroup X,
        stageLeft j
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

Concrete stage-map graph-word density, phrased as closed-generated-target membership.

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_relDeriv 
theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_relDeriv
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (stageLeft : ∀ j : J,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
    (stageRight : ∀ j : J,
      H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
    (hscalar :
      ∀ j : J, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft j (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
            (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
            stageLeft j v)
    (hquotient_basis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun j : J =>
          freeProCZCCompletedFoxSemidirectStageMap
            (C := C) (X := X) (H := H) (Nstage j) (nstage j)
            (stageLeft j) (stageRight j) (hscalar j)))
    (stageBoundary : ∀ j : J,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
    (hboundary :
      ∀ j : J,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
            stageBoundary j
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hderivative :
      ∀ j : J, ∀ w : FreeGroup X,
        stageLeft j
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

The same concrete stage-map route, with the conclusion phrased as membership in the closed-generated Fox graph target.

Show Lean proof
Theorem FoxDifferential.boundaryCycles_subset_kernelClosure_of_stageMaps 
theorem boundaryCycles_subset_kernelClosure_of_stageMaps
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (stageLeft : ∀ j : J,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
    (stageRight : ∀ j : J,
      H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
    (hscalar :
      ∀ j : J, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft j (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
            (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
            stageLeft j v)
    (hidentity_basis :
      HasIdentityQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun j : J =>
          freeProCZCCompletedFoxSemidirectStageMap
            (C := C) (X := X) (H := H) (Nstage j) (nstage j)
            (stageLeft j) (stageRight j) (hscalar j)))
    (stageBoundary : ∀ j : J,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
    (hboundary :
      ∀ j : J,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
            stageBoundary j
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hderivative :
      ∀ j : J, ∀ w : FreeGroup X,
        stageLeft j
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)

Stage-map density is formulated using identity-neighborhood kernels rather than left-coset kernels. This is the topological form produced by separation through finite quotients in profinite groups. The conversion to the left-coset closure basis is performed internally.

Show Lean proof
Theorem FoxDifferential.boundaryCycles_subset_graphWordClosure_of_stageMaps 
theorem boundaryCycles_subset_graphWordClosure_of_stageMaps
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (stageLeft : ∀ j : J,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
    (stageRight : ∀ j : J,
      H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
    (hscalar :
      ∀ j : J, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft j (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
            (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
            stageLeft j v)
    (hidentity_basis :
      HasIdentityQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun j : J =>
          freeProCZCCompletedFoxSemidirectStageMap
            (C := C) (X := X) (H := H) (Nstage j) (nstage j)
            (stageLeft j) (stageRight j) (hscalar j)))
    (stageBoundary : ∀ j : J,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
    (hboundary :
      ∀ j : J,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
            stageBoundary j
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hright_word :
      ∀ j : J, ∀ w : FreeGroup X,
        stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)
    (hderivative :
      ∀ j : J, ∀ w : FreeGroup X,
        stageLeft j
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ)

Graph-word density using identity-neighborhood kernels rather than left-coset kernels.

Show Lean proof
Theorem FoxDifferential.boundaryCycles_subset_closedGenTarget_of_stageGraph 
theorem boundaryCycles_subset_closedGenTarget_of_stageGraph
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (stageLeft : ∀ j : J,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
    (stageRight : ∀ j : J,
      H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
    (hscalar :
      ∀ j : J, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft j (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
            (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
            stageLeft j v)
    (hidentity_basis :
      HasIdentityQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun j : J =>
          freeProCZCCompletedFoxSemidirectStageMap
            (C := C) (X := X) (H := H) (Nstage j) (nstage j)
            (stageLeft j) (stageRight j) (hscalar j)))
    (stageBoundary : ∀ j : J,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
    (hboundary :
      ∀ j : J,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
            stageBoundary j
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hright_word :
      ∀ j : J, ∀ w : FreeGroup X,
        stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)
    (hderivative :
      ∀ j : J, ∀ w : FreeGroup X,
        stageLeft j
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

Closed-generated-target version of the identity-kernel graph-word stage-map theorem.

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_identityKernel_relDeriv 
theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_identityKernel_relDeriv
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (stageLeft : ∀ j : J,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
    (stageRight : ∀ j : J,
      H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
    (hscalar :
      ∀ j : J, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft j (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
            (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
            stageLeft j v)
    (hidentity_basis :
      HasIdentityQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun j : J =>
          freeProCZCCompletedFoxSemidirectStageMap
            (C := C) (X := X) (H := H) (Nstage j) (nstage j)
            (stageLeft j) (stageRight j) (hscalar j)))
    (stageBoundary : ∀ j : J,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
    (hboundary :
      ∀ j : J,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
            stageBoundary j
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hderivative :
      ∀ j : J, ∀ w : FreeGroup X,
        stageLeft j
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

Closed-generated-target version of the identity-kernel stage-map density theorem.

Show Lean proof