NYLL
Module

Vector.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.OnGroup.Vector
5 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — derivative — on group — vector

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTargetOnGroup

The dense group-level completed-target Fox derivative vector. It evaluates the completed-target derivative vector on group-like elements of the source completed group algebra.

  • primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_apply

The prime-power completed-group-algebra Fox-derivative vector is evaluated on group elements by the corresponding completed-target finite-stage formula.

  • primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_of

On a free generator, the completed-target derivative vector has the corresponding standard basis vector as its value.

  • primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_unique

The completed-target Fox derivative vector is the unique crossed homomorphism with standard basis values.

Imports1
Imported by1

Declarations

def

primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTargetOnGroup

L50 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTargetOnGroup
Documentation

The dense group-level completed-target Fox derivative vector. It evaluates the completed-target derivative vector on group-like elements of the source completed 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 (ℓ : ℕ) [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 : ℕ)
Lean source · full declaration
def primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTargetOnGroup
    [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))) :
    ScalarCrossedHom
      (foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom (ℓ := ℓ) (X := X) N)
      (X → PrimePowerCompletedGroupAlgebra ℓ
        (foxAlgebraicStageTargetQuotient (X := X) N)) where
  toFun w := fun i =>
    primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
      (ℓ := ℓ) (X := X) N hfinite i w
  map_mul' := by
    intro u v
    funext i
    change
      primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
          (ℓ := ℓ) (X := X) N hfinite i (u * v) =
        primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
            (ℓ := ℓ) (X := X) N hfinite i u +
          foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom
              (ℓ := ℓ) (X := X) N u •
            primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
              (ℓ := ℓ) (X := X) N hfinite i v
    exact ScalarCrossedHom.map_mul
      (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
        (ℓ := ℓ) (X := X) N hfinite i) u v
theorem

primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_apply

L88 ↗
FoxDifferential.primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_apply
Documentation

The prime-power completed-group-algebra Fox-derivative vector is evaluated on group elements by the corresponding completed-target finite-stage formula.

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 primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_apply
    [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) (i : X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTargetOnGroup
        (ℓ := ℓ) (X := X) N hfinite w i =
      primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
        (ℓ := ℓ) (X := X) N hfinite i w
theorem

primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_of

L109 ↗
FoxDifferential.primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_of
Documentation

On a free generator, the completed-target derivative vector has the corresponding standard basis vector as its value.

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 primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_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)))
    (j : X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTargetOnGroup
        (ℓ := ℓ) (X := X) N hfinite (FreeGroup.of j) =
      Pi.single j
        (1 : PrimePowerCompletedGroupAlgebra ℓ
          (foxAlgebraicStageTargetQuotient (X := X) N))
theorem

primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_unique

L139 ↗
FoxDifferential.primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_unique
Documentation

The completed-target Fox derivative vector is the unique crossed homomorphism with standard basis values.

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 primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup_unique
    [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)))
    (delta : ScalarCrossedHom
      (foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom (ℓ := ℓ) (X := X) N)
      (X → PrimePowerCompletedGroupAlgebra ℓ
        (foxAlgebraicStageTargetQuotient (X := X) N)))
    (hbasis : ∀ j : X, delta (FreeGroup.of j) =
      Pi.single j
        (1 : PrimePowerCompletedGroupAlgebra ℓ
          (foxAlgebraicStageTargetQuotient (X := X) N))) :
    delta =
      primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTargetOnGroup
        (ℓ := ℓ) (X := X) N hfinite
theorem

existsUnique_primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup

L184 ↗
FoxDifferential.existsUnique_primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup
Documentation

Existence and uniqueness of the completed-target Fox derivative-vector crossed homomorphism.

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 existsUnique_primePowerCompletedGAFreeFoxDerivativeVectorToCompletedTargetOnGroup
    [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))) :
    ∃! delta : ScalarCrossedHom
        (foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom (ℓ := ℓ) (X := X) N)
        (X → PrimePowerCompletedGroupAlgebra ℓ
          (foxAlgebraicStageTargetQuotient (X := X) N)),
      ∀ j : X, delta (FreeGroup.of j) =
        Pi.single j
          (1 : PrimePowerCompletedGroupAlgebra ℓ
            (foxAlgebraicStageTargetQuotient (X := X) N))

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