Module

Representatives.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.Representatives

13 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — completion — source — representatives

The principal declarations in this module are:

foxAlgebraicStagePrimePowerSourceOf

The compatible source-limit family represented by a free-group word.

foxAlgebraicStagePrimePowerTargetOf

The compatible target-limit family represented by a free-group word.

foxAlgebraicStagePrimePowerSourceOf_projection

Projecting the source-limit element represented by a word gives the corresponding finite-stage source coordinate.

foxAlgebraicStagePrimePowerSourceProjection_eq_sourceOf_projection

Projecting a group-like free-group algebra element to a source stage agrees with the corresponding source-limit projection.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.LimitMap

Imported by2

def

foxAlgebraicStagePrimePowerSourceOf

L45 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceOf

Documentation

The compatible source-limit family represented by a free-group word.

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 foxAlgebraicStagePrimePowerSourceOf
    (N : Subgroup (FreeGroup X)) (w : FreeGroup X) :
    FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N

theorem

foxAlgebraicStagePrimePowerSourceOf_projection

L75 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceOf_projection

Documentation

Projecting the source-limit element represented by a word gives the corresponding finite-stage source 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 foxAlgebraicStagePrimePowerSourceOf_projection
    (N : Subgroup (FreeGroup X)) (w : FreeGroup X) (a : ℕ) :
    (foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a
        (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N w) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
        (FreeGroup X ⧸
          foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a))
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)) w)

theorem

foxAlgebraicStagePrimePowerSourceProjection_eq_sourceOf_projection

L91 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceProjection_eq_sourceOf_projection

Documentation

Projecting a group-like free-group algebra element to a source stage agrees with the corresponding source-limit projection.

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 foxAlgebraicStagePrimePowerSourceProjection_eq_sourceOf_projection
    (N : Subgroup (FreeGroup X)) (w : FreeGroup X) (a : ℕ) :
    foxAlgebraicStagePrimePowerSourceProjection (ℓ := ℓ) (X := X) N a
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a)) (FreeGroup X) w) =
      (foxAlgebraicStagePrimePowerSourceSystem (ℓ := ℓ) (X := X) N).projection a
        (foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N w)

theorem

primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_of

L106 ↗

FoxDifferential.primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_of

Documentation

The completed-source-to-finite-stage-limit map sends a group-like completed element to the source-limit element represented by the same word.

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_of
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (w : FreeGroup X) :
    primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
        (ℓ := ℓ) (X := X) N hfinite
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) =
      foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N w

theorem

primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_sub_one

L135 ↗

FoxDifferential.primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit_sub_one

Documentation

The source-limit bridge sends the completed group-like boundary \([w]-1\) to the corresponding source-limit boundary.

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_sub_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)))
    (w : FreeGroup X) :
    primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit
        (ℓ := ℓ) (X := X) N hfinite
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w - 1) =
      foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N w - 1

def

foxAlgebraicStagePrimePowerTargetOf

L152 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetOf

Documentation

The compatible target-limit family represented by a free-group word.

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 foxAlgebraicStagePrimePowerTargetOf
    (N : Subgroup (FreeGroup X)) [N.Normal] (w : FreeGroup X) :
    FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N

theorem

foxAlgebraicStagePrimePowerTargetOf_projection

L176 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetOf_projection

Documentation

Projecting the target-limit element represented by a word gives the corresponding finite-stage target 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 foxAlgebraicStagePrimePowerTargetOf_projection
    (N : Subgroup (FreeGroup X)) [N.Normal] (w : FreeGroup X) (a : ℕ) :
    (foxAlgebraicStagePrimePowerTargetSystem (ℓ := ℓ) (X := X) N).projection a
        (foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N w) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
        (foxAlgebraicStageTargetQuotient (X := X) N)
        (QuotientGroup.mk' N w)

theorem

foxAlgebraicStagePrimePowerTargetLimitToCompletedGroupAlgebra_targetOf

L190 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToCompletedGroupAlgebra_targetOf

Documentation

The target-limit-to-completed-group-algebra map sends a represented word to the corresponding group-like element in the completed target 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 (ℓ : ℕ)
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 foxAlgebraicStagePrimePowerTargetLimitToCompletedGroupAlgebra_targetOf
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
    (w : FreeGroup X) :
    foxAlgebraicStagePrimePowerTargetLimitToCompletedGroupAlgebra
        ℓ (X := X) N
        (foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N w) =
      primePowerCompletedGroupAlgebraOf (ell := ℓ)
        (H := foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w)

theorem

foxAlgebraicStagePrimePowerTargetOf_toFamily

L221 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetOf_toFamily

Documentation

Family-level projection formula for the target-limit element represented by a word.

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 foxAlgebraicStagePrimePowerTargetOf_toFamily
    (N : Subgroup (FreeGroup X)) [N.Normal] (w : FreeGroup X) (a : ℕ) :
    foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N
        (foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N w) a =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
        (foxAlgebraicStageTargetQuotient (X := X) N)
        (QuotientGroup.mk' N w)

theorem

foxAlgebraicStagePrimePowerSourceOf_one

L232 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceOf_one

Documentation

The source-limit element represented by the identity word is one.

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 foxAlgebraicStagePrimePowerSourceOf_one
    (N : Subgroup (FreeGroup X)) :
    foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N (1 : FreeGroup X) = 1

theorem

foxAlgebraicStagePrimePowerSourceOf_mul

L247 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceOf_mul

Documentation

The source-limit representative of a product is the product of source-limit representatives.

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 foxAlgebraicStagePrimePowerSourceOf_mul
    (N : Subgroup (FreeGroup X)) (u v : FreeGroup X) :
    foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N (u * v) =
      foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N u *
        foxAlgebraicStagePrimePowerSourceOf (ℓ := ℓ) (X := X) N v

theorem

foxAlgebraicStagePrimePowerTargetOf_one

L272 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetOf_one

Documentation

The target-limit element represented by the identity word is one.

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 foxAlgebraicStagePrimePowerTargetOf_one
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N (1 : FreeGroup X) = 1

theorem

foxAlgebraicStagePrimePowerTargetOf_mul

L287 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetOf_mul

Documentation

The target-limit representative of a product is the product of target-limit representatives.

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 foxAlgebraicStagePrimePowerTargetOf_mul
    (N : Subgroup (FreeGroup X)) [N.Normal] (u v : FreeGroup X) :
    foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N (u * v) =
      foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N u *
        foxAlgebraicStagePrimePowerTargetOf (ℓ := ℓ) (X := X) N v

Module documentation

Fox differential: prime power — completion — source — representatives

Declarations