Module

BoundaryCycleHom.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycleHom

8 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — boundary cycle hom

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.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycles

Imported by2

abbrev

foxAlgebraicStageSourceKernel

L40 ↗

FoxDifferential.foxAlgebraicStageSourceKernel

Documentation

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

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

abbrev foxAlgebraicStageSourceKernel : Type u

def

foxAlgebraicStageSourceKernelDerivativeAddHom

L48 ↗

FoxDifferential.foxAlgebraicStageSourceKernelDerivativeAddHom

Documentation

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

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 · full declaration

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]

theorem

foxAlgebraicStageSourceKernelDerivativeAddHom_of

L78 ↗

FoxDifferential.foxAlgebraicStageSourceKernelDerivativeAddHom_of

Documentation

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

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 foxAlgebraicStageSourceKernelDerivativeAddHom_of
    (q : foxAlgebraicStageSourceKernel (X := X) N n) :
    foxAlgebraicStageSourceKernelDerivativeAddHom (X := X) N n (Additive.ofMul q) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n q.1

theorem

foxAlgebraicStageSourceKernelDerivativeAddHom_range_eq

L88 ↗

FoxDifferential.foxAlgebraicStageSourceKernelDerivativeAddHom_range_eq

Documentation

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.

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 foxAlgebraicStageSourceKernelDerivativeAddHom_range_eq :
    AddMonoidHom.range (foxAlgebraicStageSourceKernelDerivativeAddHom (X := X) N n) =
      foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n

def

foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles

L102 ↗

FoxDifferential.foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles

Documentation

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

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 · full declaration

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]

theorem

foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles_val

L136 ↗

FoxDifferential.foxAlgebraicStageSourceKernelDerivativeToBoundaryCycles_val

Documentation

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

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 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

theorem

foxAlgebraicStageBoundaryCyclesCovered_iff_surj_derivativeToBoundaryCycles

L147 ↗

FoxDifferential.foxAlgebraicStageBoundaryCyclesCovered_iff_surj_derivativeToBoundaryCycles

Documentation

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

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 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)

theorem

foxAlgebraicStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_of_surjective

L168 ↗

FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_of_surjective

Documentation

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

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 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))

Module documentation

Fox differential: completed — finite stage — boundary cycle hom

Declarations