NYLL
Module

BoundaryQuotient.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryQuotient
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — boundary quotient

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.

Imports1
Imported by2

Declarations

abbrev

foxAlgebraicStageCoordinateModuloRelations

L39 ↗
FoxDifferential.foxAlgebraicStageCoordinateModuloRelations
Documentation

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

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
abbrev foxAlgebraicStageCoordinateModuloRelations : Type u
def

foxAlgebraicStageBoundaryModuloRelations

L44 ↗
FoxDifferential.foxAlgebraicStageBoundaryModuloRelations
Documentation

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

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 foxAlgebraicStageBoundaryModuloRelations [Fintype X] :
    foxAlgebraicStageCoordinateModuloRelations (X := X) N n →ₗ[
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n]
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n
theorem

foxAlgebraicStageBoundaryModuloRelations_mk

L57 ↗
FoxDifferential.foxAlgebraicStageBoundaryModuloRelations_mk
Documentation

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

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

foxAlgebraicStageCoordinateModuloRelations_mk_eq_zero_of_cycle

L68 ↗
FoxDifferential.foxAlgebraicStageCoordinateModuloRelations_mk_eq_zero_of_cycle
Documentation

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

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

foxAlgebraicStageBoundaryModuloRelations_injective_of_relationBoundaryModuleExact

L79 ↗
FoxDifferential.foxAlgebraicStageBoundaryModuloRelations_injective_of_relationBoundaryModuleExact
Documentation

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

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 foxAlgebraicStageBoundaryModuloRelations_injective_of_relationBoundaryModuleExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n) :
    Function.Injective (foxAlgebraicStageBoundaryModuloRelations (X := X) N n)
theorem

foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryModuloRelations_injective

L99 ↗
FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryModuloRelations_injective
Documentation

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

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 foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryModuloRelations_injective
    [Fintype X]
    (hinj : Function.Injective (foxAlgebraicStageBoundaryModuloRelations (X := X) N n)) :
    foxAlgebraicStageRelationBoundaryModuleExact (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.