Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.Basic

6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — system — limit — basic

The principal declarations in this module are:

FoxAlgebraicStagePrimePowerSourceLimit

Inverse limit of the prime-power finite Fox source group-algebra system.

FoxAlgebraicStagePrimePowerTargetLimit

Inverse limit of the prime-power finite Fox target group-algebra system.

foxAlgebraicStagePrimePowerSourceLimitToFamily_injective

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

foxAlgebraicStagePrimePowerTargetLimitToFamily_injective

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

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.System.Basic

Imported by3

abbrev

FoxAlgebraicStagePrimePowerSourceLimit

L43 ↗

FoxDifferential.FoxAlgebraicStagePrimePowerSourceLimit

Documentation

Inverse limit of the prime-power finite Fox source group-algebra 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 (ℓ : ℕ)
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 FoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) : Type u

abbrev

FoxAlgebraicStagePrimePowerTargetLimit

L48 ↗

FoxDifferential.FoxAlgebraicStagePrimePowerTargetLimit

Documentation

Inverse limit of the prime-power finite Fox target group-algebra 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 (ℓ : ℕ)
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 FoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] : Type u

def

foxAlgebraicStagePrimePowerSourceLimitToFamily

L53 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily

Documentation

Forget a source inverse-limit element to its compatible family of source 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

def foxAlgebraicStagePrimePowerSourceLimitToFamily
    (N : Subgroup (FreeGroup X)) :
    FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N →
      ((a : ℕ) → foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a)

def

foxAlgebraicStagePrimePowerTargetLimitToFamily

L60 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily

Documentation

Forget a target inverse-limit element to its compatible family of target 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

def foxAlgebraicStagePrimePowerTargetLimitToFamily
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N →
      ((a : ℕ) → foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a)

theorem

foxAlgebraicStagePrimePowerSourceLimitToFamily_injective

L68 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily_injective

Documentation

The family map out of the source 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 (ℓ : ℕ)
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 foxAlgebraicStagePrimePowerSourceLimitToFamily_injective
    (N : Subgroup (FreeGroup X)) :
    Function.Injective
      (foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N)

theorem

foxAlgebraicStagePrimePowerTargetLimitToFamily_injective

L79 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily_injective

Documentation

The family map out of the target 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 (ℓ : ℕ)
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 foxAlgebraicStagePrimePowerTargetLimitToFamily_injective
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    Function.Injective
      (foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N)

Module documentation

Fox differential: prime power — system — limit — basic

Declarations

FoxAlgebraicStagePrimePowerSourceLimit

FoxAlgebraicStagePrimePowerTargetLimit

foxAlgebraicStagePrimePowerSourceLimitToFamily

foxAlgebraicStagePrimePowerTargetLimitToFamily

foxAlgebraicStagePrimePowerSourceLimitToFamily_injective

foxAlgebraicStagePrimePowerTargetLimitToFamily_injective