NYLL
Module

LimitMap.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.LimitMap
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — completion — source — limit map

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit

The additive map from the completed source group algebra to the prime-power finite-stage source inverse limit.

  • primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_one

The completed-source-to-finite-stage-limit map preserves \(1\).

  • primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_mul

The completed-source-to-finite-stage-limit map preserves multiplication.

  • primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_projection

Projecting the completed-source-to-finite-stage-limit map gives the corresponding finite-stage limit coordinate.

Imports1
Imported by3

Declarations

def

primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit

L48 ↗
FoxDifferential.primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
Documentation

The additive map from the completed source group algebra to the prime-power finite-stage source inverse 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 primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a))) :
    PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X) →+
      FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N where
  toFun z :=
    ⟨fun a =>
        primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
          (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite a) z,
      by
        intro a b hab
        change foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
            (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
              (b, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite b)
                  z) =
          primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
            (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite a) z
        exact z.2
          (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite a)
          (b, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite b)
          ⟨hab,
            foxAlgebraicStagePrimePowerSourceCompletedIndex_mono
              (ℓ := ℓ) (X := X) N hfinite hab⟩⟩
  map_zero' := by
    apply foxAlgebraicStagePrimePowerSourceLimitToFamily_injective (ℓ := ℓ) (X := X) N
    funext a
    change primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
        (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite a)
        (0 : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X)) = 0
    exact primePowerCompletedGroupAlgebraProjection_zero (ℓ := ℓ) (G := FreeGroup X) _
  map_add' x y := by
    apply foxAlgebraicStagePrimePowerSourceLimitToFamily_injective (ℓ := ℓ) (X := X) N
    funext a
    change primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
        (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite a)
        (x + y) =
      primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
        (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite a) x +
      primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
        (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite a) y
    exact primePowerCompletedGroupAlgebraProjection_add (ℓ := ℓ) (G := FreeGroup X) _ x y
theorem

primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_one

L97 ↗
FoxDifferential.primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_one
Documentation

The completed-source-to-finite-stage-limit map preserves \(1\).

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 (ℓ : ℕ)
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 [DecidableEq X] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_one
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a))) :
    primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
        (ℓ := ℓ) (X := X) N hfinite
        (1 : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X)) = 1
theorem

primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_mul

L117 ↗
FoxDifferential.primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_mul
Documentation

The completed-source-to-finite-stage-limit map preserves multiplication.

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 (ℓ : ℕ)
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 [DecidableEq X] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_mul
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (x y : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X)) :
    primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
        (ℓ := ℓ) (X := X) N hfinite (x * y) =
      primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
          (ℓ := ℓ) (X := X) N hfinite x *
        primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
          (ℓ := ℓ) (X := X) N hfinite y
theorem

primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_projection

L148 ↗
FoxDifferential.primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_projection
Documentation

Projecting the completed-source-to-finite-stage-limit map gives the corresponding finite-stage limit coordinate.

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 (ℓ : ℕ)
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 [DecidableEq X] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_projection
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (z : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X)) (a : ℕ) :
    (foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a
        (primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
          (ℓ := ℓ) (X := X) N hfinite z) =
      primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
        (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite a) z
theorem

primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_surjective

L169 ↗
FoxDifferential.primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_surjective
Documentation

The restriction from the genuine completed group algebra to the completed-free-derivative source subsystem is surjective. This stays inside completed group algebras and inverse limits: each source stage is one of the finite completed group-algebra stages, and the stage projections are already surjective.

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 (ℓ : ℕ)
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 [DecidableEq X] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_surjective
    [Fact (0 < ℓ)]
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a))) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
        (ℓ := ℓ) (X := X) N hfinite)
theorem

foxCommutatorPowerSourceGroupAlgebraAugmentation_projection_eq_completed

L267 ↗
FoxDifferential.foxCommutatorPowerSourceGroupAlgebraAugmentation_projection_eq_completed
Documentation

The compatibility between source-stage augmentation and completed-group-algebra augmentation after projecting to a finite Fox source 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 (ℓ : ℕ)
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 [DecidableEq X] in
Lean source · statement
theorem foxCommutatorPowerSourceGroupAlgebraAugmentation_projection_eq_completed
    [TopologicalSpace (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (z : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X)) (a : ℕ) :
    foxCommutatorPowerSourceGroupAlgebraAugmentation
        (F := FreeGroup X) N (ℓ ^ a)
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
          (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
            N hfinite a) z) =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := FreeGroup X)
        (a, foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
          N hfinite a)
        (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := FreeGroup X) z)

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