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

ProCGroups.FoxDifferential.Completed.FiniteStage.SemidirectCycles

10 Theorems | 6 Definitions

The principal declarations in this module are:

  • foxAlgebraicStageSemidirectSourceKernelPoint The finite semidirect point \((Dq,1)\) attached to a source-quotient element. - foxAlgebraicStageSemidirectKernelWordPoint The finite semidirect point (Dw,1) attached to a word. - foxAlgebraicStageSemidirectSourceKernelPoint_left The left coordinate of the finite-stage semidirect point is the specified derivative component. - foxAlgebraicStageSemidirectSourceKernelPoint_right The right coordinate of the finite-stage semidirect point is the corresponding quotient component.
import
Imported by

Declarations

Definition FoxDifferential.foxAlgebraicStageSemidirectSourceKernelPoint 
def foxAlgebraicStageSemidirectSourceKernelPoint
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    FoxAlgebraicStageSemidirect (X := X) N n :=
  { left := foxAlgebraicStageQuotientDerivativeVector (X := X) N n q,
    right := 1 }

The finite semidirect point \((Dq,1)\) attached to a source-quotient element.

Theorem FoxDifferential.foxAlgebraicStageSemidirectSourceKernelPoint_left 
@[simp]
theorem foxAlgebraicStageSemidirectSourceKernelPoint_left
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    (foxAlgebraicStageSemidirectSourceKernelPoint (X := X) N n q).left =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n q

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

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectSourceKernelPoint_right 
@[simp]
theorem foxAlgebraicStageSemidirectSourceKernelPoint_right
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    (foxAlgebraicStageSemidirectSourceKernelPoint (X := X) N n q).right = 1

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

Show Lean proof
Definition FoxDifferential.foxAlgebraicStageSemidirectKernelWordPoint 
def foxAlgebraicStageSemidirectKernelWordPoint (w : FreeGroup X) :
    FoxAlgebraicStageSemidirect (X := X) N n :=
  { left := foxAlgebraicStageDerivativeVector (X := X) N n w,
    right := 1 }

The finite semidirect point (Dw,1) attached to a word.

Theorem FoxDifferential.foxAlgebraicStageSemidirectKernelWordPoint_left 
@[simp]
theorem foxAlgebraicStageSemidirectKernelWordPoint_left (w : FreeGroup X) :
    (foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w).left =
      foxAlgebraicStageDerivativeVector (X := X) N n w

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

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectKernelWordPoint_right 
@[simp]
theorem foxAlgebraicStageSemidirectKernelWordPoint_right (w : FreeGroup X) :
    (foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w).right = 1

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

Show Lean proof
Definition FoxDifferential.foxAlgebraicStageSemidirectBoundaryCycleSet 
def foxAlgebraicStageSemidirectBoundaryCycleSet [Fintype X] :
    Set (FoxAlgebraicStageSemidirect (X := X) N n) :=
  { y | y.right = 1 ∧
      y.left ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n }

Finite-stage boundary cycles as semidirect points \((v,1)\) with \(\partial v = 0\).

Theorem FoxDifferential.mem_foxAlgebraicStageSemidirectBoundaryCycleSet 
omit [DecidableEq X] in
@[simp]
theorem mem_foxAlgebraicStageSemidirectBoundaryCycleSet
    (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ) [Fintype X]
    {y : FoxAlgebraicStageSemidirect (X := X) N n} :
    y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n ↔
      y.right = 1 ∧ y.left ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n

Membership in the finite-stage boundary-cycle object is characterized by the corresponding boundary-vanishing condition.

Show Lean proof
Definition FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSet 
def foxAlgebraicStageSemidirectSourceKernelDerivativeSet :
    Set (FoxAlgebraicStageSemidirect (X := X) N n) :=
  { y | ∃ q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n,
      foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1 ∧
        foxAlgebraicStageSemidirectSourceKernelPoint (X := X) N n q = y }

Semidirect source-kernel derivative points in the finite stage.

Definition FoxDifferential.foxAlgebraicStageSemidirectKernelWordDerivativeSet 
def foxAlgebraicStageSemidirectKernelWordDerivativeSet :
    Set (FoxAlgebraicStageSemidirect (X := X) N n) :=
  { y | ∃ w : FreeGroup X,
      w ∈ N ∧ foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w = y }

This set consists of semidirect kernel-word derivative points at the finite Fox stage.

Theorem FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet 
theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet :
    foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n =
      foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) N n

Source-kernel semidirect points and actual kernel-word semidirect points coincide.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSet_subset_boundaryCycleSet 
theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSet_subset_boundaryCycleSet
    [Fintype X] :
    foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n ⊆
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n

Every finite semidirect source-kernel derivative point is a semidirect boundary cycle.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectKernelWordDerivativeSet_subset_boundaryCycleSet 
theorem foxAlgebraicStageSemidirectKernelWordDerivativeSet_subset_boundaryCycleSet
    [Fintype X] :
    foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) N n ⊆
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n

Every finite semidirect kernel-word derivative point is a semidirect boundary cycle.

Show Lean proof
Definition FoxDifferential.foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel 
def foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel [Fintype X] : Prop :=
  foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n ⊆
    foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n

Semidirect finite-stage coverage: every semidirect boundary cycle is represented by a source-kernel derivative point.

Theorem FoxDifferential.foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff 
theorem foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔
      foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

The semidirect finite-stage coverage target is equivalent to the coordinate coverage target.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageSemidirectBoundaryCyclesCoveredByKernelWords_iff 
theorem foxAlgebraicStageSemidirectBoundaryCyclesCoveredByKernelWords_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n ⊆
        foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) N n ↔
      foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

Finite-stage semidirect coverage is equivalent to coverage by actual kernel words.

Show Lean proof