Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryQuotient
ProCGroups/FoxDifferential/Completed/FiniteStage/BoundaryQuotient

ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryQuotient

4 Theorems | 1 Definition | 1 Abbreviation

The principal declarations in this module are:

  • foxAlgebraicStageCoordinateModuloRelations Finite coordinate vectors modulo the submodule generated by finite relation boundaries. - foxAlgebraicStageBoundaryModuloRelations The finite Fox boundary descends to the quotient by relation boundaries. - foxAlgebraicStageBoundaryModuloRelations_mk The finite Fox boundary on the quotient by relation boundaries is evaluated by applying the ordinary finite-stage boundary to a representative. - foxAlgebraicStageCoordinateModuloRelations_mk_eq_zero_of_cycle A boundary cycle represents zero in the relation quotient when module-level finite exactness holds.
import
Imported by

Declarations

Abbreviation FoxDifferential.foxAlgebraicStageCoordinateModuloRelations 
abbrev foxAlgebraicStageCoordinateModuloRelations : Type u :=
  foxAlgebraicStageCoordinateVector (X := X) N n ⧸
    foxAlgebraicStageRelationBoundarySubmodule (X := X) N n

Finite coordinate vectors modulo the submodule generated by finite relation boundaries.

Definition FoxDifferential.foxAlgebraicStageBoundaryModuloRelations 
def foxAlgebraicStageBoundaryModuloRelations [Fintype X] :
    foxAlgebraicStageCoordinateModuloRelations (X := X) N n →ₗ[
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n]
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n :=
  Submodule.liftQ (foxAlgebraicStageRelationBoundarySubmodule (X := X) N n)
    (foxAlgebraicStageFoxBoundary (X := X) N n)
    (foxAlgebraicStageRelationBoundarySubmodule_le_boundaryCycleSubmodule (X := X) N n)

The finite Fox boundary descends to the quotient by relation boundaries.

Theorem FoxDifferential.foxAlgebraicStageBoundaryModuloRelations_mk 
@[simp]
theorem foxAlgebraicStageBoundaryModuloRelations_mk
    [Fintype X] (v : foxAlgebraicStageCoordinateVector (X := X) N n) :
    foxAlgebraicStageBoundaryModuloRelations (X := X) N n
        (Submodule.Quotient.mk v : foxAlgebraicStageCoordinateModuloRelations (X := X) N n) =
      foxAlgebraicStageFoxBoundary (X := X) N n v

The finite Fox boundary on the quotient by relation boundaries is evaluated by applying the ordinary finite-stage boundary to a representative.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageCoordinateModuloRelations_mk_eq_zero_of_cycle 
theorem foxAlgebraicStageCoordinateModuloRelations_mk_eq_zero_of_cycle
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n)
    {v : foxAlgebraicStageCoordinateVector (X := X) N n}
    (hv : v ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n) :
    (Submodule.Quotient.mk v : foxAlgebraicStageCoordinateModuloRelations (X := X) N n) = 0

A boundary cycle represents zero in the relation quotient when module-level finite exactness holds.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageBoundaryModuloRelations_injective_of_relationBoundaryModuleExact 
theorem foxAlgebraicStageBoundaryModuloRelations_injective_of_relationBoundaryModuleExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n) :
    Function.Injective (foxAlgebraicStageBoundaryModuloRelations (X := X) N n)

If module-level finite exactness holds, the descended finite boundary has trivial kernel.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryModuloRelations_injective 
theorem foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryModuloRelations_injective
    [Fintype X]
    (hinj : Function.Injective (foxAlgebraicStageBoundaryModuloRelations (X := X) N n)) :
    foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n

Injectivity of the descended finite boundary implies module-level finite exactness.

Show Lean proof