ProCGroups.FoxDifferential.Completed.FiniteStage.RelationRealization

5 Theorems

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.

imports

Imported by

ProCGroups.FoxDifferential.Completed.FiniteStage

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet_zsmul_mem

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

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSourceKernelDerivativeSet_basis_smul_mem

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

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.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageKernelWordDerivativeSet_basis_smul_mem

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

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageRelationBoundaryExact_of_relationBoundaryModuleExact

theorem foxAlgebraicStageRelationBoundaryExact_of_relationBoundaryModuleExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n) :
    foxAlgebraicStageRelationBoundaryExact (X := X) N n

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSemiBoundaryCyclesCovered_of_relBoundaryModuleExact

theorem foxAlgebraicStageSemiBoundaryCyclesCovered_of_relBoundaryModuleExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n) :
    foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n

Module-level finite exactness gives finite semidirect coverage of boundary cycles (v,1).

Show Lean proof

ProCGroups.FoxDifferential.Completed.FiniteStage.RelationRealization

Declarations