NYLL
Module

CompletedTarget.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.CompletedTarget
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: finite stage — prime power — derivative — completed target

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget

The completed source Fox derivative, mapped from the finite-stage target limit into the completed group algebra of the target quotient.

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_projection

Projecting the completed-target Fox derivative gives the corresponding finite-stage derivative.

  • primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_unique

The completed-target prime-power Fox derivative is uniquely determined by all completed target finite-stage projection formulas.

  • ppCompletedGAFoxDerivToTarget_fundFormula_proj

The completed-target fundamental formula after projection to one completed target stage.

Imports1
Imported by3

Declarations

def

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget

L48 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
Documentation

The completed source Fox derivative, mapped from the finite-stage target limit into the completed group algebra of the target quotient.

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 · statement
def primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
    [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) :
    PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X) →+
      PrimePowerCompletedGroupAlgebra ℓ
        (foxAlgebraicStageTargetQuotient (X := X) N)
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_projection

L71 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_projection
Documentation

Projecting the completed-target Fox derivative gives the corresponding finite-stage derivative.

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_projection
    [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) (z : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X))
    (j : PrimePowerCompletedGroupAlgebraIndex
      (foxAlgebraicStageTargetQuotient (X := X) N)) :
    primePowerCompletedGroupAlgebraProjection
        (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
        (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
          (ℓ := ℓ) (X := X) N hfinite i z) =
      modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
        (foxAlgebraicStageTargetQuotient (X := X) N) j.2
        (foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ j.1) i
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
            (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
              N hfinite j.1) z))
theorem

primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_unique

L103 ↗
FoxDifferential.primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_unique
Documentation

The completed-target prime-power Fox derivative is uniquely determined by all completed target finite-stage projection formulas.

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_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)
    (f : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X) →+
      PrimePowerCompletedGroupAlgebra ℓ (foxAlgebraicStageTargetQuotient (X := X) N))
    (hf : ∀ z
      (j : PrimePowerCompletedGroupAlgebraIndex (foxAlgebraicStageTargetQuotient (X := X) N)),
      primePowerCompletedGroupAlgebraProjection
          (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j (f z) =
        modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
          (foxAlgebraicStageTargetQuotient (X := X) N) j.2
          (foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ j.1) i
            (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
              (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
                N hfinite j.1) z))) :
    f = primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
      (ℓ := ℓ) (X := X) N hfinite i
theorem

ppCompletedGAFoxDerivToTarget_fundFormula_proj

L143 ↗
FoxDifferential.ppCompletedGAFoxDerivToTarget_fundFormula_proj
Documentation

The completed-target fundamental formula 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_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)))
    (z : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X))
    (j : PrimePowerCompletedGroupAlgebraIndex
      (foxAlgebraicStageTargetQuotient (X := X) N)) :
    modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
        (foxAlgebraicStageTargetQuotient (X := X) N) j.2
        (foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N (ℓ ^ j.1)
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
            (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
              N hfinite j.1) z) -
          algebraMap (ModNCompletedCoeff (ℓ ^ j.1))
            (foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ j.1))
            (foxCommutatorPowerSourceGroupAlgebraAugmentation
              (F := FreeGroup X) N (ℓ ^ j.1)
              (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
                (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
                  N hfinite j.1) z))) =
      ∑ i : X,
        primePowerCompletedGroupAlgebraProjection
          (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
          (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
            (ℓ := ℓ) (X := X) N hfinite i z) *
          primePowerCompletedGroupAlgebraProjection
            (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
            (primePowerCompletedGroupAlgebraOf (ell := ℓ)
              (H := foxAlgebraicStageTargetQuotient (X := X) N)
              (QuotientGroup.mk' N (FreeGroup.of i)) - 1)
theorem

ppCompletedGAFoxDerivToTarget_fundFormula_proj_algebraMap

L202 ↗
FoxDifferential.ppCompletedGAFoxDerivToTarget_fundFormula_proj_algebraMap
Documentation

The projected completed-target fundamental formula with the augmentation term written through the target-stage algebra map.

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_fundFormula_proj_algebraMap
    [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)))
    (z : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X))
    (j : PrimePowerCompletedGroupAlgebraIndex
      (foxAlgebraicStageTargetQuotient (X := X) N)) :
    modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
        (foxAlgebraicStageTargetQuotient (X := X) N) j.2
        (foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N (ℓ ^ j.1)
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
            (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
              N hfinite j.1) z)) -
      algebraMap (ModNCompletedCoeff (ℓ ^ j.1))
        (PrimePowerCompletedGroupAlgebraStage ℓ
          (foxAlgebraicStageTargetQuotient (X := X) N) j)
        (foxCommutatorPowerSourceGroupAlgebraAugmentation
          (F := FreeGroup X) N (ℓ ^ j.1)
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
            (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
              N hfinite j.1) z)) =
      ∑ i : X,
        primePowerCompletedGroupAlgebraProjection
          (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
          (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
            (ℓ := ℓ) (X := X) N hfinite i z) *
          primePowerCompletedGroupAlgebraProjection
            (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
            (primePowerCompletedGroupAlgebraOf (ell := ℓ)
              (H := foxAlgebraicStageTargetQuotient (X := X) N)
              (QuotientGroup.mk' N (FreeGroup.of i)) - 1)
theorem

primePowerCompletedTarget_fundamentalFormula_projection_completedAugmentation

L250 ↗
FoxDifferential.primePowerCompletedTarget_fundamentalFormula_projection_completedAugmentation
Documentation

After projection to the completed target, the fundamental formula uses the source augmentation computed 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 primePowerCompletedTarget_fundamentalFormula_projection_completedAugmentation
    [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)))
    (z : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X))
    (j : PrimePowerCompletedGroupAlgebraIndex
      (foxAlgebraicStageTargetQuotient (X := X) N)) :
    modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
        (foxAlgebraicStageTargetQuotient (X := X) N) j.2
        (foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N (ℓ ^ j.1)
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
            (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
              N hfinite j.1) z)) -
      algebraMap (ModNCompletedCoeff (ℓ ^ j.1))
        (PrimePowerCompletedGroupAlgebraStage ℓ
          (foxAlgebraicStageTargetQuotient (X := X) N) j)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := FreeGroup X)
          (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
            N hfinite j.1)
          (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := FreeGroup X) z)) =
      ∑ i : X,
        primePowerCompletedGroupAlgebraProjection
          (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
          (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
            (ℓ := ℓ) (X := X) N hfinite i z) *
          primePowerCompletedGroupAlgebraProjection
            (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
            (primePowerCompletedGroupAlgebraOf (ell := ℓ)
              (H := foxAlgebraicStageTargetQuotient (X := X) N)
              (QuotientGroup.mk' N (FreeGroup.of i)) - 1)

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