Module

RelationAction.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationAction

8 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — relation action

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.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationModule

Imported by3

def

foxAlgebraicStageRelationConjBySource

L41 ↗

FoxDifferential.foxAlgebraicStageRelationConjBySource

Documentation

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

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 foxAlgebraicStageRelationConjBySource
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageRelationGroup (X := X) N n

theorem

foxAlgebraicStageRelationConjBySource_val

L54 ↗

FoxDifferential.foxAlgebraicStageRelationConjBySource_val

Documentation

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

Source context 8 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 : ℕ)
omit [DecidableEq X] in

Lean source · statement

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⁻¹

theorem

foxAlgebraicStageRelationBoundary_conjBySource

L61 ↗

FoxDifferential.foxAlgebraicStageRelationBoundary_conjBySource

Documentation

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

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

def

foxAlgebraicStageTargetQuotientLiftToSource

L97 ↗

FoxDifferential.foxAlgebraicStageTargetQuotientLiftToSource

Documentation

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

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 foxAlgebraicStageTargetQuotientLiftToSource
    (h : foxAlgebraicStageTargetQuotient (X := X) N) :
    FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n

theorem

foxAlgebraicStageTargetQuotientLiftToSource_spec

L107 ↗

FoxDifferential.foxAlgebraicStageTargetQuotientLiftToSource_spec

Documentation

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

Source context 8 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 : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStageTargetQuotientLiftToSource_spec
    (h : foxAlgebraicStageTargetQuotient (X := X) N) :
    foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n
      (foxAlgebraicStageTargetQuotientLiftToSource (X := X) N n h) = h

theorem

foxAlgebraicStageQuotientCoefficient_targetLift

L118 ↗

FoxDifferential.foxAlgebraicStageQuotientCoefficient_targetLift

Documentation

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

Source context 8 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 : ℕ)
omit [DecidableEq X] in

Lean source · statement

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

theorem

foxAlgebraicStageRelationBoundary_of_basis_smul

L128 ↗

FoxDifferential.foxAlgebraicStageRelationBoundary_of_basis_smul

Documentation

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

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

theorem

foxAlgebraicStageRelationBoundaryRange_basis_smul_mem

L142 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryRange_basis_smul_mem

Documentation

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

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

Module documentation

Fox differential: completed — finite stage — relation action

Declarations