Module

Limit.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Limit

8 declarations indexed from sourceView source ↗

Module documentation

Fox differential: finite stage — prime power — derivative — limit

The principal declarations in this module are:

foxAlgebraicStagePrimePowerDerivativeLimit

The inverse-limit Fox derivative obtained by applying the finite-stage derivative at every prime-power stage.

foxAlgebraicStagePrimePowerDerivativeLimitAddHom

The additive-homomorphism version of the prime-power derivative limit.

foxAlgebraicStagePrimePowerGroupAlgebraDerivative_transition

Naturality of the finite-stage group-algebra Fox derivative along a prime-power transition.

foxAlgebraicStagePrimePowerDerivativeLimit_projection

Projecting the prime-power derivative limit gives the corresponding finite derivative coordinate.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Target

Imported by3

theorem

foxAlgebraicStagePrimePowerGroupAlgebraDerivative_transition

L44 ↗

FoxDifferential.foxAlgebraicStagePrimePowerGroupAlgebraDerivative_transition

Documentation

Naturality of the finite-stage group-algebra Fox derivative along a prime-power transition.

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 (ℓ : ℕ)
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

theorem foxAlgebraicStagePrimePowerGroupAlgebraDerivative_transition
    (N : Subgroup (FreeGroup X)) [N.Normal] {a b : ℕ} (hab : a ≤ b) (i : X)
    (x : foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b) :
    foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N
        (primePow_dvd_primePow (ℓ := ℓ) hab)
        (foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ b) i x) =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        (foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab x)

def

foxAlgebraicStagePrimePowerDerivativeLimit

L59 ↗

FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimit

Documentation

The inverse-limit Fox derivative obtained by applying the finite-stage derivative at every prime-power stage.

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 (ℓ : ℕ)
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 foxAlgebraicStagePrimePowerDerivativeLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] (i : X) :
    FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N →
      FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N

theorem

foxAlgebraicStagePrimePowerDerivativeLimit_projection

L106 ↗

FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimit_projection

Documentation

Projecting the prime-power derivative limit gives the corresponding finite derivative coordinate.

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 (ℓ : ℕ)
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

theorem foxAlgebraicStagePrimePowerDerivativeLimit_projection
    (N : Subgroup (FreeGroup X)) [N.Normal] (i : X)
    (z : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) (a : ℕ) :
    (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
        (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i z) =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a z)

theorem

foxAlgebraicStagePrimePowerDerivativeLimit_unique

L118 ↗

FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimit_unique

Documentation

The prime-power finite-stage derivative limit is uniquely determined by its projections to all finite stages.

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 (ℓ : ℕ)
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

theorem foxAlgebraicStagePrimePowerDerivativeLimit_unique
    (N : Subgroup (FreeGroup X)) [N.Normal] (i : X)
    (f : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N →
      FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N)
    (hf : ∀ z a,
      (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
          (f z) =
        foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
          ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a z)) :
    f = foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i

theorem

foxAlgebraicStagePrimePowerDerivativeLimit_fundamental_formula_projection

L141 ↗

FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimit_fundamental_formula_projection

Documentation

The finite-stage fundamental formula, expressed after projecting a prime-power derivative limit to one stage.

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 (ℓ : ℕ)
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

theorem foxAlgebraicStagePrimePowerDerivativeLimit_fundamental_formula_projection
    [Fintype X]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (z : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) (a : ℕ) :
    foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N (ℓ ^ a)
        ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a z) -
        algebraMap (ModNCompletedCoeff (ℓ ^ a))
          (foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ a))
          (foxCommutatorPowerSourceGroupAlgebraAugmentation
            (F := FreeGroup X) N (ℓ ^ a)
            ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a z)) =
      ∑ i : X,
        (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from
          (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
            (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i z)) *
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1) := by
  rw [foxAlgebraicStageGroupAlgebraDerivative_groupAlgebra_fundamental_formula
    (X := X) (N := N) (n := ℓ ^ a)
    ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a z)]
  apply Finset.sum_congr rfl
  intro i _hi
  rw [foxAlgebraicStagePrimePowerDerivativeLimit_projection]

def

foxAlgebraicStagePrimePowerDerivativeLimitAddHom

L167 ↗

FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimitAddHom

Documentation

The additive-homomorphism version of the prime-power derivative limit.

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 (ℓ : ℕ)
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 foxAlgebraicStagePrimePowerDerivativeLimitAddHom
    (N : Subgroup (FreeGroup X)) [N.Normal] (i : X) :
    FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N →+
      FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N where
  toFun := foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i
  map_zero' := by
    apply foxAlgebraicStagePrimePowerTargetLimitToFamily_injective (ℓ := ℓ) (X := X) N
    funext a
    change
      (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
          (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i 0) =
        (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
          (0 : FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N)
    rw [foxAlgebraicStagePrimePowerDerivativeLimit_projection]
    change foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a
          (0 : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N)) = 0
    change foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        (0 : foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a) = 0
    exact map_zero _
  map_add' x y := by
    apply foxAlgebraicStagePrimePowerTargetLimitToFamily_injective (ℓ := ℓ) (X := X) N
    funext a
    change
      (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
          (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i (x + y)) =
        (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from
          (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
            (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i x)) +
        (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from
          (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
            (foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i y))
    rw [foxAlgebraicStagePrimePowerDerivativeLimit_projection,
      foxAlgebraicStagePrimePowerDerivativeLimit_projection,
      foxAlgebraicStagePrimePowerDerivativeLimit_projection]
    change foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a (x + y)) =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a x) +
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a y)
    change foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        ((show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from
          (foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a x) +
          (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from
            (foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a y)) =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a x) +
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
        ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a y)
    exact map_add _ _ _

theorem

foxAlgebraicStagePrimePowerDerivativeLimitAddHom_apply

L221 ↗

FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimitAddHom_apply

Documentation

Evaluation formula for the additive-homomorphism version of the derivative limit.

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 (ℓ : ℕ)
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

theorem foxAlgebraicStagePrimePowerDerivativeLimitAddHom_apply
    (N : Subgroup (FreeGroup X)) [N.Normal] (i : X)
    (z : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerDerivativeLimitAddHom (ℓ := ℓ) (X := X) N i z =
      foxAlgebraicStagePrimePowerDerivativeLimit (ℓ := ℓ) (X := X) N i z

theorem

foxAlgebraicStagePrimePowerDerivativeLimitAddHom_unique

L231 ↗

FoxDifferential.foxAlgebraicStagePrimePowerDerivativeLimitAddHom_unique

Documentation

Additive maps into the prime-power finite-stage target limit are uniquely determined by the finite-stage Fox derivative projection formula.

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 (ℓ : ℕ)
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

theorem foxAlgebraicStagePrimePowerDerivativeLimitAddHom_unique
    (N : Subgroup (FreeGroup X)) [N.Normal] (i : X)
    (f : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N →+
      FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N)
    (hf : ∀ z a,
      (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
          (f z) =
        foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ a) i
          ((foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a z)) :
    f = foxAlgebraicStagePrimePowerDerivativeLimitAddHom (ℓ := ℓ) (X := X) N i

Module documentation

Fox differential: finite stage — prime power — derivative — limit

Declarations