Module

SemidirectCycles.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.SemidirectCycles

16 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — semidirect cycles

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.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycleHom

Imported by5

def

foxAlgebraicStageSemidirectSourceKernelPoint

L37 ↗

FoxDifferential.foxAlgebraicStageSemidirectSourceKernelPoint

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSemidirectSourceKernelPoint
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    FoxAlgebraicStageSemidirect (X := X) N n

theorem

foxAlgebraicStageSemidirectSourceKernelPoint_left

L47 ↗

FoxDifferential.foxAlgebraicStageSemidirectSourceKernelPoint_left

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

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

theorem

foxAlgebraicStageSemidirectSourceKernelPoint_right

L58 ↗

FoxDifferential.foxAlgebraicStageSemidirectSourceKernelPoint_right

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSemidirectSourceKernelPoint_right
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    (foxAlgebraicStageSemidirectSourceKernelPoint (X := X) N n q).right = 1

def

foxAlgebraicStageSemidirectKernelWordPoint

L64 ↗

FoxDifferential.foxAlgebraicStageSemidirectKernelWordPoint

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSemidirectKernelWordPoint (w : FreeGroup X) :
    FoxAlgebraicStageSemidirect (X := X) N n

theorem

foxAlgebraicStageSemidirectKernelWordPoint_left

L73 ↗

FoxDifferential.foxAlgebraicStageSemidirectKernelWordPoint_left

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSemidirectKernelWordPoint_left (w : FreeGroup X) :
    (foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w).left =
      foxAlgebraicStageDerivativeVector (X := X) N n w

theorem

foxAlgebraicStageSemidirectKernelWordPoint_right

L83 ↗

FoxDifferential.foxAlgebraicStageSemidirectKernelWordPoint_right

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSemidirectKernelWordPoint_right (w : FreeGroup X) :
    (foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w).right = 1

def

foxAlgebraicStageSemidirectBoundaryCycleSet

L88 ↗

FoxDifferential.foxAlgebraicStageSemidirectBoundaryCycleSet

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSemidirectBoundaryCycleSet [Fintype X] :
    Set (FoxAlgebraicStageSemidirect (X := X) N n)

theorem

mem_foxAlgebraicStageSemidirectBoundaryCycleSet

L99 ↗

FoxDifferential.mem_foxAlgebraicStageSemidirectBoundaryCycleSet

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

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

def

foxAlgebraicStageSemidirectSourceKernelDerivativeSet

L107 ↗

FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSet

Documentation

Semidirect source-kernel derivative points in the finite stage.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSemidirectSourceKernelDerivativeSet :
    Set (FoxAlgebraicStageSemidirect (X := X) N n)

def

foxAlgebraicStageSemidirectKernelWordDerivativeSet

L114 ↗

FoxDifferential.foxAlgebraicStageSemidirectKernelWordDerivativeSet

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSemidirectKernelWordDerivativeSet :
    Set (FoxAlgebraicStageSemidirect (X := X) N n)

theorem

foxAlgebraicStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet

L120 ↗

FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet :
    foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n =
      foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) N n

theorem

foxAlgebraicStageSemidirectSourceKernelDerivativeSet_subset_boundaryCycleSet

L151 ↗

FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSet_subset_boundaryCycleSet

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSet_subset_boundaryCycleSet
    [Fintype X] :
    foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n ⊆
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n

theorem

foxAlgebraicStageSemidirectKernelWordDerivativeSet_subset_boundaryCycleSet

L164 ↗

FoxDifferential.foxAlgebraicStageSemidirectKernelWordDerivativeSet_subset_boundaryCycleSet

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSemidirectKernelWordDerivativeSet_subset_boundaryCycleSet
    [Fintype X] :
    foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) N n ⊆
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n

def

foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel

L177 ↗

FoxDifferential.foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel [Fintype X] : Prop

theorem

foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff

L182 ↗

FoxDifferential.foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

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

theorem

foxAlgebraicStageSemidirectBoundaryCyclesCoveredByKernelWords_iff

L206 ↗

FoxDifferential.foxAlgebraicStageSemidirectBoundaryCyclesCoveredByKernelWords_iff

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

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

Module documentation

Fox differential: completed — finite stage — semidirect cycles

Declarations