NYLL
Module

Semidirect.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.Semidirect
11 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — system — limit — semidirect

The principal declarations in this module are:

  • FoxAlgebraicStagePrimePowerSemidirectLimit

Inverse limit of the prime-power finite Fox semidirect stage system.

  • foxAlgebraicStagePrimePowerSemidirectLimitToFamily

Forget a semidirect inverse-limit element to its compatible family of finite stages.

  • foxAlgebraicStagePrimePowerSemidirectLimitToFamily_injective

The family map out of the semidirect inverse limit is injective.

  • foxAlgebraicStagePrimePowerSemidirectLimitProjection_apply

The prime-power semidirect inverse-limit projection returns the coordinate at the selected exponent.

Imports1
Imported by2

Declarations

abbrev

FoxAlgebraicStagePrimePowerSemidirectLimit

L42 ↗
FoxDifferential.FoxAlgebraicStagePrimePowerSemidirectLimit
Documentation

Inverse limit of the prime-power finite Fox semidirect stage system.

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
abbrev FoxAlgebraicStagePrimePowerSemidirectLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] : Type u
def

foxAlgebraicStagePrimePowerSemidirectLimitToFamily

L47 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSemidirectLimitToFamily
Documentation

Forget a semidirect inverse-limit element to its compatible family of 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 (ℓ : ℕ) [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 foxAlgebraicStagePrimePowerSemidirectLimitToFamily
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    FoxAlgebraicStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N →
      ((a : ℕ) → FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a))
theorem

foxAlgebraicStagePrimePowerSemidirectLimitToFamily_injective

L55 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSemidirectLimitToFamily_injective
Documentation

The family map out of the semidirect inverse limit is injective.

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 < ℓ)] [DecidableEq X] in
Lean source · statement
theorem foxAlgebraicStagePrimePowerSemidirectLimitToFamily_injective
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    Function.Injective
      (foxAlgebraicStagePrimePowerSemidirectLimitToFamily (ℓ := ℓ) (X := X) N)
def

foxAlgebraicStagePrimePowerSemidirectLimitProjection

L65 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSemidirectLimitProjection
Documentation

The \(a\)-th finite-stage projection from the semidirect prime-power 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 (ℓ : ℕ) [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 foxAlgebraicStagePrimePowerSemidirectLimitProjection
    (N : Subgroup (FreeGroup X)) [N.Normal] (a : ℕ) :
    FoxAlgebraicStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N →
      FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a)
theorem

foxAlgebraicStagePrimePowerSemidirectLimitProjection_apply

L76 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSemidirectLimitProjection_apply
Documentation

The prime-power semidirect inverse-limit projection returns the coordinate at the selected exponent.

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 < ℓ)] [DecidableEq X] in
Lean source · statement
theorem foxAlgebraicStagePrimePowerSemidirectLimitProjection_apply
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (z : FoxAlgebraicStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N) (a : ℕ) :
    foxAlgebraicStagePrimePowerSemidirectLimitProjection (ℓ := ℓ) (X := X) N a z = z.1 a
theorem

foxAlgebraicStagePrimePowerSemidirectLimitProjection_transition

L87 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSemidirectLimitProjection_transition
Documentation

The finite-stage projections of a semidirect limit element are compatible with the prime-power transition maps.

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 < ℓ)] [DecidableEq X] in
Lean source · statement
theorem foxAlgebraicStagePrimePowerSemidirectLimitProjection_transition
    (N : Subgroup (FreeGroup X)) [N.Normal]
    {a b : ℕ} (hab : a ≤ b)
    (z : FoxAlgebraicStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab
        (foxAlgebraicStagePrimePowerSemidirectLimitProjection (ℓ := ℓ) (X := X) N b z) =
      foxAlgebraicStagePrimePowerSemidirectLimitProjection (ℓ := ℓ) (X := X) N a z
def

foxAlgebraicStagePrimePowerSemidirectLimitBoundaryCycleSet

L98 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSemidirectLimitBoundaryCycleSet
Documentation

Boundary-cycle condition for a prime-power semidirect limit element, read stagewise.

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 foxAlgebraicStagePrimePowerSemidirectLimitBoundaryCycleSet
    [Fintype X]
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    Set (FoxAlgebraicStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N)
theorem

mem_foxAlgebraicStagePrimePowerSemidirectLimitBoundaryCycleSet

L112 ↗
FoxDifferential.mem_foxAlgebraicStagePrimePowerSemidirectLimitBoundaryCycleSet
Documentation

Membership in the finite-stage boundary-cycle object is characterized by the corresponding boundary-vanishing condition.

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 [DecidableEq X] in
Lean source · statement
theorem mem_foxAlgebraicStagePrimePowerSemidirectLimitBoundaryCycleSet
    {ℓ : ℕ} [Fact (0 < ℓ)] [Fintype X]
    {N : Subgroup (FreeGroup X)} [N.Normal]
    {z : FoxAlgebraicStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N} :
    z ∈ foxAlgebraicStagePrimePowerSemidirectLimitBoundaryCycleSet (ℓ := ℓ) (X := X) N ↔
      ∀ a : ℕ,
        foxAlgebraicStagePrimePowerSemidirectLimitProjection (ℓ := ℓ) (X := X) N a z ∈
          foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N (ℓ ^ a)
def

foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit

L126 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit
Documentation

The compatible semidirect limit point represented by the finite kernel-word points for one 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 (ℓ : ℕ) [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 foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] (w : FreeGroup X) :
    FoxAlgebraicStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N
theorem

foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit_projection

L141 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit_projection
Documentation

The kernel-word point in the semidirect inverse limit projects to the corresponding finite semidirect 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 foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit_projection
    (N : Subgroup (FreeGroup X)) [N.Normal] (w : FreeGroup X) (a : ℕ) :
    foxAlgebraicStagePrimePowerSemidirectLimitProjection (ℓ := ℓ) (X := X) N a
        (foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit
          (ℓ := ℓ) (X := X) N w) =
      foxAlgebraicStageSemidirectKernelWordPoint (X := X) N (ℓ ^ a) w
theorem

foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit_mem_boundaryCycleSet

L154 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit_mem_boundaryCycleSet
Documentation

If w is a relation word, its compatible prime-power semidirect point is a stagewise boundary cycle.

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 foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit_mem_boundaryCycleSet
    [Fintype X]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    {w : FreeGroup X} (hw : w ∈ N) :
    foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit (ℓ := ℓ) (X := X) N w ∈
      foxAlgebraicStagePrimePowerSemidirectLimitBoundaryCycleSet (ℓ := ℓ) (X := X) N

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