ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdealPrimitive

15 Theorems | 5 Definitions

The principal declarations in this module are:

foxAlgebraicStageSourceBoundaryPrimitive 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. - foxAlgebraicStageSourceBoundaryPrimitiveSubmodule Source-boundary primitives form a left submodule of the source group algebra. - foxAlgebraicStageSourceBoundaryPrimitive_zero The zero source-boundary primitive. - foxAlgebraicStageSourceBoundaryPrimitive_add Source-boundary primitives are closed under addition.

import

ProCGroups.FoxDifferential.Completed.FiniteStage.SourceDerivativeVector

Imported by

Definition FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive

def foxAlgebraicStageSourceBoundaryPrimitive [Fintype X]
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) : Prop :=
  ∃ p : foxAlgebraicStageSourceCoordinateVector (X := X) N n,
    foxAlgebraicStageSourceFoxBoundary (X := X) N n p = x ∧
      foxAlgebraicStageCoordinateSourceToTarget (X := X) N n p ∈
        foxAlgebraicStageRelationBoundarySubmodule (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.foxAlgebraicStageSourceBoundaryPrimitive_zero

theorem foxAlgebraicStageSourceBoundaryPrimitive_zero [Fintype X] :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n 0

The zero source-boundary primitive.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_add

theorem foxAlgebraicStageSourceBoundaryPrimitive_add [Fintype X]
    {x y : foxAlgebraicStageSourceGroupAlgebra (X := X) N n}
    (hx : foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n x)
    (hy : foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n y) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n (x + y)

Source-boundary primitives are closed under addition.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_neg

theorem foxAlgebraicStageSourceBoundaryPrimitive_neg [Fintype X]
    {x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n}
    (hx : foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n x) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n (-x)

Source-boundary primitives are closed under negation.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_sub

theorem foxAlgebraicStageSourceBoundaryPrimitive_sub [Fintype X]
    {x y : foxAlgebraicStageSourceGroupAlgebra (X := X) N n}
    (hx : foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n x)
    (hy : foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n y) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n (x - y)

Source-boundary primitives are closed under subtraction.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_smul

theorem foxAlgebraicStageSourceBoundaryPrimitive_smul [Fintype X]
    (a : foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
    {x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n}
    (hx : foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n x) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n (a • x)

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

Show Lean proof

Definition FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitiveSubmodule

def foxAlgebraicStageSourceBoundaryPrimitiveSubmodule [Fintype X] :
    Submodule (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
      (foxAlgebraicStageSourceGroupAlgebra (X := X) N n) where
  carrier := {x | foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n x}
  zero_mem' := foxAlgebraicStageSourceBoundaryPrimitive_zero (X := X) N n
  add_mem' := by
    intro x y hx hy
    exact foxAlgebraicStageSourceBoundaryPrimitive_add (X := X) N n hx hy
  smul_mem' := by
    intro a x hx
    exact foxAlgebraicStageSourceBoundaryPrimitive_smul (X := X) N n a hx

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

Theorem FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitiveSubmodule_coe

@[simp]
theorem foxAlgebraicStageSourceBoundaryPrimitiveSubmodule_coe [Fintype X] :
    ((foxAlgebraicStageSourceBoundaryPrimitiveSubmodule (X := X) N n :
      Submodule (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
        (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)) :
        Set (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)) =
      {x | foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n x}

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

Show Lean proof

Definition FoxDifferential.foxAlgebraicStageRelationAugmentationPrimitiveVector

def foxAlgebraicStageRelationAugmentationPrimitiveVector
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageSourceCoordinateVector (X := X) N n :=
  foxAlgebraicStageSourceDerivativeVector (X := X) N n q.1

The source primitive attached to a finite relation q.

Theorem FoxDifferential.foxAlgebraicStageSourceFoxBoundary_relationAugmentationPrimitiveVector

theorem foxAlgebraicStageSourceFoxBoundary_relationAugmentationPrimitiveVector
    [Fintype X]
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageSourceFoxBoundary (X := X) N n
        (foxAlgebraicStageRelationAugmentationPrimitiveVector (X := X) N n q) =
      foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageCoordinateSourceToTarget_relationAugmentationPrimitiveVector

theorem foxAlgebraicStageCoordinateSourceToTarget_relationAugmentationPrimitiveVector
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageCoordinateSourceToTarget (X := X) N n
        (foxAlgebraicStageRelationAugmentationPrimitiveVector (X := X) N n q) =
      foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q)

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_relationAugmentationGenerator

theorem foxAlgebraicStageSourceBoundaryPrimitive_relationAugmentationGenerator
    [Fintype X]
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n
      (foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q)

Relation augmentation generators have relation-compatible source Fox primitives.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_sourceBasis_mul_relationAugmentationGenerator

theorem foxAlgebraicStageSourceBoundaryPrimitive_sourceBasis_mul_relationAugmentationGenerator
    [Fintype X]
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n
      (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) s *
        foxAlgebraicStageRelationAugmentationGenerator (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 Lean proof

Definition FoxDifferential.foxAlgebraicStageRelationAugmentationRightBasisPrimitiveVector

def foxAlgebraicStageRelationAugmentationRightBasisPrimitiveVector
    (q : foxAlgebraicStageRelationGroup (X := X) N n)
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSourceCoordinateVector (X := X) N n :=
  foxAlgebraicStageSourceDerivativeVector (X := X) N n (q.1 * s) -
    foxAlgebraicStageSourceDerivativeVector (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.foxAlgebraicStageSourceFoxBoundary_relationAugmentationRightBasisPrimitiveVector

theorem foxAlgebraicStageSourceFoxBoundary_relationAugmentationRightBasisPrimitiveVector
    [Fintype X]
    (q : foxAlgebraicStageRelationGroup (X := X) N n)
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSourceFoxBoundary (X := X) N n
        (foxAlgebraicStageRelationAugmentationRightBasisPrimitiveVector (X := X) N n q s) =
      foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q *
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) s

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageCoordinateSourceToTarget_relationAugmentationRightBasisPrimitiveVector

theorem foxAlgebraicStageCoordinateSourceToTarget_relationAugmentationRightBasisPrimitiveVector
    (q : foxAlgebraicStageRelationGroup (X := X) N n)
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageCoordinateSourceToTarget (X := X) N n
        (foxAlgebraicStageRelationAugmentationRightBasisPrimitiveVector (X := X) N n q s) =
      foxAlgebraicStageRelationBoundaryAddMonoidHom (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 Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_relationAugmentationGenerator_mul_sourceBasis

theorem foxAlgebraicStageSourceBoundaryPrimitive_relationAugmentationGenerator_mul_sourceBasis
    [Fintype X]
    (q : foxAlgebraicStageRelationGroup (X := X) N n)
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n
      (foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q *
        MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (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 Lean proof

Definition FoxDifferential.foxAlgebraicStageRelationAugmentationLeftSubmodule

def foxAlgebraicStageRelationAugmentationLeftSubmodule :
    Submodule (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
      (foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :=
  Submodule.span (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
    (Set.range (foxAlgebraicStageRelationAugmentationGenerator (X := X) N n))

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

Theorem FoxDifferential.foxAlgebraicStageRelationAugmentationLeftSubmodule_le_primitiveSubmodule

theorem foxAlgebraicStageRelationAugmentationLeftSubmodule_le_primitiveSubmodule
    [Fintype X] :
    foxAlgebraicStageRelationAugmentationLeftSubmodule (X := X) N n ≤
      foxAlgebraicStageSourceBoundaryPrimitiveSubmodule (X := X) N n

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_of_mem_relationAugmentationLeftSubmodule

theorem foxAlgebraicStageSourceBoundaryPrimitive_of_mem_relationAugmentationLeftSubmodule
    [Fintype X]
    {x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n}
    (hx : x ∈ foxAlgebraicStageRelationAugmentationLeftSubmodule (X := X) N n) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n x

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdealPrimitive

Declarations