NYLL
Module

Relators.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Derivative.Relators
11 declarations indexed from sourceView source ↗

Module documentation

Fox differential: finite stage — stage — derivative — relators

The principal declarations in this module are:

  • foxAlgebraicStageLift_right_eq_one_of_mem

If a word lies in N, the finite-stage lift has trivial right component.

  • mem_ker_foxAlgebraicStageLift_iff

Membership in the kernel of the finite Fox stage lift is equivalent to vanishing of the corresponding finite-stage coordinate.

  • ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff

The finite-stage Magnus reverse inclusion is equivalent to the derivative-zero criterion inside \(N\).

  • foxAlgebraicStageSemidirect_commutator_eq_one_of_right_one

In the finite-stage semidirect product, commutators of elements with trivial right component are trivial.

Imports1
Imported by4

Declarations

theorem

foxAlgebraicStageLift_right_eq_one_of_mem

L46 ↗
FoxDifferential.foxAlgebraicStageLift_right_eq_one_of_mem
Documentation

If a word lies in N, the finite-stage lift has trivial right component.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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
theorem foxAlgebraicStageLift_right_eq_one_of_mem
    {a : FreeGroup X} (ha : a ∈ N) :
    (foxAlgebraicStageLift (X := X) N n a).right = 1
theorem

mem_ker_foxAlgebraicStageLift_iff

L57 ↗
FoxDifferential.mem_ker_foxAlgebraicStageLift_iff
Documentation

Membership in the kernel of the finite Fox stage lift is equivalent to vanishing of the corresponding finite-stage 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
open scoped commutatorElement
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
theorem mem_ker_foxAlgebraicStageLift_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {w : FreeGroup X} :
    w ∈ (foxAlgebraicStageLift (X := X) N n).ker ↔
      w ∈ N ∧ foxAlgebraicStageDerivativeVector (X := X) N n w = 0
theorem

ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff

L83 ↗
FoxDifferential.ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff
Documentation

The finite-stage Magnus reverse inclusion is equivalent to the derivative-zero criterion inside \(N\).

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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
theorem ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff
    (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ) :
    (foxAlgebraicStageLift (X := X) N n).ker ≤
        foxCommutatorPowerSubgroup (F := FreeGroup X) N n ↔
      ∀ w : FreeGroup X,
        w ∈ N →
        foxAlgebraicStageDerivativeVector (X := X) N n w = 0 →
          w ∈ foxCommutatorPowerSubgroup (F := FreeGroup X) N n
theorem

foxAlgebraicStageSemidirect_commutator_eq_one_of_right_one

L105 ↗
FoxDifferential.foxAlgebraicStageSemidirect_commutator_eq_one_of_right_one
Documentation

In the finite-stage semidirect product, commutators of elements with trivial right component are trivial.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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 foxAlgebraicStageSemidirect_commutator_eq_one_of_right_one
    (a b : FoxAlgebraicStageSemidirect (X := X) N n)
    (ha : a.right = 1) (hb : b.right = 1) :
    ⁅a, b⁆ = 1
theorem

foxAlgebraicStageLift_commutator_eq_one_of_mem

L129 ↗
FoxDifferential.foxAlgebraicStageLift_commutator_eq_one_of_mem
Documentation

The finite-stage lift kills commutators of words in \(N\).

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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
theorem foxAlgebraicStageLift_commutator_eq_one_of_mem
    {a b : FreeGroup X} (ha : a ∈ N) (hb : b ∈ N) :
    foxAlgebraicStageLift (X := X) N n ⁅a, b⁆ = 1
theorem

foxAlgebraicStageSemidirect_pow_right_eq_one_of_right_one

L145 ↗
FoxDifferential.foxAlgebraicStageSemidirect_pow_right_eq_one_of_right_one
Documentation

Powers of a finite-stage semidirect element with trivial right component still have trivial right component.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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 foxAlgebraicStageSemidirect_pow_right_eq_one_of_right_one
    (a : FoxAlgebraicStageSemidirect (X := X) N n)
    (ha : a.right = 1) (m : ℕ) :
    (a ^ m).right = 1
theorem

foxAlgebraicStageSemidirect_pow_left_of_right_one

L161 ↗
FoxDifferential.foxAlgebraicStageSemidirect_pow_left_of_right_one
Documentation

Powers of a finite-stage semidirect element with trivial right component scale the left component by the exponent.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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 foxAlgebraicStageSemidirect_pow_left_of_right_one
    (a : FoxAlgebraicStageSemidirect (X := X) N n)
    (ha : a.right = 1) (m : ℕ) :
    (a ^ m).left = m • a.left
theorem

foxAlgebraicStageSemidirect_pow_char_eq_one_of_right_one

L192 ↗
FoxDifferential.foxAlgebraicStageSemidirect_pow_char_eq_one_of_right_one
Documentation

The \(n\)-th power of a finite-stage semidirect element with trivial right component is trivial over \(\mathbb{Z}/n\mathbb{Z}\).

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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 foxAlgebraicStageSemidirect_pow_char_eq_one_of_right_one
    (a : FoxAlgebraicStageSemidirect (X := X) N n)
    (ha : a.right = 1) :
    a ^ n = 1
theorem

foxAlgebraicStageLift_pow_eq_one_of_mem

L203 ↗
FoxDifferential.foxAlgebraicStageLift_pow_eq_one_of_mem
Documentation

The finite-stage lift kills \(n\)-th powers of words in \(N\).

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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
theorem foxAlgebraicStageLift_pow_eq_one_of_mem
    {a : FreeGroup X} (ha : a ∈ N) :
    foxAlgebraicStageLift (X := X) N n (a ^ n) = 1
theorem

foxCommutatorPowerRelatorSet_subset_ker_foxAlgebraicStageLift

L212 ↗
FoxDifferential.foxCommutatorPowerRelatorSet_subset_ker_foxAlgebraicStageLift
Documentation

The finite Fox commutator-power relators lie in the kernel of the finite-stage lift.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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
theorem foxCommutatorPowerRelatorSet_subset_ker_foxAlgebraicStageLift :
    foxCommutatorPowerRelatorSet (F := FreeGroup X) N n ⊆
      (foxAlgebraicStageLift (X := X) N n).ker
theorem

foxCommutatorPowerSubgroup_le_ker_foxAlgebraicStageLift

L222 ↗
FoxDifferential.foxCommutatorPowerSubgroup_le_ker_foxAlgebraicStageLift
Documentation

The finite Fox commutator-power subgroup lies in the kernel of the finite-stage lift.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped commutatorElement
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
theorem foxCommutatorPowerSubgroup_le_ker_foxAlgebraicStageLift :
    foxCommutatorPowerSubgroup (F := FreeGroup X) N n ≤
      (foxAlgebraicStageLift (X := X) N n).ker

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