FoxDifferential.Completed.FiniteStage.SemidirectCycles

10 Theorem | 6 Definition

This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.

Open this file on GitHub

import

FoxDifferential.Completed.FiniteStage.BoundaryCycleHom

Imported by

Definition FoxDifferential.finiteFoxStageSemidirectSourceKernelPoint GitHub

def finiteFoxStageSemidirectSourceKernelPoint
    (q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    FiniteFoxStageSemidirect (X := X) N n :=
  { left := finiteFoxStageQuotientDerivativeVector (X := X) N n q,
    right := 1 }

@[simp]

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

Theorem FoxDifferential.finiteFoxStageSemidirectSourceKernelPoint_left GitHub

theorem finiteFoxStageSemidirectSourceKernelPoint_left
    (q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    (finiteFoxStageSemidirectSourceKernelPoint (X := X) N n q).left =
      finiteFoxStageQuotientDerivativeVector (X := X) N n q

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

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectSourceKernelPoint_right GitHub

theorem finiteFoxStageSemidirectSourceKernelPoint_right
    (q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    (finiteFoxStageSemidirectSourceKernelPoint (X := X) N n q).right = 1

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

Show proof

Definition FoxDifferential.finiteFoxStageSemidirectKernelWordPoint GitHub

def finiteFoxStageSemidirectKernelWordPoint (w : FreeGroup X) :
    FiniteFoxStageSemidirect (X := X) N n :=
  { left := finiteFoxStageDerivativeVector (X := X) N n w,
    right := 1 }

@[simp]

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

Theorem FoxDifferential.finiteFoxStageSemidirectKernelWordPoint_left GitHub

theorem finiteFoxStageSemidirectKernelWordPoint_left (w : FreeGroup X) :
    (finiteFoxStageSemidirectKernelWordPoint (X := X) N n w).left =
      finiteFoxStageDerivativeVector (X := X) N n w

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

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectKernelWordPoint_right GitHub

theorem finiteFoxStageSemidirectKernelWordPoint_right (w : FreeGroup X) :
    (finiteFoxStageSemidirectKernelWordPoint (X := X) N n w).right = 1

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

Show proof

Definition FoxDifferential.finiteFoxStageSemidirectBoundaryCycleSet GitHub

def finiteFoxStageSemidirectBoundaryCycleSet [Fintype X] :
    Set (FiniteFoxStageSemidirect (X := X) N n) :=
  { y | y.right = 1 ∧
      y.left ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n }

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

Theorem FoxDifferential.mem_finiteFoxStageSemidirectBoundaryCycleSet GitHub

theorem mem_finiteFoxStageSemidirectBoundaryCycleSet [Fintype X]
    {y : FiniteFoxStageSemidirect (X := X) N n} :
    y ∈ finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n ↔
      y.right = 1 ∧ y.left ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n

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

Show proof

Definition FoxDifferential.finiteFoxStageSemidirectSourceKernelDerivativeSet GitHub

def finiteFoxStageSemidirectSourceKernelDerivativeSet :
    Set (FiniteFoxStageSemidirect (X := X) N n) :=
  { y | ∃ q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n,
      finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1 ∧
        finiteFoxStageSemidirectSourceKernelPoint (X := X) N n q = y }

Semidirect source-kernel derivative points in the finite stage.

Definition FoxDifferential.finiteFoxStageSemidirectKernelWordDerivativeSet GitHub

def finiteFoxStageSemidirectKernelWordDerivativeSet :
    Set (FiniteFoxStageSemidirect (X := X) N n) :=
  { y | ∃ w : FreeGroup X,
      w ∈ N ∧ finiteFoxStageSemidirectKernelWordPoint (X := X) N n w = y }

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

Theorem FoxDifferential.finiteFoxStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet GitHub

theorem finiteFoxStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet :
    finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n =
      finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N n

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

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectSourceKernelDerivativeSet_subset_boundaryCycleSet GitHub

theorem finiteFoxStageSemidirectSourceKernelDerivativeSet_subset_boundaryCycleSet
    [Fintype X] :
    finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n ⊆
      finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n

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

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectKernelWordDerivativeSet_subset_boundaryCycleSet GitHub

theorem finiteFoxStageSemidirectKernelWordDerivativeSet_subset_boundaryCycleSet
    [Fintype X] :
    finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N n ⊆
      finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n

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

Show proof

Definition FoxDifferential.finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel GitHub

def finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel [Fintype X] : Prop :=
  finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n ⊆
    finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n

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

Theorem FoxDifferential.finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff GitHub

theorem finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff
    [Fintype X] :
    finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔
      finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

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

Show proof

Theorem FoxDifferential.finiteFoxStageSemidirectBoundaryCyclesCoveredByKernelWords_iff GitHub

theorem finiteFoxStageSemidirectBoundaryCyclesCoveredByKernelWords_iff
    [Fintype X] :
    finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n ⊆
        finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N n ↔
      finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

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

Show proof

FoxDifferential.Completed.FiniteStage.SemidirectCycles

Declarations