ProCGroups.FoxDifferential.Completed.FiniteStage.RelationModule

10 Theorems | 3 Definitions | 1 Abbreviation

The principal declarations in this module are:

foxAlgebraicStageRelationGroup The finite-stage relation group \(\ker(F/[N,N]N^n \to F/N)\). Its elements are exactly finite-stage kernel relations. - foxAlgebraicStageRelationBoundaryAddMonoidHom The finite-stage relation boundary, written additively: \(N/[N,N]N^n \to ((\mathbb{Z}/n\mathbb{Z})[F/N])^X\). - foxAlgebraicStageRelationGroup_target_eq_one Every finite-stage relation group element maps to \(1\) in the target normal quotient. - foxAlgebraicStageQuotientCoefficient_relation_eq_one Every finite-stage relation group element has quotient coefficient equal to \(1\).

import

ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycles

Imported by

Abbreviation FoxDifferential.foxAlgebraicStageRelationGroup

abbrev foxAlgebraicStageRelationGroup : Type u :=
  (foxCommutatorPowerQuotientMapToNormalQuotient
    (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.foxAlgebraicStageRelationGroup_target_eq_one

omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageRelationGroup_target_eq_one
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxCommutatorPowerQuotientMapToNormalQuotient
      (F := FreeGroup X) N n q.1 = 1

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageQuotientCoefficient_relation_eq_one

omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageQuotientCoefficient_relation_eq_one
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageQuotientCoefficient (X := X) N n q.1 = 1

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

Show Lean proof

Definition FoxDifferential.foxAlgebraicStageRelationBoundaryAddMonoidHom

def foxAlgebraicStageRelationBoundaryAddMonoidHom :
    Additive (foxAlgebraicStageRelationGroup (X := X) N n) →+
      foxAlgebraicStageCoordinateVector (X := X) N n where
  toFun q := foxAlgebraicStageQuotientDerivativeVector (X := X) N n
    (Additive.toMul q).1
  map_zero' := by
    change foxAlgebraicStageQuotientDerivativeVector (X := X) N n 1 = 0
    exact ScalarCrossedHom.map_one
      (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)
  map_add' := by
    intro q r
    change foxAlgebraicStageQuotientDerivativeVector (X := X) N n
        ((Additive.toMul q).1 * (Additive.toMul r).1) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1 +
        foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul r).1
    rw [ScalarCrossedHom.map_mul
      (foxAlgebraicStageQuotientDerivativeVector (X := X) N n),
      foxAlgebraicStageQuotientCoefficient_relation_eq_one]
    simp only [one_smul]

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

Theorem FoxDifferential.foxAlgebraicStageRelationBoundaryAddMonoidHom_of

@[simp]
theorem foxAlgebraicStageRelationBoundaryAddMonoidHom_of
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q) =
      foxAlgebraicStageQuotientDerivativeVector (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 Lean proof

Definition FoxDifferential.foxAlgebraicStageRelationBoundaryRange

def foxAlgebraicStageRelationBoundaryRange :
    AddSubgroup (foxAlgebraicStageCoordinateVector (X := X) N n) :=
  foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n

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

Theorem FoxDifferential.foxAlgebraicStageRelationBoundaryRange_coe

@[simp]
theorem foxAlgebraicStageRelationBoundaryRange_coe :
    ((foxAlgebraicStageRelationBoundaryRange (X := X) N n :
        AddSubgroup (foxAlgebraicStageCoordinateVector (X := X) N n)) :
          Set (foxAlgebraicStageCoordinateVector (X := X) N n)) =
      foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n

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

Show Lean proof

Theorem FoxDifferential.mem_foxAlgebraicStageRelationBoundaryRange_iff

theorem mem_foxAlgebraicStageRelationBoundaryRange_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {v : foxAlgebraicStageCoordinateVector (X := X) N n} :
    v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N n ↔
      ∃ q : Additive (foxAlgebraicStageRelationGroup (X := X) N n),
        foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n q = v

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageFoxBoundary_relationBoundary_eq_zero

theorem foxAlgebraicStageFoxBoundary_relationBoundary_eq_zero
    [Fintype X] (q : Additive (foxAlgebraicStageRelationGroup (X := X) N n)) :
    foxAlgebraicStageFoxBoundary (X := X) N n
      (foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n q) = 0

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageRelationBoundary_range_le_boundaryCycleSubmodule

theorem foxAlgebraicStageRelationBoundary_range_le_boundaryCycleSubmodule
    [Fintype X] :
    foxAlgebraicStageRelationBoundaryRange (X := X) N n ≤
      (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n).toAddSubgroup

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

Show Lean proof

Definition FoxDifferential.foxAlgebraicStageRelationBoundaryExact

def foxAlgebraicStageRelationBoundaryExact [Fintype X] : Prop :=
  Function.Exact
    (foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n)
    (foxAlgebraicStageFoxBoundary (X := X) N n)

Finite-stage exactness at the coordinate module.

Theorem FoxDifferential.foxAlgebraicStageRelationBoundaryExact_iff_boundaryCyclesCoveredBySourceKernel

theorem foxAlgebraicStageRelationBoundaryExact_iff_boundaryCyclesCoveredBySourceKernel
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageRelationBoundaryExact (X := X) N n ↔
      foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageRelationBoundaryExact_of_boundaryCyclesCoveredBySourceKernel

theorem foxAlgebraicStageRelationBoundaryExact_of_boundaryCyclesCoveredBySourceKernel
    [Fintype X]
    (hcovered : foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n) :
    foxAlgebraicStageRelationBoundaryExact (X := X) N n

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

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact

theorem foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryExact (X := X) N n) :
    foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.FiniteStage.RelationModule

Declarations