Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.FiniteStage.TargetMap
ProCGroups/FoxDifferential/Completed/FiniteStage/TargetMap

ProCGroups.FoxDifferential.Completed.FiniteStage.TargetMap

9 Theorems

The principal declarations in this module are:

  • foxAlgebraicStageSemidirectMap_left The left coordinate of the finite-stage semidirect point is the specified derivative component. - foxAlgebraicStageSemidirectMap_right The right coordinate of the finite-stage semidirect point is the corresponding quotient component. - foxAlgebraicStageFoxBoundary_targetMap Target-quotient refinement commutes with the finite-stage Fox boundary. - foxAlgebraicStageBoundaryCycleSubmodule_targetMap_mem Target-quotient refinement sends finite boundary cycles to finite boundary cycles.
import
Imported by

Declarations

Theorem FoxDifferential.foxAlgebraicStageSemidirectMap_left 
omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageSemidirectMap_left
    (y : FoxAlgebraicStageSemidirect (X := X) N n) :
    (foxAlgebraicStageSemidirectMap (X := X) hNM n y).left =
      fun i : X => foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n (y.left i)

The left coordinate of the finite-stage semidirect point is the specified derivative component.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectMap_right 
omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageSemidirectMap_right
    (y : FoxAlgebraicStageSemidirect (X := X) N n) :
    (foxAlgebraicStageSemidirectMap (X := X) hNM n y).right =
      foxAlgebraicStageTargetQuotientMap (X := X) hNM y.right

The right coordinate of the finite-stage semidirect point is the corresponding quotient component.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageFoxBoundary_targetMap 
omit [DecidableEq X] in
theorem foxAlgebraicStageFoxBoundary_targetMap
    [Fintype X]
    (v : foxAlgebraicStageCoordinateVector (X := X) N n) :
    foxAlgebraicStageFoxBoundary (X := X) M n
        (fun i : X => foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n (v i)) =
      foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n
        (foxAlgebraicStageFoxBoundary (X := X) N n v)

Target-quotient refinement commutes with the finite-stage Fox boundary.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageBoundaryCycleSubmodule_targetMap_mem 
omit [DecidableEq X] in
theorem foxAlgebraicStageBoundaryCycleSubmodule_targetMap_mem
    [Fintype X]
    {v : foxAlgebraicStageCoordinateVector (X := X) N n}
    (hv : v ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n) :
    (fun i : X => foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n (v i)) ∈
      foxAlgebraicStageBoundaryCycleSubmodule (X := X) M n

Target-quotient refinement sends finite boundary cycles to finite boundary cycles.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectMap_mem_boundaryCycleSet 
omit [DecidableEq X] in
theorem foxAlgebraicStageSemidirectMap_mem_boundaryCycleSet
    [Fintype X]
    {y : FoxAlgebraicStageSemidirect (X := X) N n}
    (hy : y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n) :
    foxAlgebraicStageSemidirectMap (X := X) hNM n y ∈
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) M n

Target-quotient refinement sends semidirect boundary-cycle points to boundary-cycle points.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectMap_kernelWordPoint 
theorem foxAlgebraicStageSemidirectMap_kernelWordPoint
    (w : FreeGroup X) :
    foxAlgebraicStageSemidirectMap (X := X) hNM n
        (foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w) =
      foxAlgebraicStageSemidirectKernelWordPoint (X := X) M n w

Target-quotient refinement sends finite kernel-word points to finite kernel-word points.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectMap_sourceKernelPoint 
theorem foxAlgebraicStageSemidirectMap_sourceKernelPoint
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSemidirectMap (X := X) hNM n
        (foxAlgebraicStageSemidirectSourceKernelPoint (X := X) N n q) =
      foxAlgebraicStageSemidirectSourceKernelPoint (X := X) M n
        (foxAlgebraicStageSourceQuotientMap (X := X) hNM n q)

Target-quotient refinement sends finite source-kernel semidirect points to source-kernel semidirect points.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectMap_kernelWordDerivativeSet_subset 
theorem foxAlgebraicStageSemidirectMap_kernelWordDerivativeSet_subset :
    (fun y : FoxAlgebraicStageSemidirect (X := X) N n =>
        foxAlgebraicStageSemidirectMap (X := X) hNM n y) ''
      foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) N n ⊆
        foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) M n

Target refinement sends the finite semidirect kernel-word derivative set into the refined one.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectMap_sourceKernelDerivativeSet_subset 
theorem foxAlgebraicStageSemidirectMap_sourceKernelDerivativeSet_subset :
    (fun y : FoxAlgebraicStageSemidirect (X := X) N n =>
        foxAlgebraicStageSemidirectMap (X := X) hNM n y) ''
      foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n ⊆
        foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) M n

Target refinement sends source-kernel derivative points into source-kernel derivative points.

Show Lean proof