NYLL
Module

Index.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.Index
5 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — completion — source — index

The principal declarations in this module are:

  • foxCommutatorPowerOpenNormalSubgroup

The open normal subgroup associated to the finite Fox commutator-power quotient.

  • foxAlgebraicStagePrimePowerSourceCompletedIndex

The completed group-algebra index corresponding to the finite Fox commutator-power source quotient at the prime-power stage \(a\).

  • foxCommutatorPowerOpenNormalSubgroup_subgroup

The underlying subgroup of \(\mathrm{finiteFoxCommutatorPowerOpenNormalSubgroup}\) is the corresponding commutator-power subgroup.

  • foxAlgebraicStagePrimePowerSourceCompletedIndex_subgroup

The source completed index has the expected underlying commutator-power subgroup.

Imports1
Imported by3

Declarations

def

foxCommutatorPowerOpenNormalSubgroup

L45 ↗
FoxDifferential.foxCommutatorPowerOpenNormalSubgroup
Documentation

The open normal subgroup associated to the finite Fox commutator-power quotient.

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 foxCommutatorPowerOpenNormalSubgroup
    [TopologicalSpace (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) (n : ℕ) :
    OpenNormalSubgroup (FreeGroup X) where
  toOpenSubgroup :=
    { toSubgroup := foxCommutatorPowerSubgroup (F := FreeGroup X) N n
      isOpen' := isOpen_discrete _ }
  isNormal' := by
    change (foxCommutatorPowerSubgroup (F := FreeGroup X) N n).Normal
    infer_instance
theorem

foxCommutatorPowerOpenNormalSubgroup_subgroup

L63 ↗
FoxDifferential.foxCommutatorPowerOpenNormalSubgroup_subgroup
Documentation

The underlying subgroup of \(\mathrm{finiteFoxCommutatorPowerOpenNormalSubgroup}\) is the corresponding commutator-power subgroup.

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 foxCommutatorPowerOpenNormalSubgroup_subgroup
    [TopologicalSpace (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) (n : ℕ) :
    ((foxCommutatorPowerOpenNormalSubgroup (X := X) N n :
        OpenNormalSubgroup (FreeGroup X)) : Subgroup (FreeGroup X)) =
      foxCommutatorPowerSubgroup (F := FreeGroup X) N n
def

foxAlgebraicStagePrimePowerSourceCompletedIndex

L75 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSourceCompletedIndex
Documentation

The completed group-algebra index corresponding to the finite Fox commutator-power source quotient at the prime-power stage \(a\).

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 foxAlgebraicStagePrimePowerSourceCompletedIndex
    [TopologicalSpace (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (a : ℕ) : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex (FreeGroup X)
theorem

foxAlgebraicStagePrimePowerSourceCompletedIndex_subgroup

L91 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSourceCompletedIndex_subgroup
Documentation

The source completed index has the expected underlying commutator-power subgroup.

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 foxAlgebraicStagePrimePowerSourceCompletedIndex_subgroup
    [TopologicalSpace (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (a : ℕ) :
    (((OrderDual.ofDual
        (foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X)
          N hfinite a)).1 : OpenNormalSubgroup (FreeGroup X)) :
        Subgroup (FreeGroup X)) =
      foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)
theorem

foxAlgebraicStagePrimePowerSourceCompletedIndex_mono

L107 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSourceCompletedIndex_mono
Documentation

The source completed indices are monotone along prime-power stages.

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 foxAlgebraicStagePrimePowerSourceCompletedIndex_mono
    [TopologicalSpace (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X))
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    {a b : ℕ} (hab : a ≤ b) :
    foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite a ≤
      foxAlgebraicStagePrimePowerSourceCompletedIndex (ℓ := ℓ) (X := X) N hfinite b

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