NYLL
Module

RelationRealization.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationRealization
5 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — relation realization

The principal declarations in this module are:

  • foxAlgebraicStageSourceKernelDerivativeSet_zsmul_mem

The additive source-kernel derivative set is closed under integer multiples.

  • foxAlgebraicStageSourceKernelDerivativeSet_basis_smul_mem

The source-kernel derivative set is stable under multiplication by target-group basis coefficients. This is the finite algebraic form of conjugating a relation by a chosen lift of a target quotient element.

  • foxAlgebraicStageKernelWordDerivativeSet_basis_smul_mem

Word-level finite relation derivatives are stable under multiplication by target-group basis coefficients, after rewriting the source-kernel and word-level descriptions.

  • foxAlgebraicStageRelationBoundaryExact_of_relationBoundaryModuleExact

Module-level finite exactness gives function-level finite exactness for the relation boundary followed by the Fox boundary.

Imports2
Imported by2

Declarations

theorem

foxAlgebraicStageSourceKernelDerivativeSet_zsmul_mem

L42 ↗
FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet_zsmul_mem
Documentation

The additive source-kernel derivative set is closed under integer multiples.

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_zsmul_mem
    (m : ℤ) {v : foxAlgebraicStageCoordinateVector (X := X) N n}
    (hv : v ∈ foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n) :
    m • v ∈ foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n
theorem

foxAlgebraicStageSourceKernelDerivativeSet_basis_smul_mem

L54 ↗
FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet_basis_smul_mem
Documentation

The source-kernel derivative set is stable under multiplication by target-group basis coefficients. This is the finite algebraic form of conjugating a relation by a chosen lift of a target quotient element.

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_basis_smul_mem
    (h : foxAlgebraicStageTargetQuotient (X := X) N)
    {v : foxAlgebraicStageCoordinateVector (X := X) N n}
    (hv : v ∈ foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n) :
    (MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) h) • v ∈
      foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n
theorem

foxAlgebraicStageKernelWordDerivativeSet_basis_smul_mem

L68 ↗
FoxDifferential.foxAlgebraicStageKernelWordDerivativeSet_basis_smul_mem
Documentation

Word-level finite relation derivatives are stable under multiplication by target-group basis coefficients, after rewriting the source-kernel and word-level descriptions.

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 foxAlgebraicStageKernelWordDerivativeSet_basis_smul_mem
    (h : foxAlgebraicStageTargetQuotient (X := X) N)
    {v : foxAlgebraicStageCoordinateVector (X := X) N n}
    (hv : v ∈ foxAlgebraicStageKernelWordDerivativeSet (X := X) N n) :
    (MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) h) • v ∈
      foxAlgebraicStageKernelWordDerivativeSet (X := X) N n
theorem

foxAlgebraicStageRelationBoundaryExact_of_relationBoundaryModuleExact

L83 ↗
FoxDifferential.foxAlgebraicStageRelationBoundaryExact_of_relationBoundaryModuleExact
Documentation

Module-level finite exactness gives function-level finite exactness for the relation boundary followed by the Fox boundary.

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 foxAlgebraicStageRelationBoundaryExact_of_relationBoundaryModuleExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n) :
    foxAlgebraicStageRelationBoundaryExact (X := X) N n
theorem

foxAlgebraicStageSemiBoundaryCyclesCovered_of_relBoundaryModuleExact

L93 ↗
FoxDifferential.foxAlgebraicStageSemiBoundaryCyclesCovered_of_relBoundaryModuleExact
Documentation

Module-level finite exactness gives finite semidirect coverage of boundary cycles (v,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 foxAlgebraicStageSemiBoundaryCyclesCovered_of_relBoundaryModuleExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n) :
    foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.