Module

Fundamental.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Fundamental

2 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — derivative — source — fundamental

The principal declarations in this module are:

ppCompletedGAFoxDerivToTarget_of_fundFormula_proj

The completed-target Fox fundamental formula for a group-like source element after projection to one completed target stage.

ppCompletedGAFoxDerivToTarget_of_fundFormula

The completed-target Fox fundamental formula for a group-like source element.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.GroupLike

Imported by4

theorem

ppCompletedGAFoxDerivToTarget_of_fundFormula_proj

L44 ↗

FoxDifferential.ppCompletedGAFoxDerivToTarget_of_fundFormula_proj

Documentation

The completed-target Fox fundamental formula for a group-like source element after projection to one completed target stage.

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 ppCompletedGAFoxDerivToTarget_of_fundFormula_proj
    [Fintype X]
    [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)
    (j : PrimePowerCompletedGroupAlgebraIndex
      (foxAlgebraicStageTargetQuotient (X := X) N)) :
    primePowerCompletedGroupAlgebraProjection
        (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
        (primePowerCompletedGroupAlgebraOf (ell := ℓ)
          (H := foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w) - 1) =
      ∑ i : X,
        primePowerCompletedGroupAlgebraProjection
          (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
          (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
            (ℓ := ℓ) (X := X) N hfinite i
            (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w)) *
          primePowerCompletedGroupAlgebraProjection
            (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
            (primePowerCompletedGroupAlgebraOf (ell := ℓ)
              (H := foxAlgebraicStageTargetQuotient (X := X) N)
              (QuotientGroup.mk' N (FreeGroup.of i)) - 1)