NYLL
Module

Source.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.CoeffMap.Source
10 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — coeff map — source

The principal declarations in this module are:

  • foxAlgebraicStageSameSourceGroupAlgebraCoeffMap

Coefficient-reduction map on a fixed finite Fox source quotient.

  • foxAlgebraicStagePowerSourceQuotientMap

Source quotient transition \(F/[N,N]N^m \to F/[N,N]N^n\) induced by \(n \mid m\).

  • foxAlgebraicStageSameSourceGroupAlgebraCoeffMap_of

Fixed-source coefficient reduction evaluated on a quotient basis element.

  • foxAlgebraicStagePowerSourceQuotientMap_mk

Evaluation of the source quotient transition on a representative.

Imports1
Imported by2

Declarations

def

foxAlgebraicStageSameSourceGroupAlgebraCoeffMap

L44 ↗
FoxDifferential.foxAlgebraicStageSameSourceGroupAlgebraCoeffMap
Documentation

Coefficient-reduction map on a fixed finite Fox source quotient.

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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
Lean source · statement
def foxAlgebraicStageSameSourceGroupAlgebraCoeffMap
    (N : Subgroup (FreeGroup X)) (k : ℕ) (hnm : n₀ ∣ m₀) :
    MonoidAlgebra (ModNCompletedCoeff m₀)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N k) →+*
      MonoidAlgebra (ModNCompletedCoeff n₀)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N k)
theorem

foxAlgebraicStageSameSourceGroupAlgebraCoeffMap_of

L57 ↗
FoxDifferential.foxAlgebraicStageSameSourceGroupAlgebraCoeffMap_of
Documentation

Fixed-source coefficient reduction evaluated on a quotient basis element.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageSameSourceGroupAlgebraCoeffMap_of
    (N : Subgroup (FreeGroup X)) (k : ℕ) (hnm : n₀ ∣ m₀)
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N k) :
    foxAlgebraicStageSameSourceGroupAlgebraCoeffMap (X := X) N k hnm
        (MonoidAlgebra.of (ModNCompletedCoeff m₀)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N k) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n₀)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N k) q
def

foxAlgebraicStagePowerSourceQuotientMap

L73 ↗
FoxDifferential.foxAlgebraicStagePowerSourceQuotientMap
Documentation

Source quotient transition \(F/[N,N]N^m \to F/[N,N]N^n\) induced by \(n \mid m\).

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
def foxAlgebraicStagePowerSourceQuotientMap
    (N : Subgroup (FreeGroup X)) (hnm : n₀ ∣ m₀) :
    FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N m₀ →*
      FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n₀
theorem

foxAlgebraicStagePowerSourceQuotientMap_mk

L83 ↗
FoxDifferential.foxAlgebraicStagePowerSourceQuotientMap_mk
Documentation

Evaluation of the source quotient transition on a representative.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStagePowerSourceQuotientMap_mk
    (N : Subgroup (FreeGroup X)) (hnm : n₀ ∣ m₀) (w : FreeGroup X) :
    foxAlgebraicStagePowerSourceQuotientMap (X := X) N hnm
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N m₀) w) =
      QuotientGroup.mk'
        (foxCommutatorPowerSubgroup (F := FreeGroup X) N n₀) w
def

foxAlgebraicStagePowerSourceGroupAlgebraMap

L96 ↗
FoxDifferential.foxAlgebraicStagePowerSourceGroupAlgebraMap
Documentation

Combined source transition on finite Fox source group algebras: quotient transition plus coefficient reduction.

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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
Lean source · statement
def foxAlgebraicStagePowerSourceGroupAlgebraMap
    (N : Subgroup (FreeGroup X)) (hnm : n₀ ∣ m₀) :
    MonoidAlgebra (ModNCompletedCoeff m₀)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N m₀) →+*
      MonoidAlgebra (ModNCompletedCoeff n₀)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n₀)
theorem

foxAlgebraicStagePowerSourceGroupAlgebraMap_of

L109 ↗
FoxDifferential.foxAlgebraicStagePowerSourceGroupAlgebraMap_of
Documentation

The finite Fox source group-algebra transition evaluated on a represented word.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStagePowerSourceGroupAlgebraMap_of
    (N : Subgroup (FreeGroup X)) (hnm : n₀ ∣ m₀) (w : FreeGroup X) :
    foxAlgebraicStagePowerSourceGroupAlgebraMap (X := X) N hnm
        (MonoidAlgebra.of (ModNCompletedCoeff m₀)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N m₀)
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := FreeGroup X) N m₀) w)) =
      MonoidAlgebra.of (ModNCompletedCoeff n₀)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n₀)
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N n₀) w)
theorem

foxAlgebraicStagePowerSourceGroupAlgebraMap_single_apply

L151 ↗
FoxDifferential.foxAlgebraicStagePowerSourceGroupAlgebraMap_single_apply
Documentation

On a single source-stage basis coefficient, the finite source transition sends the group coordinate by the quotient map and reduces the coefficient.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStagePowerSourceGroupAlgebraMap_single_apply
    (N : Subgroup (FreeGroup X)) (hnm : n₀ ∣ m₀)
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N m₀)
    (a : ModNCompletedCoeff m₀) :
    foxAlgebraicStagePowerSourceGroupAlgebraMap (X := X) N hnm
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        (foxAlgebraicStagePowerSourceQuotientMap (X := X) N hnm q)
        (modNCompletedCoeffMap (n := n₀) (m := m₀) hnm a)
theorem

foxAlgebraicStagePowerSourceGroupAlgebraMap_rfl

L201 ↗
FoxDifferential.foxAlgebraicStagePowerSourceGroupAlgebraMap_rfl
Documentation

The finite Fox source group-algebra transition is the identity map when the modulus is unchanged.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] in
Lean source · statement
theorem foxAlgebraicStagePowerSourceGroupAlgebraMap_rfl
    (N : Subgroup (FreeGroup X)) :
    foxAlgebraicStagePowerSourceGroupAlgebraMap (X := X) (n₀ := n₀) (m₀ := n₀) N
        dvd_rfl =
      RingHom.id _
theorem

foxAlgebraicStagePowerSourceGroupAlgebraMap_comp

L230 ↗
FoxDifferential.foxAlgebraicStagePowerSourceGroupAlgebraMap_comp
Documentation

Finite Fox source group-algebra transitions compose along divisibility.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStagePowerSourceGroupAlgebraMap_comp
    {k₀ : ℕ}
    (N : Subgroup (FreeGroup X)) (hnm : n₀ ∣ m₀) (hmk : m₀ ∣ k₀) :
    (foxAlgebraicStagePowerSourceGroupAlgebraMap (X := X) N hnm).comp
        (foxAlgebraicStagePowerSourceGroupAlgebraMap (X := X) N hmk) =
      foxAlgebraicStagePowerSourceGroupAlgebraMap (X := X) N (dvd_trans hnm hmk)
theorem

foxAlgebraicStageGroupAlgebraMap_powerSourceGroupAlgebraMap

L268 ↗
FoxDifferential.foxAlgebraicStageGroupAlgebraMap_powerSourceGroupAlgebraMap
Documentation

The natural finite-stage map \(((\mathbb{Z}/m\mathbb{Z})[F/[N,N]N^m]) \to ((\mathbb{Z}/m\mathbb{Z})[F/N])\) commutes with coefficient/source reduction to a divisor \(n \mid m\).

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageGroupAlgebraMap_powerSourceGroupAlgebraMap
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N m₀) :
    foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm
        (foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N m₀ x) =
      foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n₀
        (foxAlgebraicStagePowerSourceGroupAlgebraMap (X := X) N hnm x)

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