FoxDifferential.Completed.FiniteStage.RelationModule

10 Theorem | 3 Definition | 1 Abbreviation

This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.

Open this file on GitHub

import

FoxDifferential.Completed.FiniteStage.BoundaryCycles

Imported by

Abbreviation FoxDifferential.finiteFoxStageRelationGroup GitHub

abbrev finiteFoxStageRelationGroup : Type u :=
  (finiteFoxCommutatorPowerQuotientMapToNormalQuotient
    (F := FreeGroup X) N n).ker

The finite-stage relation group \(\ker(F/[N,N]N^n \to F/N)\). Its elements are exactly finite-stage kernel relations.

Theorem FoxDifferential.finiteFoxStageRelationGroup_target_eq_one GitHub

theorem finiteFoxStageRelationGroup_target_eq_one
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxCommutatorPowerQuotientMapToNormalQuotient
      (F := FreeGroup X) N n q.1 = 1

Every finite-stage relation group element maps to \(1\) in the target normal quotient.

Show proof

Theorem FoxDifferential.finiteFoxStageQuotientCoefficient_relation_eq_one GitHub

theorem finiteFoxStageQuotientCoefficient_relation_eq_one
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxStageQuotientCoefficient (X := X) N n q.1 = 1

Every finite-stage relation group element has quotient coefficient equal to \(1\).

Show proof

Definition FoxDifferential.finiteFoxStageRelationBoundaryAddMonoidHom GitHub

def finiteFoxStageRelationBoundaryAddMonoidHom :
    Additive (finiteFoxStageRelationGroup (X := X) N n) →+
      finiteFoxStageCoordinateVector (X := X) N n :=
  IsCrossedDifferential.restrictTrivialSubgroupAddMonoidHom
    (finiteFoxStageQuotientDerivativeVector_isCrossedDifferential (X := X) N n)
    ((finiteFoxCommutatorPowerQuotientMapToNormalQuotient
      (F := FreeGroup X) N n).ker)
    (fun q => finiteFoxStageQuotientCoefficient_relation_eq_one (X := X) N n q)

@[simp]

The finite-stage relation boundary, written additively: \(N/[N,N]N^n \to ((\mathbb{Z}/n\mathbb{Z})[F/N])^X\).

Theorem FoxDifferential.finiteFoxStageRelationBoundaryAddMonoidHom_of GitHub

theorem finiteFoxStageRelationBoundaryAddMonoidHom_of
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q) =
      finiteFoxStageQuotientDerivativeVector (X := X) N n q.1

The relation-boundary add monoid homomorphism is evaluated on a finite-stage relation by the defining boundary formula.

Show proof

Definition FoxDifferential.finiteFoxStageRelationBoundaryRange GitHub

def finiteFoxStageRelationBoundaryRange :
    AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n) :=
  finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n

@[simp]

The relation-boundary image, as an additive subgroup of the finite coordinate module.

Theorem FoxDifferential.finiteFoxStageRelationBoundaryRange_coe GitHub

theorem finiteFoxStageRelationBoundaryRange_coe :
    ((finiteFoxStageRelationBoundaryRange (X := X) N n :
        AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n)) :
          Set (finiteFoxStageCoordinateVector (X := X) N n)) =
      finiteFoxStageSourceKernelDerivativeSet (X := X) N n

The relation-boundary range has the finite-stage source-kernel derivative set as its underlying set.

Show proof

Theorem FoxDifferential.mem_finiteFoxStageRelationBoundaryRange_iff GitHub

theorem mem_finiteFoxStageRelationBoundaryRange_iff
    {v : finiteFoxStageCoordinateVector (X := X) N n} :
    v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n ↔
      ∃ q : Additive (finiteFoxStageRelationGroup (X := X) N n),
        finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n q = v

Membership in the finite-stage relation-boundary range is equivalent to the displayed coordinate condition.

Show proof

Theorem FoxDifferential.finiteFoxStageFoxBoundary_relationBoundary_eq_zero GitHub

theorem finiteFoxStageFoxBoundary_relationBoundary_eq_zero
    [Fintype X] (q : Additive (finiteFoxStageRelationGroup (X := X) N n)) :
    finiteFoxStageFoxBoundary (X := X) N n
      (finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n q) = 0

The finite-stage relation boundary lands in finite Fox boundary cycles.

Show proof

Theorem FoxDifferential.finiteFoxStageRelationBoundary_range_le_boundaryCycleSubmodule GitHub

theorem finiteFoxStageRelationBoundary_range_le_boundaryCycleSubmodule
    [Fintype X] :
    finiteFoxStageRelationBoundaryRange (X := X) N n ≤
      (finiteFoxStageBoundaryCycleSubmodule (X := X) N n).toAddSubgroup

The relation-boundary range is contained in \(\ker \partial\).

Show proof

Definition FoxDifferential.finiteFoxStageRelationBoundaryExact GitHub

def finiteFoxStageRelationBoundaryExact [Fintype X] : Prop :=
  Function.Exact
    (finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n)
    (finiteFoxStageFoxBoundary (X := X) N n)

Finite-stage exactness at the coordinate module.

Theorem FoxDifferential.finiteFoxStageRelationBoundaryExact_iff_boundaryCyclesCoveredBySourceKernel GitHub

theorem finiteFoxStageRelationBoundaryExact_iff_boundaryCyclesCoveredBySourceKernel
    [Fintype X] :
    finiteFoxStageRelationBoundaryExact (X := X) N n ↔
      finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

Finite-stage exactness is equivalent to the coverage statement formulated at the level of finite-stage boundary cycles.

Show proof

Theorem FoxDifferential.finiteFoxStageRelationBoundaryExact_of_boundaryCyclesCoveredBySourceKernel GitHub

theorem finiteFoxStageRelationBoundaryExact_of_boundaryCyclesCoveredBySourceKernel
    [Fintype X]
    (hcovered : finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n) :
    finiteFoxStageRelationBoundaryExact (X := X) N n

Coverage of finite boundary cycles gives finite-stage exactness in the usual function-level form.

Show proof

Theorem FoxDifferential.finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact GitHub

theorem finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact
    [Fintype X]
    (hexact : finiteFoxStageRelationBoundaryExact (X := X) N n) :
    finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

Function-level finite-stage exactness gives the set-level coverage used by the density step.

Show proof

FoxDifferential.Completed.FiniteStage.RelationModule

Declarations