NYLL
Module

GroupLike.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.GroupLike
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — derivative — source — group like

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraFreeFoxDerivative_of

The completed source Fox derivative on a group-like element agrees with the prime-power finite-stage derivative limit of the same word.

  • foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_projection

Projecting the derivative limit of a group-like finite-stage source element gives the corresponding derivative coordinate.

  • foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_fundamental_formula

Fundamental formula for a group-like finite-stage source element at one prime-power stage.

  • primePowerCompletedGroupAlgebraFreeFoxDerivative_of_projection

Projecting the completed source Fox derivative evaluated on a group-like element gives the corresponding finite-stage derivative value.

Imports5
Imported by5

Declarations

theorem

primePowerCompletedGroupAlgebraFreeFoxDerivative_of

L54 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivative_of
Documentation

The completed source Fox derivative on a group-like element agrees with the prime-power finite-stage derivative limit of the same word.

Source context 10 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 (ℓ : ℕ)
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 : ℕ)
Lean source · statement
theorem primePowerCompletedGroupAlgebraFreeFoxDerivative_of
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (i : X) (w : FreeGroup X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivative
        (ℓ := ℓ) (X := X) N hfinite i
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) =
      foxAlgebraicStagePrimePowerDerivativeLimit
        (ℓ := ℓ) (X := X) N i
        (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N w)
theorem

foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_projection

L78 ↗
FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_projection
Documentation

Projecting the derivative limit of a group-like finite-stage source element gives the corresponding derivative coordinate.

Source context 10 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 (ℓ : ℕ)
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 : ℕ)
Lean source · statement
theorem foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_projection
    (N : Subgroup (FreeGroup X)) [N.Normal] (i : X) (w : FreeGroup X) (a : ℕ) :
    (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
        (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i
          (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N w)) =
      foxAlgebraicStageDerivative (X := X) N (ℓ ^ a) i w
theorem

foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_fundamental_formula

L89 ↗
FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_fundamental_formula
Documentation

Fundamental formula for a group-like finite-stage source element at one prime-power stage.

Source context 10 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 (ℓ : ℕ)
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 : ℕ)
Lean source · full declaration
theorem foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_fundamental_formula
    [Fintype X]
    (N : Subgroup (FreeGroup X)) [N.Normal] (w : FreeGroup X) (a : ℕ) :
    MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
        (foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w) - 1 =
      ∑ i : X,
        (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from
          (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
            (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i
              (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N w))) *
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1) := by
  rw [foxAlgebraicStageDerivative_fundamental_formula (X := X) (N := N) (n := ℓ ^ a) w]
  apply Finset.sum_congr rfl
  intro i hi
  rw [foxAlgebraicStagePrimePowerDerivativeLimit_sourceOf_projection]
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivative_of_projection

L112 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivative_of_projection
Documentation

Projecting the completed source Fox derivative evaluated on a group-like element gives the corresponding finite-stage derivative value.

Source context 10 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 (ℓ : ℕ)
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 : ℕ)
Lean source · statement
theorem primePowerCompletedGroupAlgebraFreeFoxDerivative_of_projection
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (i : X) (w : FreeGroup X) (a : ℕ) :
    (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
        (primePowerCompletedGroupAlgebraFreeFoxDerivative
          (ℓ := ℓ) (X := X) N hfinite i
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w)) =
      foxAlgebraicStageDerivative (X := X) N (ℓ ^ a) i w
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of

L133 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of
Documentation

The completed-target derivative of a group-like source element is the image of the prime-power derivative limit in the completed target group algebra.

Source context 10 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 (ℓ : ℕ)
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 : ℕ)
Lean source · statement
theorem primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of
    [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) =
      foxAlgebraicStagePrimePowerTargetLimitToCompletedGroupAlgebra
        ℓ (X := X) N
        (foxAlgebraicStagePrimePowerDerivativeLimit
          (ℓ := ℓ) (X := X) N i
          (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N w))
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_projection

L160 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_projection
Documentation

Projecting the completed-target derivative evaluated on a group-like source element gives the corresponding finite-stage derivative value.

Source context 10 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 (ℓ : ℕ)
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 : ℕ)
Lean source · statement
theorem primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_projection
    [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)
    (j : PrimePowerCompletedGroupAlgebraIndex
      (foxAlgebraicStageTargetQuotient (X := X) N)) :
    primePowerCompletedGroupAlgebraProjection
        (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
        (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
          (ℓ := ℓ) (X := X) N hfinite i
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w)) =
      modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
        (foxAlgebraicStageTargetQuotient (X := X) N) j.2
        (foxAlgebraicStageDerivative (X := X) N (ℓ ^ j.1) i w)

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