ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycles

8 Theorems | 5 Definitions

The principal declarations in this module are:

foxAlgebraicStageBoundaryCycleSubmodule The finite-stage Fox boundary-cycle submodule \(\ker \partial\). - foxAlgebraicStageSourceKernelDerivativeSet Quotient-level source-kernel derivatives in the finite stage. These are the finite-stage relation cycles coming from the kernel of \(F/[N,N]N^n \to F/N\). - mem_foxAlgebraicStageBoundaryCycleSubmodule Membership in the finite-stage boundary-cycle object is characterized by the corresponding boundary-vanishing condition. - foxAlgebraicStageCoefficient_eq_one_of_mem A word lying in the normal subgroup \(N\) has finite-stage coefficient equal to \(1\) in the quotient by \(N\).

import

ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Derivative.Quotient.Fundamental

Imported by

Definition FoxDifferential.foxAlgebraicStageBoundaryCycleSubmodule

def foxAlgebraicStageBoundaryCycleSubmodule [Fintype X] :
    Submodule (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n) :=
  LinearMap.ker (foxAlgebraicStageFoxBoundary (X := X) N n)

The finite-stage Fox boundary-cycle submodule \(\ker \partial\).

Theorem FoxDifferential.mem_foxAlgebraicStageBoundaryCycleSubmodule

omit [DecidableEq X] in
@[simp]
theorem mem_foxAlgebraicStageBoundaryCycleSubmodule [Fintype X]
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {v : foxAlgebraicStageCoordinateVector (X := X) N n} :
    v ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n ↔
      foxAlgebraicStageFoxBoundary (X := X) N n v = 0

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

Show Lean proof

Definition FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet

def foxAlgebraicStageSourceKernelDerivativeSet :
    Set (foxAlgebraicStageCoordinateVector (X := X) N n) :=
  { v | ∃ q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n,
      foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1 ∧
        foxAlgebraicStageQuotientDerivativeVector (X := X) N n q = v }

Quotient-level source-kernel derivatives in the finite stage. These are the finite-stage relation cycles coming from the kernel of \(F/[N,N]N^n \to F/N\).

Definition FoxDifferential.foxAlgebraicStageKernelWordDerivativeSet

def foxAlgebraicStageKernelWordDerivativeSet :
    Set (foxAlgebraicStageCoordinateVector (X := X) N n) :=
  { v | ∃ w : FreeGroup X,
      w ∈ N ∧ foxAlgebraicStageDerivativeVector (X := X) N n w = v }

Word-level kernel derivatives in the finite stage. This is the algebraic form obtained from actual relation words w \(\in\) N.

Theorem FoxDifferential.foxAlgebraicStageCoefficient_eq_one_of_mem

omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageCoefficient_eq_one_of_mem
    {w : FreeGroup X} (hw : w ∈ N) :
    foxAlgebraicStageCoefficient (X := X) N n w = 1

A word lying in the normal subgroup \(N\) has finite-stage coefficient equal to \(1\) in the quotient by \(N\).

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageQuotientCoefficient_eq_one_of_kernel

omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageQuotientCoefficient_eq_one_of_kernel
    {q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n}
    (hq : foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1) :
    foxAlgebraicStageQuotientCoefficient (X := X) N n q = 1

For a kernel element, the finite Fox-stage quotient coefficient evaluates to one after coefficient change.

Show Lean proof

Definition FoxDifferential.foxAlgebraicStageSourceKernelDerivativeAddSubgroup

def foxAlgebraicStageSourceKernelDerivativeAddSubgroup :
    AddSubgroup (foxAlgebraicStageCoordinateVector (X := X) N n) where
  carrier := foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n
  zero_mem' := by
    refine ⟨1, ?_, ?_⟩
    · simp only [map_one]
    · exact ScalarCrossedHom.map_one
        (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)
  add_mem' := by
    intro a b ha hb
    rcases ha with ⟨q, hq, hqa⟩
    rcases hb with ⟨r, hr, hrb⟩
    refine ⟨q * r, ?_, ?_⟩
    · rw [map_mul, hq, hr, one_mul]
    · rw [ScalarCrossedHom.map_mul
          (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)]
      rw [foxAlgebraicStageQuotientCoefficient_eq_one_of_kernel (X := X) N n hq]
      simp only [hqa, hrb, one_smul]
  neg_mem' := by
    intro a ha
    rcases ha with ⟨q, hq, hqa⟩
    refine ⟨q⁻¹, ?_, ?_⟩
    · rw [map_inv, hq]
      simp only [inv_one]
    · rw [ScalarCrossedHom.map_inv
          (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)]
      have hcoeff :
          foxAlgebraicStageQuotientCoefficient (X := X) N n q⁻¹ = 1 := by
        apply foxAlgebraicStageQuotientCoefficient_eq_one_of_kernel (X := X) N n
        rw [map_inv, hq]
        simp only [inv_one]
      rw [hcoeff]
      simp only [hqa, one_smul]

Source-kernel derivatives form an additive subgroup of the finite coordinate module.

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeAddSubgroup_coe

@[simp]
theorem foxAlgebraicStageSourceKernelDerivativeAddSubgroup_coe :
    ((foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n :
        AddSubgroup (foxAlgebraicStageCoordinateVector (X := X) N n)) :
          Set (foxAlgebraicStageCoordinateVector (X := X) N n)) =
      foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n

The finite-stage source-kernel derivative additive subgroup coerces to its defining carrier.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet

theorem foxAlgebraicStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet :
    foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n =
      foxAlgebraicStageKernelWordDerivativeSet (X := X) N n

The quotient-level and word-level descriptions of finite-stage source-kernel derivatives coincide.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet_subset_boundaryCycleSubmodule

theorem foxAlgebraicStageSourceKernelDerivativeSet_subset_boundaryCycleSubmodule
    [Fintype X] :
    foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n ⊆
      (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n :
        Set (foxAlgebraicStageCoordinateVector (X := X) N n))

Every finite-stage source-kernel derivative is a finite Fox boundary cycle.

Show Lean proof

Definition FoxDifferential.foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel

def foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel [Fintype X] : Prop :=
  (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n :
      Set (foxAlgebraicStageCoordinateVector (X := X) N n)) ⊆
    foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n

The finite-stage exactness target: every finite Fox boundary cycle is represented by a source-kernel derivative in \(F/[N,N]N^n\).

Theorem FoxDifferential.foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_iff_words

theorem foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_iff_words
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔
      (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n :
          Set (foxAlgebraicStageCoordinateVector (X := X) N n)) ⊆
        foxAlgebraicStageKernelWordDerivativeSet (X := X) N n

The finite-stage exactness target is equivalent to the formulation using actual kernel words.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_iff

theorem foxAlgebraicStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n =
        (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n :
          Set (foxAlgebraicStageCoordinateVector (X := X) N n)) ↔
      foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

The finite-stage source-kernel derivative set is equal to \(\ker \partial\) exactly when the reverse coverage inclusion holds.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycles

Declarations