FoxDifferential.Completed.FiniteStage.CoeffMap.BoundaryCycles

7 Theorem

Fox Differential / Completed / Finite Stage / Coefficient Map / Boundary Cycles.

import

Imported by

Theorem FoxDifferential.finiteFoxStageSemidirectCoeffMap_left GitHub

theorem finiteFoxStageSemidirectCoeffMap_left
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (y : FiniteFoxStageSemidirect (X := X) N m₀) :
    (finiteFoxStageSemidirectCoeffMap (X := X) N hnm y).left =
      fun i : X => finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm (y.left i)

The left component of finite-stage semidirect coefficient reduction is obtained by reducing each coordinate coefficient.

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectCoeffMap_right GitHub

theorem finiteFoxStageSemidirectCoeffMap_right
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (y : FiniteFoxStageSemidirect (X := X) N m₀) :
    (finiteFoxStageSemidirectCoeffMap (X := X) N hnm y).right = y.right

The right component of finite-stage semidirect coefficient reduction is unchanged.

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectCoeffMap_rfl GitHub

theorem finiteFoxStageSemidirectCoeffMap_rfl
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    finiteFoxStageSemidirectCoeffMap
        (X := X) (n₀ := n₀) (m₀ := n₀) N dvd_rfl =
      MonoidHom.id (FiniteFoxStageSemidirect (X := X) N n₀)

Coefficient reduction is the identity on finite-stage semidirect targets when the modulus is unchanged.

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectCoeffMap_comp GitHub

theorem finiteFoxStageSemidirectCoeffMap_comp
    {k₀ : ℕ} [Fact (0 < k₀)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (hnm : n₀ ∣ m₀) (hmk : m₀ ∣ k₀) :
    (finiteFoxStageSemidirectCoeffMap (X := X) N hnm).comp
        (finiteFoxStageSemidirectCoeffMap (X := X) N hmk) =
      finiteFoxStageSemidirectCoeffMap (X := X) N (dvd_trans hnm hmk)

Coefficient reductions compose on finite-stage semidirect targets.

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectCoeffMap_mem_boundaryCycleSet GitHub

theorem finiteFoxStageSemidirectCoeffMap_mem_boundaryCycleSet
    [Fintype X]
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    {y : FiniteFoxStageSemidirect (X := X) N m₀}
    (hy : y ∈ finiteFoxStageSemidirectBoundaryCycleSet (X := X) N m₀) :
    finiteFoxStageSemidirectCoeffMap (X := X) N hnm y ∈
      finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n₀

Coefficient reduction carries finite semidirect boundary cycles to finite semidirect boundary cycles.

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectCoeffMap_kernelWordPoint GitHub

theorem finiteFoxStageSemidirectCoeffMap_kernelWordPoint
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (w : FreeGroup X) :
    finiteFoxStageSemidirectCoeffMap (X := X) N hnm
        (finiteFoxStageSemidirectKernelWordPoint (X := X) N m₀ w) =
      finiteFoxStageSemidirectKernelWordPoint (X := X) N n₀ w

Coefficient reduction sends the finite semidirect kernel-word point at modulus \(m\) to the corresponding point at modulus \(n\).

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectCoeffMap_kernelWordDerivativeSet_subset GitHub

theorem finiteFoxStageSemidirectCoeffMap_kernelWordDerivativeSet_subset
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) :
    (fun y : FiniteFoxStageSemidirect (X := X) N m₀ =>
        finiteFoxStageSemidirectCoeffMap (X := X) N hnm y) ''
      finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N m₀ ⊆
        finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N n₀

Coefficient reduction sends the finite semidirect kernel-word derivative set at modulus \(m\) into the corresponding set at modulus \(n\).

Show proof

FoxDifferential.Completed.FiniteStage.CoeffMap.BoundaryCycles

Declarations