NYLL
Module

Mul.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Mul
4 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — derivative — source — mul

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraFreeFoxDerivative_of_mul

Product rule for the completed source Fox derivative on group-like source elements.

  • primePowerCompletedGroupAlgebraFreeFoxDerivative_of_mul_product

Product rule for the completed source Fox derivative when the source product is written in the completed group algebra.

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_mul

Product rule for the completed-target Fox derivative on group-like source elements.

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_mul_product

Product rule for the completed-target Fox derivative when the source product is written in the completed group algebra.

Imports1
Imported by4

Declarations

theorem

primePowerCompletedGroupAlgebraFreeFoxDerivative_of_mul

L46 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivative_of_mul
Documentation

Product rule for the completed source Fox derivative 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 primePowerCompletedGroupAlgebraFreeFoxDerivative_of_mul
    [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) (u v : FreeGroup X) :
      primePowerCompletedGroupAlgebraFreeFoxDerivative
        (ℓ := ℓ) (X := X) N hfinite i
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) (u * v)) =
      primePowerCompletedGroupAlgebraFreeFoxDerivative
          (ℓ := ℓ) (X := X) N hfinite i
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u) +
        foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N u *
          primePowerCompletedGroupAlgebraFreeFoxDerivative
            (ℓ := ℓ) (X := X) N hfinite i
            (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v)
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivative_of_mul_product

L76 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivative_of_mul_product
Documentation

Product rule for the completed source Fox derivative when the source product is written in the completed group algebra.

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 primePowerCompletedGroupAlgebraFreeFoxDerivative_of_mul_product
    [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) (u v : FreeGroup X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivative
        (ℓ := ℓ) (X := X) N hfinite i
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u *
          primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v) =
      primePowerCompletedGroupAlgebraFreeFoxDerivative
          (ℓ := ℓ) (X := X) N hfinite i
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u) +
        foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N u *
          primePowerCompletedGroupAlgebraFreeFoxDerivative
            (ℓ := ℓ) (X := X) N hfinite i
            (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v)
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_mul

L101 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_mul
Documentation

Product rule for the completed-target Fox derivative 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 primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_mul
    [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) (u v : FreeGroup X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite i
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) (u * v)) =
      primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
          (ℓ := ℓ) (X := X) N hfinite i
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u) +
        primePowerCompletedGroupAlgebraOf (ell := ℓ)
          (H := foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N u) *
          primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
            (ℓ := ℓ) (X := X) N hfinite i
            (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v)
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_mul_product

L133 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_mul_product
Documentation

Product rule for the completed-target Fox derivative when the source product is written in the completed group algebra.

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_of_mul_product
    [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) (u v : FreeGroup X) :
    primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
        (ℓ := ℓ) (X := X) N hfinite i
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u *
          primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v) =
      primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
          (ℓ := ℓ) (X := X) N hfinite i
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u) +
        primePowerCompletedGroupAlgebraOf (ell := ℓ)
          (H := foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N u) *
          primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
            (ℓ := ℓ) (X := X) N hfinite i
            (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v)

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