ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental

2 Theorems

The principal declarations in this module are:

ppCompletedGAFoxDerivToTarget_of_fundFormula_map The completed Fox derivative satisfies the fundamental formula after passage to the target quotient. - ppCompletedGAFoxDerivToTarget_of_mul_product_map The completed Fox derivative of a product is computed by the crossed product rule after passage to the target quotient.

imports

Imported by

Theorem FoxDifferential.ppCompletedGAFoxDerivToTarget_of_fundFormula_map

theorem ppCompletedGAFoxDerivToTarget_of_fundFormula_map
    [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) :
    primePowerCompletedGroupAlgebraMap
        (ℓ := ℓ) (G := FreeGroup X)
        (H := foxAlgebraicStageTargetQuotient (X := X) N)
        (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) - 1 =
      ∑ i : X,
        primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
          (ℓ := ℓ) (X := X) N hfinite i
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) *
          (primePowerCompletedGroupAlgebraMap
            (ℓ := ℓ) (G := FreeGroup X)
            (H := foxAlgebraicStageTargetQuotient (X := X) N)
            (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
            (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X)
              (FreeGroup.of i)) - 1)

The completed Fox derivative satisfies the fundamental formula after passage to the target quotient.

Show Lean proof

Theorem FoxDifferential.ppCompletedGAFoxDerivToTarget_of_mul_product_map

theorem ppCompletedGAFoxDerivToTarget_of_mul_product_map
    [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) +
        primePowerCompletedGroupAlgebraMap
          (ℓ := ℓ) (G := FreeGroup X)
          (H := foxAlgebraicStageTargetQuotient (X := X) N)
          (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
          (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u) *
          primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
            (ℓ := ℓ) (X := X) N hfinite i
            (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v)

The completed Fox derivative of a product is computed by the crossed product rule after passage to the target quotient.

Show Lean proof

ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental

Declarations