Module

RelationIdealPrimitive.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdealPrimitive

20 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — relation ideal primitive

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.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.SourceDerivativeVector

Imported by2

def

foxAlgebraicStageSourceBoundaryPrimitive

L43 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive

Documentation

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 foxAlgebraicStageSourceBoundaryPrimitive [Fintype X]
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) : Prop

theorem

foxAlgebraicStageSourceBoundaryPrimitive_zero

L51 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_zero

Documentation

The zero source-boundary primitive.

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 foxAlgebraicStageSourceBoundaryPrimitive_zero [Fintype X] :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n 0

theorem

foxAlgebraicStageSourceBoundaryPrimitive_add

L59 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_add

Documentation

Source-boundary primitives are closed under addition.

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

theorem

foxAlgebraicStageSourceBoundaryPrimitive_neg

L72 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_neg

Documentation

Source-boundary primitives are closed under negation.

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 foxAlgebraicStageSourceBoundaryPrimitive_neg [Fintype X]
    {x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n}
    (hx : foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n x) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n (-x)

theorem

foxAlgebraicStageSourceBoundaryPrimitive_sub

L83 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_sub

Documentation

Source-boundary primitives are closed under subtraction.

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

theorem

foxAlgebraicStageSourceBoundaryPrimitive_smul

L93 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_smul

Documentation

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

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

def

foxAlgebraicStageSourceBoundaryPrimitiveSubmodule

L106 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitiveSubmodule

Documentation

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

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

theorem

foxAlgebraicStageSourceBoundaryPrimitiveSubmodule_coe

L123 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitiveSubmodule_coe

Documentation

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

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

def

foxAlgebraicStageRelationAugmentationPrimitiveVector

L132 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationPrimitiveVector

Documentation

The source primitive attached to a finite relation q.

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 foxAlgebraicStageRelationAugmentationPrimitiveVector
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageSourceCoordinateVector (X := X) N n

theorem

foxAlgebraicStageSourceFoxBoundary_relationAugmentationPrimitiveVector

L138 ↗

FoxDifferential.foxAlgebraicStageSourceFoxBoundary_relationAugmentationPrimitiveVector

Documentation

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

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

theorem

foxAlgebraicStageCoordinateSourceToTarget_relationAugmentationPrimitiveVector

L149 ↗

FoxDifferential.foxAlgebraicStageCoordinateSourceToTarget_relationAugmentationPrimitiveVector

Documentation

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

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

theorem

foxAlgebraicStageSourceBoundaryPrimitive_relationAugmentationGenerator

L159 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_relationAugmentationGenerator

Documentation

Relation augmentation generators have relation-compatible source Fox primitives.

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 foxAlgebraicStageSourceBoundaryPrimitive_relationAugmentationGenerator
    [Fintype X]
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageSourceBoundaryPrimitive (X := X) N n
      (foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q)

theorem

foxAlgebraicStageSourceBoundaryPrimitive_sourceBasis_mul_relationAugmentationGenerator

L179 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_sourceBasis_mul_relationAugmentationGenerator

Documentation

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

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

def

foxAlgebraicStageRelationAugmentationRightBasisPrimitiveVector

L197 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationRightBasisPrimitiveVector

Documentation

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

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

theorem

foxAlgebraicStageSourceFoxBoundary_relationAugmentationRightBasisPrimitiveVector

L205 ↗

FoxDifferential.foxAlgebraicStageSourceFoxBoundary_relationAugmentationRightBasisPrimitiveVector

Documentation

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

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

theorem

foxAlgebraicStageCoordinateSourceToTarget_relationAugmentationRightBasisPrimitiveVector

L225 ↗

FoxDifferential.foxAlgebraicStageCoordinateSourceToTarget_relationAugmentationRightBasisPrimitiveVector

Documentation

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

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

theorem

foxAlgebraicStageSourceBoundaryPrimitive_relationAugmentationGenerator_mul_sourceBasis

L244 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_relationAugmentationGenerator_mul_sourceBasis

Documentation

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

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

def

foxAlgebraicStageRelationAugmentationLeftSubmodule

L263 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationLeftSubmodule

Documentation

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

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 foxAlgebraicStageRelationAugmentationLeftSubmodule :
    Submodule (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
      (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)

theorem

foxAlgebraicStageRelationAugmentationLeftSubmodule_le_primitiveSubmodule

L270 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationLeftSubmodule_le_primitiveSubmodule

Documentation

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

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 foxAlgebraicStageRelationAugmentationLeftSubmodule_le_primitiveSubmodule
    [Fintype X] :
    foxAlgebraicStageRelationAugmentationLeftSubmodule (X := X) N n ≤
      foxAlgebraicStageSourceBoundaryPrimitiveSubmodule (X := X) N n

theorem

foxAlgebraicStageSourceBoundaryPrimitive_of_mem_relationAugmentationLeftSubmodule

L283 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryPrimitive_of_mem_relationAugmentationLeftSubmodule

Documentation

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

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

Module documentation

Fox differential: completed — finite stage — relation ideal primitive

Declarations