NYLL
Module

SpecialValues.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.SpecialValues
7 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — derivative — source — special values

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_one

The completed-target Fox derivative sends the unit of the completed source group algebra to zero.

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_sub_one

Subtracting the unit from a group-like source element does not change its completed-target Fox derivative.

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget_sub_one

Subtracting the unit from a group-like source element does not change its completed-target Fox derivative vector.

  • foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_toFamily

Family-level projection formula for the derivative limit of a group-like source element.

Imports1
Imported by4

Declarations

theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_one

L50 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_one
Documentation

The completed-target Fox derivative sends the unit of the completed source group algebra to zero.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_one
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (i : X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite i
        (1 : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X)) = 0
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_sub_one

L96 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_sub_one
Documentation

Subtracting the unit from a group-like source element does not change its completed-target Fox derivative.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_sub_one
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (i : X) (w : FreeGroup X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite i
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w - 1) =
      primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite i
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w)
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget_sub_one

L120 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget_sub_one
Documentation

Subtracting the unit from a group-like source element does not change its completed-target Fox derivative vector.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget_sub_one
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (w : FreeGroup X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w - 1) =
      primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w)
theorem

foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_toFamily

L144 ↗
FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_toFamily
Documentation

Family-level projection formula for the derivative limit of a group-like source element.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_toFamily
    (N : Subgroup (FreeGroup X)) [N.Normal] (i : X) (w : FreeGroup X) (a : ℕ) :
    foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N
        (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i
          (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N w)) a =
      foxAlgebraicStageDerivative (X := X) N (ℓ ^ a) i w
theorem

foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_mul

L154 ↗
FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_mul
Documentation

Product rule for the prime-power derivative limit on group-like source elements.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_mul
    (N : Subgroup (FreeGroup X)) [N.Normal] (i : X) (u v : FreeGroup X) :
    foxAlgebraicStagePrimePowerDerivativeLimitAddHom (ℓ := ℓ) (X := X) N i
        (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N (u * v)) =
      foxAlgebraicStagePrimePowerDerivativeLimitAddHom (ℓ := ℓ) (X := X) N i
          (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N u) +
        foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N u *
          foxAlgebraicStagePrimePowerDerivativeLimitAddHom (ℓ := ℓ) (X := X) N i
            (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N v)
theorem

foxAlgebraicStagePrimePowerDerivativeLimit_generator_projection

L175 ↗
FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimit_generator_projection
Documentation

The generator-value projection formula for the prime-power derivative limit.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem foxAlgebraicStagePrimePowerDerivativeLimit_generator_projection
    (N : Subgroup (FreeGroup X)) [N.Normal] (i j : X) (a : ℕ) :
    (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
        (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i
          (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N (FreeGroup.of j))) =
      ((Pi.single j (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ a))) :
        X → foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ a)) i
theorem

ppCompletedGAFoxDerivToTarget_generator_proj

L191 ↗
FoxDifferential.ppCompletedGAFoxDerivToTarget_generator_proj
Documentation

The generator-value projection formula for the completed-target Fox derivative.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem ppCompletedGAFoxDerivToTarget_generator_proj
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (i j : X)
    (k : PrimePowerCompletedGroupAlgebraIndex
      (foxAlgebraicStageTargetQuotient (X := X) N)) :
    primePowerCompletedGroupAlgebraProjection
        (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) k
        (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
          (ℓ := ℓ) (X := X) N hfinite i
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X)
            (FreeGroup.of j))) =
      modNCompletedGroupAlgebraStageMap (ℓ ^ k.1)
        (foxAlgebraicStageTargetQuotient (X := X) N) k.2
        (((Pi.single j
          (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ k.1))) :
            X → foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ k.1)) i)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.