Module

Fundamental.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Derivative.Quotient.Fundamental

4 declarations indexed from sourceView source ↗

Module documentation

Fox differential: stage — derivative — quotient — fundamental

The principal declarations in this module are:

foxAlgebraicStageQuotientDerivative_fundamental_formula

Finite-stage Fox fundamental formula on the finite source quotient.

foxAlgebraicStageFoxBoundary_quotientDerivativeVector

Boundary-map form of the finite-stage Fox fundamental formula on the finite source quotient.

foxAlgebraicStageFoxBoundary_quotient_of_crossedHom

Any quotient-level scalar crossed homomorphism with standard generator values satisfies the Fox boundary formula.

foxAlgebraicStageQuotientDerivative_fundamental_formula_of_crossedHom

The quotient Fox fundamental formula for a scalar crossed homomorphism with standard generator values.

Imports2

Imported by3

theorem

foxAlgebraicStageQuotientDerivative_fundamental_formula

L40 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivative_fundamental_formula

Documentation

Finite-stage Fox fundamental formula on the finite source quotient.

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 foxAlgebraicStageQuotientDerivative_fundamental_formula
    [Fintype X]
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageQuotientCoefficient (X := X) N n q - 1 =
      ∑ i : X,
        foxAlgebraicStageQuotientDerivative (X := X) N n i q *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1)

theorem

foxAlgebraicStageFoxBoundary_quotientDerivativeVector

L56 ↗

FoxDifferential.foxAlgebraicStageFoxBoundary_quotientDerivativeVector

Documentation

Boundary-map form of the finite-stage Fox fundamental formula on the finite source quotient.

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 foxAlgebraicStageFoxBoundary_quotientDerivativeVector
    [Fintype X]
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageFoxBoundary (X := X) N n
        (foxAlgebraicStageQuotientDerivativeVector (X := X) N n q) =
      foxAlgebraicStageQuotientCoefficient (X := X) N n q - 1

theorem

foxAlgebraicStageFoxBoundary_quotient_of_crossedHom

L70 ↗

FoxDifferential.foxAlgebraicStageFoxBoundary_quotient_of_crossedHom

Documentation

Any quotient-level scalar crossed homomorphism with standard generator values satisfies the Fox boundary formula.

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 foxAlgebraicStageFoxBoundary_quotient_of_crossedHom
    [Fintype X]
    (delta : ScalarCrossedHom
      (foxAlgebraicStageQuotientCoefficient (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n))
    (hbasis :
      ∀ x : X,
        delta
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
            (FreeGroup.of x)) =
          Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n))
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageFoxBoundary (X := X) N n (delta q) =
      foxAlgebraicStageQuotientCoefficient (X := X) N n q - 1

theorem

foxAlgebraicStageQuotientDerivative_fundamental_formula_of_crossedHom

L95 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivative_fundamental_formula_of_crossedHom

Documentation

The quotient Fox fundamental formula for a scalar crossed homomorphism with standard generator values.

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 foxAlgebraicStageQuotientDerivative_fundamental_formula_of_crossedHom
    [Fintype X]
    (delta : ScalarCrossedHom
      (foxAlgebraicStageQuotientCoefficient (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n))
    (hbasis :
      ∀ x : X,
        delta
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
            (FreeGroup.of x)) =
          Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n))
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageQuotientCoefficient (X := X) N n q - 1 =
      ∑ i : X,
        delta q i *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1)

Module documentation

Fox differential: stage — derivative — quotient — fundamental

Declarations

foxAlgebraicStageQuotientDerivative_fundamental_formula

foxAlgebraicStageFoxBoundary_quotientDerivativeVector

foxAlgebraicStageFoxBoundary_quotient_of_crossedHom

foxAlgebraicStageQuotientDerivative_fundamental_formula_of_crossedHom