FoxDifferential.Completed.FiniteStage.RelationIdealPrimitive

15 Theorem | 5 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.SourceDerivativeVector

Imported by

FoxDifferential.Completed.FiniteStage.SourceCycleReduction

Definition FoxDifferential.finiteFoxStageSourceBoundaryPrimitive GitHub

def finiteFoxStageSourceBoundaryPrimitive [Fintype X]
    (x : finiteFoxStageSourceGroupAlgebra (X := X) N n) : Prop :=
  ∃ p : finiteFoxStageSourceCoordinateVector (X := X) N n,
    finiteFoxStageSourceFoxBoundary (X := X) N n p = x ∧
      finiteFoxStageCoordinateSourceToTarget (X := X) N n p ∈
        finiteFoxStageRelationBoundarySubmodule (X := X) N n

An element of the source finite group algebra has a relation-compatible source Fox primitive if it is the source boundary of a vector whose target projection lies in the finite relation-boundary submodule.

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitive_zero GitHub

theorem finiteFoxStageSourceBoundaryPrimitive_zero [Fintype X] :
    finiteFoxStageSourceBoundaryPrimitive (X := X) N n 0

The zero source-boundary primitive.

Show proof

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitive_add GitHub

theorem finiteFoxStageSourceBoundaryPrimitive_add [Fintype X]
    {x y : finiteFoxStageSourceGroupAlgebra (X := X) N n}
    (hx : finiteFoxStageSourceBoundaryPrimitive (X := X) N n x)
    (hy : finiteFoxStageSourceBoundaryPrimitive (X := X) N n y) :
    finiteFoxStageSourceBoundaryPrimitive (X := X) N n (x + y)

Source-boundary primitives are closed under addition.

Show proof

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitive_neg GitHub

theorem finiteFoxStageSourceBoundaryPrimitive_neg [Fintype X]
    {x : finiteFoxStageSourceGroupAlgebra (X := X) N n}
    (hx : finiteFoxStageSourceBoundaryPrimitive (X := X) N n x) :
    finiteFoxStageSourceBoundaryPrimitive (X := X) N n (-x)

Source-boundary primitives are closed under negation.

Show proof

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitive_sub GitHub

theorem finiteFoxStageSourceBoundaryPrimitive_sub [Fintype X]
    {x y : finiteFoxStageSourceGroupAlgebra (X := X) N n}
    (hx : finiteFoxStageSourceBoundaryPrimitive (X := X) N n x)
    (hy : finiteFoxStageSourceBoundaryPrimitive (X := X) N n y) :
    finiteFoxStageSourceBoundaryPrimitive (X := X) N n (x - y)

Source-boundary primitives are closed under subtraction.

Show proof

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitive_smul GitHub

theorem finiteFoxStageSourceBoundaryPrimitive_smul [Fintype X]
    (a : finiteFoxStageSourceGroupAlgebra (X := X) N n)
    {x : finiteFoxStageSourceGroupAlgebra (X := X) N n}
    (hx : finiteFoxStageSourceBoundaryPrimitive (X := X) N n x) :
    finiteFoxStageSourceBoundaryPrimitive (X := X) N n (a • x)

Source-boundary primitives are closed under left multiplication by source coefficients.

Show proof

Definition FoxDifferential.finiteFoxStageSourceBoundaryPrimitiveSubmodule GitHub

def finiteFoxStageSourceBoundaryPrimitiveSubmodule [Fintype X] :
    Submodule (finiteFoxStageSourceGroupAlgebra (X := X) N n)
      (finiteFoxStageSourceGroupAlgebra (X := X) N n) where
  carrier := {x | finiteFoxStageSourceBoundaryPrimitive (X := X) N n x}
  zero_mem' := finiteFoxStageSourceBoundaryPrimitive_zero (X := X) N n
  add_mem' := by
    intro x y hx hy
    exact finiteFoxStageSourceBoundaryPrimitive_add (X := X) N n hx hy
  smul_mem' := by
    intro a x hx
    exact finiteFoxStageSourceBoundaryPrimitive_smul (X := X) N n a hx

@[simp]

Source-boundary primitives form a left submodule of the source group algebra.

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitiveSubmodule_coe GitHub

theorem finiteFoxStageSourceBoundaryPrimitiveSubmodule_coe [Fintype X] :
    ((finiteFoxStageSourceBoundaryPrimitiveSubmodule (X := X) N n :
      Submodule (finiteFoxStageSourceGroupAlgebra (X := X) N n)
        (finiteFoxStageSourceGroupAlgebra (X := X) N n)) :
        Set (finiteFoxStageSourceGroupAlgebra (X := X) N n)) =
      {x | finiteFoxStageSourceBoundaryPrimitive (X := X) N n x}

The source-boundary primitive submodule has exactly the finite-stage source-boundary primitive elements as its underlying set.

Show proof

Definition FoxDifferential.finiteFoxStageRelationAugmentationPrimitiveVector GitHub

def finiteFoxStageRelationAugmentationPrimitiveVector
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxStageSourceCoordinateVector (X := X) N n :=
  finiteFoxStageSourceDerivativeVector (X := X) N n q.1

The source primitive attached to a finite relation q.

Theorem FoxDifferential.finiteFoxStageSourceFoxBoundary_relationAugmentationPrimitiveVector GitHub

theorem finiteFoxStageSourceFoxBoundary_relationAugmentationPrimitiveVector
    [Fintype X]
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxStageSourceFoxBoundary (X := X) N n
        (finiteFoxStageRelationAugmentationPrimitiveVector (X := X) N n q) =
      finiteFoxStageRelationAugmentationGenerator (X := X) N n q

The source boundary of the primitive vector for q is the augmentation generator \(q-1\).

Show proof

