ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycleHom

5 Theorems | 2 Definitions | 1 Abbreviation

The principal declarations in this module are:

foxAlgebraicStageSourceKernel The kernel of the finite source-to-target quotient \(F/[N,N]N^n \to F/N\). - foxAlgebraicStageSourceKernelDerivativeAddHom The descended finite-stage Fox derivative, restricted to the source quotient kernel, is an additive homomorphism. - foxAlgebraicStageSourceKernelDerivativeAddHom_of The finite-stage boundary or derivative construction defines the corresponding additive homomorphism. - foxAlgebraicStageSourceKernelDerivativeAddHom_range_eq The range of the additive source-kernel derivative map is exactly the source-kernel derivative additive subgroup already used in the finite-stage density target.

import

ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycles

Imported by

Abbreviation FoxDifferential.foxAlgebraicStageSourceKernel

abbrev foxAlgebraicStageSourceKernel : Type u :=
  (foxCommutatorPowerQuotientMapToNormalQuotient
    (F := FreeGroup X) N n).ker

The kernel of the finite source-to-target quotient \(F/[N,N]N^n \to F/N\).

Definition FoxDifferential.foxAlgebraicStageSourceKernelDerivativeAddHom

def foxAlgebraicStageSourceKernelDerivativeAddHom :
    Additive (foxAlgebraicStageSourceKernel (X := X) N n) →+
      foxAlgebraicStageCoordinateVector (X := X) N n where
  toFun q :=
    foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1
  map_zero' := by
    change foxAlgebraicStageQuotientDerivativeVector (X := X) N n
      (1 : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) = 0
    exact ScalarCrossedHom.map_one
      (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)
  map_add' := by
    intro q r
    change foxAlgebraicStageQuotientDerivativeVector (X := X) N n
        ((Additive.toMul q).1 * (Additive.toMul r).1) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1 +
        foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul r).1
    rw [ScalarCrossedHom.map_mul
      (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)]
    have hqcoeff :
        foxAlgebraicStageQuotientCoefficient (X := X) N n (Additive.toMul q).1 = 1 :=
      foxAlgebraicStageQuotientCoefficient_eq_one_of_kernel (X := X) N n
        (Additive.toMul q).2
    rw [hqcoeff]
    simp only [one_smul]

The descended finite-stage Fox derivative, restricted to the source quotient kernel, is an additive homomorphism.

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeAddHom_of

@[simp]
theorem foxAlgebraicStageSourceKernelDerivativeAddHom_of
    (q : foxAlgebraicStageSourceKernel (X := X) N n) :
    foxAlgebraicStageSourceKernelDerivativeAddHom (X := X) N n (Additive.ofMul q) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n q.1

The finite-stage boundary or derivative construction defines the corresponding additive homomorphism.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeAddHom_range_eq

theorem foxAlgebraicStageSourceKernelDerivativeAddHom_range_eq :
    AddMonoidHom.range (foxAlgebraicStageSourceKernelDerivativeAddHom (X := X) N n) =
      foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n

The range of the additive source-kernel derivative map is exactly the source-kernel derivative additive subgroup already used in the finite-stage density target.

Show Lean proof

Definition FoxDifferential.foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles

def foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles [Fintype X] :
    Additive (foxAlgebraicStageSourceKernel (X := X) N n) →+
      foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n where
  toFun q :=
    ⟨foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1,
      foxAlgebraicStageSourceKernelDerivativeSet_subset_boundaryCycleSubmodule (X := X) N n
        ⟨(Additive.toMul q).1, (Additive.toMul q).2, rfl⟩⟩
  map_zero' := by
    apply Subtype.ext
    change foxAlgebraicStageQuotientDerivativeVector (X := X) N n
      (1 : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) = 0
    exact ScalarCrossedHom.map_one
      (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)
  map_add' := by
    intro q r
    apply Subtype.ext
    change foxAlgebraicStageQuotientDerivativeVector (X := X) N n
        ((Additive.toMul q).1 * (Additive.toMul r).1) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1 +
        foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul r).1
    rw [ScalarCrossedHom.map_mul
      (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)]
    have hqcoeff :
        foxAlgebraicStageQuotientCoefficient (X := X) N n (Additive.toMul q).1 = 1 :=
      foxAlgebraicStageQuotientCoefficient_eq_one_of_kernel (X := X) N n
        (Additive.toMul q).2
    rw [hqcoeff]
    simp only [one_smul]

The source-kernel derivative map, with codomain restricted to finite Fox boundary cycles.

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles_val

@[simp]
theorem foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles_val
    [Fintype X] (q : foxAlgebraicStageSourceKernel (X := X) N n) :
    (foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles (X := X) N n
      (Additive.ofMul q) : foxAlgebraicStageCoordinateVector (X := X) N n) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n q.1

The map from the finite source kernel to boundary cycles has coordinates given by the finite-stage quotient derivative vector.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageBoundaryCyclesCovered_iff_surj_derivativeToBoundaryCycles

theorem foxAlgebraicStageBoundaryCyclesCovered_iff_surj_derivativeToBoundaryCycles
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔
      Function.Surjective
        (foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles (X := X) N n)

The finite-stage coverage statement is precisely surjectivity of the source-kernel derivative map onto the boundary-cycle subgroup.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_of_surjective

theorem foxAlgebraicStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_of_surjective
    [Fintype X]
    (hsurj : Function.Surjective
      (foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles (X := X) N n)) :
    foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n =
      (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n :
        Set (foxAlgebraicStageCoordinateVector (X := X) N n))

If the restricted source-kernel derivative map is surjective, then the source-kernel image is all of the finite boundary-cycle subgroup.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycleHom

Declarations