NYLL
Module

Scalar.lean

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

Module documentation

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

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup

The dense group-level form of the completed-target Fox derivative. This is the completed-target derivative evaluated on group-like elements of the source completed group algebra.

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_apply

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

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_of

On a free generator, the group-level completed-target Fox derivative has the expected Kronecker generator value.

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_unique

The group-level completed-target Fox derivative is the unique crossed homomorphism with its standard Kronecker values on free generators.

Imports1
Imported by2

Declarations

def

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup

L50 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
Documentation

The dense group-level form of the completed-target Fox derivative. This is the completed-target derivative evaluated 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 primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
    [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) :
    ScalarCrossedHom
      (foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom (ℓ := ℓ) (X := X) N)
      (PrimePowerCompletedGroupAlgebra ℓ
        (foxAlgebraicStageTargetQuotient (X := X) N)) where
  toFun w := primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
      (ℓ := ℓ) (X := X) N hfinite i
      (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w)
  map_mul' := by
    intro u v
    simpa only [scalarCrossedAction_apply,
      foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom_apply, smul_eq_mul]
      using primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_mul
        (ℓ := ℓ) (X := X) N hfinite i u v
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_apply

L80 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_apply
Documentation

The Fox derivative from the prime-power completed group algebra to the completed target is evaluated on group elements by the corresponding 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 primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_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)))
    (i : X) (w : FreeGroup X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
        (ℓ := ℓ) (X := X) N hfinite i w =
      primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite i
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w)
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_of

L102 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_of
Documentation

On a free generator, the group-level completed-target Fox derivative has the expected Kronecker generator 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 primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_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 j : X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup
        (ℓ := ℓ) (X := X) N hfinite i (FreeGroup.of j) =
      ((Pi.single i
        (1 : PrimePowerCompletedGroupAlgebra ℓ
          (foxAlgebraicStageTargetQuotient (X := X) N))) :
        X → PrimePowerCompletedGroupAlgebra ℓ
          (foxAlgebraicStageTargetQuotient (X := X) N)) j
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_unique

L154 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup_unique
Documentation

The group-level completed-target Fox derivative is the unique crossed homomorphism with its standard Kronecker values on free generators.

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

existsUnique_ppCompletedGAFoxDerivToTargetOnGroup

L208 ↗
FoxDifferential.existsUnique_ppCompletedGAFoxDerivToTargetOnGroup
Documentation

Existence and uniqueness of the completed-target Fox crossed homomorphism 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 existsUnique_ppCompletedGAFoxDerivToTargetOnGroup
    [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) :
    ∃! delta : ScalarCrossedHom
        (foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom (ℓ := ℓ) (X := X) N)
        (PrimePowerCompletedGroupAlgebra ℓ
          (foxAlgebraicStageTargetQuotient (X := X) N)),
      ∀ j : X, delta (FreeGroup.of j) =
        ((Pi.single i
          (1 : PrimePowerCompletedGroupAlgebra ℓ
            (foxAlgebraicStageTargetQuotient (X := X) N))) :
          X → PrimePowerCompletedGroupAlgebra ℓ
            (foxAlgebraicStageTargetQuotient (X := X) N)) j

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