Theorem FoxDifferential.finiteFoxStageCoordinateSourceToTarget_relationAugmentationPrimitiveVector GitHub

theorem finiteFoxStageCoordinateSourceToTarget_relationAugmentationPrimitiveVector
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxStageCoordinateSourceToTarget (X := X) N n
        (finiteFoxStageRelationAugmentationPrimitiveVector (X := X) N n q) =
      finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q)

The target projection of the primitive vector for q is the finite relation boundary of q.

Show proof

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitive_relationAugmentationGenerator GitHub

theorem finiteFoxStageSourceBoundaryPrimitive_relationAugmentationGenerator
    [Fintype X]
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxStageSourceBoundaryPrimitive (X := X) N n
      (finiteFoxStageRelationAugmentationGenerator (X := X) N n q)

Relation augmentation generators have relation-compatible source Fox primitives.

Show proof

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitive_sourceBasis_mul_relationAugmentationGenerator GitHub

theorem finiteFoxStageSourceBoundaryPrimitive_sourceBasis_mul_relationAugmentationGenerator
    [Fintype X]
    (s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxStageSourceBoundaryPrimitive (X := X) N n
      (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s *
        finiteFoxStageRelationAugmentationGenerator (X := X) N n q)

Left multiplication of a relation augmentation generator by a source quotient basis element has an explicit relation-compatible source primitive.

Show proof

Definition FoxDifferential.finiteFoxStageRelationAugmentationRightBasisPrimitiveVector GitHub

def finiteFoxStageRelationAugmentationRightBasisPrimitiveVector
    (q : finiteFoxStageRelationGroup (X := X) N n)
    (s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    finiteFoxStageSourceCoordinateVector (X := X) N n :=
  finiteFoxStageSourceDerivativeVector (X := X) N n (q.1 * s) -
    finiteFoxStageSourceDerivativeVector (X := X) N n s

Source primitive for the right basis multiple \((q - 1)s\); the primitive is \(D_{\mathrm{src}}(q s) - D_{\mathrm{src}}(s)\).

Theorem FoxDifferential.finiteFoxStageSourceFoxBoundary_relationAugmentationRightBasisPrimitiveVector GitHub

theorem finiteFoxStageSourceFoxBoundary_relationAugmentationRightBasisPrimitiveVector
    [Fintype X]
    (q : finiteFoxStageRelationGroup (X := X) N n)
    (s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    finiteFoxStageSourceFoxBoundary (X := X) N n
        (finiteFoxStageRelationAugmentationRightBasisPrimitiveVector (X := X) N n q s) =
      finiteFoxStageRelationAugmentationGenerator (X := X) N n q *
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s

The source boundary of \(D_{\mathrm{src}}(q s) - D_{\mathrm{src}}(s)\) is \((q - 1)s\).

Show proof

Theorem FoxDifferential.finiteFoxStageCoordinateSourceToTarget_relationAugmentationRightBasisPrimitiveVector GitHub

theorem finiteFoxStageCoordinateSourceToTarget_relationAugmentationRightBasisPrimitiveVector
    (q : finiteFoxStageRelationGroup (X := X) N n)
    (s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    finiteFoxStageCoordinateSourceToTarget (X := X) N n
        (finiteFoxStageRelationAugmentationRightBasisPrimitiveVector (X := X) N n q s) =
      finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q)

The target projection of \(D_{\mathrm{src}}(q s) - D_{\mathrm{src}}(s)\) is the relation boundary of \(q\).

Show proof

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitive_relationAugmentationGenerator_mul_sourceBasis GitHub

theorem finiteFoxStageSourceBoundaryPrimitive_relationAugmentationGenerator_mul_sourceBasis
    [Fintype X]
    (q : finiteFoxStageRelationGroup (X := X) N n)
    (s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    finiteFoxStageSourceBoundaryPrimitive (X := X) N n
      (finiteFoxStageRelationAugmentationGenerator (X := X) N n q *
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s)

Right multiplication of a relation augmentation generator by a source quotient basis element has an explicit relation-compatible source primitive.

Show proof

Definition FoxDifferential.finiteFoxStageRelationAugmentationLeftSubmodule GitHub

def finiteFoxStageRelationAugmentationLeftSubmodule [Fintype X] :
    Submodule (finiteFoxStageSourceGroupAlgebra (X := X) N n)
      (finiteFoxStageSourceGroupAlgebra (X := X) N n) :=
  Submodule.span (finiteFoxStageSourceGroupAlgebra (X := X) N n)
    (Set.range (finiteFoxStageRelationAugmentationGenerator (X := X) N n))

The left source-submodule generated by the relation augmentation generators.

Theorem FoxDifferential.finiteFoxStageRelationAugmentationLeftSubmodule_le_primitiveSubmodule GitHub

theorem finiteFoxStageRelationAugmentationLeftSubmodule_le_primitiveSubmodule
    [Fintype X] :
    finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n ≤
      finiteFoxStageSourceBoundaryPrimitiveSubmodule (X := X) N n

The left relation-augmentation submodule is contained in the primitive submodule.

Show proof

Theorem FoxDifferential.finiteFoxStageSourceBoundaryPrimitive_of_mem_relationAugmentationLeftSubmodule GitHub

theorem finiteFoxStageSourceBoundaryPrimitive_of_mem_relationAugmentationLeftSubmodule
    [Fintype X]
    {x : finiteFoxStageSourceGroupAlgebra (X := X) N n}
    (hx : x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n) :
    finiteFoxStageSourceBoundaryPrimitive (X := X) N n x

Membership in the left relation-augmentation submodule gives a relation-compatible source primitive.

Show proof

FoxDifferential.Completed.FiniteStage.RelationIdealPrimitive

Declarations