Module

Vector.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Vector

2 declarations indexed from sourceView source ↗

Module documentation

Fox differential: finite stage — prime power — derivative — vector

The principal declarations in this module are:

primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget

The vector of all completed-target Fox derivatives, indexed by free generators.

primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget_apply

Evaluation of the completed-target derivative vector at a coordinate.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.CompletedTarget

Imported by2

def

primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget

L39 ↗

FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget

Documentation

The vector of all completed-target Fox derivatives, indexed by free generators.

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

def primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget
    [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))) :
    PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X) →+
      (X → PrimePowerCompletedGroupAlgebra ℓ
        (foxAlgebraicStageTargetQuotient (X := X) N)) where
  toFun z i :=
    primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
      (ℓ := ℓ) (X := X) N hfinite i z
  map_zero' := by
    funext i
    exact map_zero
      (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite i)
  map_add' z z' := by
    funext i
    exact map_add
      (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite i) z z'

theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget_apply

L67 ↗

FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget_apply