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

ProCGroups.FoxDifferential.Completed.FiniteStage.RelationAction

6 Theorems | 2 Definitions

The principal declarations in this module are:

  • foxAlgebraicStageRelationConjBySource Conjugating a finite-stage relation by an arbitrary source-quotient element gives another finite-stage relation. - foxAlgebraicStageTargetQuotientLiftToSource A chosen source-quotient lift of an element of \(F/N\). - foxAlgebraicStageRelationConjBySource_val Conjugating a finite-stage relation by a source element has the stated finite-stage value. - foxAlgebraicStageRelationBoundary_conjBySource Relation-boundary equivariance for conjugation by a source-quotient element.
import
Imported by

Declarations

Definition FoxDifferential.foxAlgebraicStageRelationConjBySource 
def foxAlgebraicStageRelationConjBySource
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageRelationGroup (X := X) N n :=
  ⟨s * q.1 * s⁻¹, by
    change foxCommutatorPowerQuotientMapToNormalQuotient
      (F := FreeGroup X) N n (s * q.1 * s⁻¹) = 1
    rw [map_mul, map_mul, map_inv, q.2]
    simp only [mul_one, mul_inv_cancel]⟩

Conjugating a finite-stage relation by an arbitrary source-quotient element gives another finite-stage relation.

Theorem FoxDifferential.foxAlgebraicStageRelationConjBySource_val 
omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageRelationConjBySource_val
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    (foxAlgebraicStageRelationConjBySource (X := X) N n s q).1 = s * q.1 * s⁻¹

Conjugating a finite-stage relation by a source element has the stated finite-stage value.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageRelationBoundary_conjBySource 
theorem foxAlgebraicStageRelationBoundary_conjBySource
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n
        (Additive.ofMul (foxAlgebraicStageRelationConjBySource (X := X) N n s q)) =
      foxAlgebraicStageQuotientCoefficient (X := X) N n s •
        foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q)

Relation-boundary equivariance for conjugation by a source-quotient element.

Show Lean proof
Definition FoxDifferential.foxAlgebraicStageTargetQuotientLiftToSource 
def foxAlgebraicStageTargetQuotientLiftToSource
    (h : foxAlgebraicStageTargetQuotient (X := X) N) :
    FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n :=
  Classical.choose
    (foxCommutatorPowerQuotientMapToNormalQuotient_surjective
      (F := FreeGroup X) N n h)

A chosen source-quotient lift of an element of \(F/N\).

Theorem FoxDifferential.foxAlgebraicStageTargetQuotientLiftToSource_spec 
omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageTargetQuotientLiftToSource_spec
    (h : foxAlgebraicStageTargetQuotient (X := X) N) :
    foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n
      (foxAlgebraicStageTargetQuotientLiftToSource (X := X) N n h) = h

The chosen lift to the source quotient satisfies its finite-stage target specification.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageQuotientCoefficient_targetLift 
omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageQuotientCoefficient_targetLift
    (h : foxAlgebraicStageTargetQuotient (X := X) N) :
    foxAlgebraicStageQuotientCoefficient (X := X) N n
        (foxAlgebraicStageTargetQuotientLiftToSource (X := X) N n h) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) h

The coefficient of a chosen source lift is the corresponding group-ring basis element.

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageRelationBoundary_of_basis_smul 
theorem foxAlgebraicStageRelationBoundary_of_basis_smul
    (h : foxAlgebraicStageTargetQuotient (X := X) N)
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n
        (Additive.ofMul
          (foxAlgebraicStageRelationConjBySource (X := X) N n
            (foxAlgebraicStageTargetQuotientLiftToSource (X := X) N n h) q)) =
      (MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) h) •
        foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q)

The relation boundary is equivariant on basis elements over \(\mathbb{Z}/n\mathbb{Z}[F/N]\).

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStageRelationBoundaryRange_basis_smul_mem 
theorem foxAlgebraicStageRelationBoundaryRange_basis_smul_mem
    (h : foxAlgebraicStageTargetQuotient (X := X) N)
    {v : foxAlgebraicStageCoordinateVector (X := X) N n}
    (hv : v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N n) :
    (MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) h) • v ∈
      foxAlgebraicStageRelationBoundaryRange (X := X) N n

The relation-boundary image is stable under multiplication by target group basis elements.

Show Lean proof