NYLL
Module

Naturality.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Naturality
18 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — stage — naturality

The principal declarations in this module are:

  • foxAlgebraicStageTargetQuotientMap

Natural quotient map \(F/N \to F/M\) induced by an inclusion \(N \le M\).

  • foxAlgebraicStageTargetGroupAlgebraMap

Group-algebra map on finite-stage targets induced by \(N \le M\).

  • foxCommutatorPowerRelatorSet_mono

Commutator-power relators are monotone in the normal subgroup.

  • foxCommutatorPowerSubgroup_mono

The finite Fox commutator-power subgroup is monotone in the normal subgroup.

Imports1
Imported by2

Declarations

theorem

foxCommutatorPowerRelatorSet_mono

L43 ↗
FoxDifferential.foxCommutatorPowerRelatorSet_mono
Documentation

Commutator-power relators are monotone in the normal 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 (ℓ : ℕ) [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 foxCommutatorPowerRelatorSet_mono
    {N M : Subgroup (FreeGroup X)} {n : ℕ} (hNM : N ≤ M) :
    foxCommutatorPowerRelatorSet (F := FreeGroup X) N n ⊆
      foxCommutatorPowerRelatorSet (F := FreeGroup X) M n
theorem

foxCommutatorPowerSubgroup_mono

L54 ↗
FoxDifferential.foxCommutatorPowerSubgroup_mono
Documentation

The finite Fox commutator-power subgroup is monotone in the normal 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 (ℓ : ℕ) [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 foxCommutatorPowerSubgroup_mono
    {N M : Subgroup (FreeGroup X)} (hNM : N ≤ M) (n : ℕ) :
    foxCommutatorPowerSubgroup (F := FreeGroup X) N n ≤
      foxCommutatorPowerSubgroup (F := FreeGroup X) M n
theorem

foxCommutatorPowerRelatorSet_dvd

L64 ↗
FoxDifferential.foxCommutatorPowerRelatorSet_dvd
Documentation

Commutator-power relators are contravariantly monotone under divisibility of exponents.

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 foxCommutatorPowerRelatorSet_dvd
    {N : Subgroup (FreeGroup X)} {n m : ℕ} (hnm : n ∣ m) :
    foxCommutatorPowerRelatorSet (F := FreeGroup X) N m ⊆
      foxCommutatorPowerRelatorSet (F := FreeGroup X) N n
theorem

foxCommutatorPowerSubgroup_dvd

L79 ↗
FoxDifferential.foxCommutatorPowerSubgroup_dvd
Documentation

The finite Fox commutator-power subgroup is contravariantly monotone under divisibility of exponents.

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 foxCommutatorPowerSubgroup_dvd
    (N : Subgroup (FreeGroup X)) {n m : ℕ} (hnm : n ∣ m) :
    foxCommutatorPowerSubgroup (F := FreeGroup X) N m ≤
      foxCommutatorPowerSubgroup (F := FreeGroup X) N n
def

foxAlgebraicStageTargetQuotientMap

L88 ↗
FoxDifferential.foxAlgebraicStageTargetQuotientMap
Documentation

Natural quotient map \(F/N \to F/M\) induced by an inclusion \(N \le M\).

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 foxAlgebraicStageTargetQuotientMap
    {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal] (hNM : N ≤ M) :
    foxAlgebraicStageTargetQuotient (X := X) N →*
      foxAlgebraicStageTargetQuotient (X := X) M
theorem

foxAlgebraicStageTargetQuotientMap_mk

L97 ↗
FoxDifferential.foxAlgebraicStageTargetQuotientMap_mk
Documentation

Evaluation of the finite-stage target quotient map on a representative.

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 foxAlgebraicStageTargetQuotientMap_mk
    {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
    (hNM : N ≤ M) (w : FreeGroup X) :
    foxAlgebraicStageTargetQuotientMap (X := X) hNM (QuotientGroup.mk' N w) =
      QuotientGroup.mk' M w
def

foxAlgebraicStageTargetGroupAlgebraMap

L105 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraMap
Documentation

Group-algebra map on finite-stage targets induced by \(N \le M\).

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 foxAlgebraicStageTargetGroupAlgebraMap
    {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal] (hNM : N ≤ M) (n : ℕ) :
    foxAlgebraicStageTargetGroupAlgebra (X := X) N n →+*
      foxAlgebraicStageTargetGroupAlgebra (X := X) M n
theorem

foxAlgebraicStageTargetGroupAlgebraMap_of

L115 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraMap_of
Documentation

Evaluation of the finite-stage target group-algebra map on a represented word.

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 foxAlgebraicStageTargetGroupAlgebraMap_of
    {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
    (hNM : N ≤ M) (n : ℕ) (w : FreeGroup X) :
    foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w)) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) M) (QuotientGroup.mk' M w)
theorem

foxAlgebraicStageTargetGroupAlgebraMap_of_quotient

L133 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraMap_of_quotient
Documentation

Evaluation of the finite-stage target group-algebra map on a quotient basis element.

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 foxAlgebraicStageTargetGroupAlgebraMap_of_quotient
    {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
    (hNM : N ≤ M) (n : ℕ) (q : foxAlgebraicStageTargetQuotient (X := X) N) :
    foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) M)
        (foxAlgebraicStageTargetQuotientMap (X := X) hNM q)
def

foxAlgebraicStageSourceQuotientMap

L146 ↗
FoxDifferential.foxAlgebraicStageSourceQuotientMap
Documentation

The natural quotient map between finite-stage source quotients is induced by \(N \le M\).

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 foxAlgebraicStageSourceQuotientMap
    {N M : Subgroup (FreeGroup X)} (hNM : N ≤ M) (n : ℕ) :
    FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n →*
      FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) M n
theorem

foxAlgebraicStageSourceQuotientMap_mk

L156 ↗
FoxDifferential.foxAlgebraicStageSourceQuotientMap_mk
Documentation

Evaluation of the finite-stage source quotient map on a representative.

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 foxAlgebraicStageSourceQuotientMap_mk
    {N M : Subgroup (FreeGroup X)}
    (hNM : N ≤ M) (n : ℕ) (w : FreeGroup X) :
    foxAlgebraicStageSourceQuotientMap (X := X) hNM n
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N n) w) =
      QuotientGroup.mk'
        (foxCommutatorPowerSubgroup (F := FreeGroup X) M n) w
def

foxAlgebraicStageSourceGroupAlgebraMap

L167 ↗
FoxDifferential.foxAlgebraicStageSourceGroupAlgebraMap
Documentation

Group-algebra map on finite-stage source quotients induced by \(N \le M\).

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 foxAlgebraicStageSourceGroupAlgebraMap
    {N M : Subgroup (FreeGroup X)} (hNM : N ≤ M) (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) →+*
      MonoidAlgebra (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) M n)
theorem

foxAlgebraicStageSourceGroupAlgebraMap_of

L179 ↗
FoxDifferential.foxAlgebraicStageSourceGroupAlgebraMap_of
Documentation

Evaluation of the finite-stage source group-algebra map on a represented word.

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 foxAlgebraicStageSourceGroupAlgebraMap_of
    {N M : Subgroup (FreeGroup X)}
    (hNM : N ≤ M) (n : ℕ) (w : FreeGroup X) :
    foxAlgebraicStageSourceGroupAlgebraMap (X := X) hNM n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := FreeGroup X) N n) w)) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) M n)
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) M n) w)
theorem

foxAlgebraicStageSourceGroupAlgebraMap_of_quotient

L205 ↗
FoxDifferential.foxAlgebraicStageSourceGroupAlgebraMap_of_quotient
Documentation

Evaluation of the finite-stage source group-algebra map on a quotient basis element.

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 foxAlgebraicStageSourceGroupAlgebraMap_of_quotient
    {N M : Subgroup (FreeGroup X)}
    (hNM : N ≤ M) (n : ℕ)
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSourceGroupAlgebraMap (X := X) hNM n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) M n)
        (foxAlgebraicStageSourceQuotientMap (X := X) hNM n q)
def

foxAlgebraicStageSemidirectMap

L220 ↗
FoxDifferential.foxAlgebraicStageSemidirectMap
Documentation

Semidirect target map induced by functoriality in the normal subgroup.

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 · full declaration
def foxAlgebraicStageSemidirectMap
    {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal] (hNM : N ≤ M) (n : ℕ) :
    FoxAlgebraicStageSemidirect (X := X) N n →*
      FoxAlgebraicStageSemidirect (X := X) M n where
  toFun a :=
    { left := fun i => foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n (a.left i)
      right := foxAlgebraicStageTargetQuotientMap (X := X) hNM a.right }
  map_one' := by
    apply FoxAlgebraicStageSemidirect.ext
    · funext i
      simp only [FoxAlgebraicStageSemidirect.one_left, Pi.zero_apply, map_zero]
    · simp only [FoxAlgebraicStageSemidirect.one_right, map_one]
  map_mul' a b := by
    apply FoxAlgebraicStageSemidirect.ext
    · funext i
      have hright :
          foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n
              (MonoidAlgebra.single a.right (1 : ModNCompletedCoeff n)) =
            MonoidAlgebra.single
              (foxAlgebraicStageTargetQuotientMap (X := X) hNM a.right) 1 := by
        change
          MonoidAlgebra.mapDomain
              (foxAlgebraicStageTargetQuotientMap (X := X) hNM)
              (MonoidAlgebra.single a.right 1) =
            MonoidAlgebra.single
              (foxAlgebraicStageTargetQuotientMap (X := X) hNM a.right) 1
        exact MonoidAlgebra.mapDomain_single
      simp only [FoxAlgebraicStageSemidirect.mul_left, MonoidAlgebra.of_apply, Pi.add_apply,
          Pi.smul_apply,
  smul_eq_mul, map_add, map_mul, hright]
    · simp only [FoxAlgebraicStageSemidirect.mul_right, map_mul]
theorem

foxAlgebraicStageSemidirectMap_lift

L253 ↗
FoxDifferential.foxAlgebraicStageSemidirectMap_lift
Documentation

The finite-stage semidirect map carries the lift for \(N\) to the lift for \(M\).

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
theorem foxAlgebraicStageSemidirectMap_lift
    {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
    (hNM : N ≤ M) (n : ℕ) (w : FreeGroup X) :
    foxAlgebraicStageSemidirectMap (X := X) hNM n
        (foxAlgebraicStageLift (X := X) N n w) =
      foxAlgebraicStageLift (X := X) M n w
theorem

foxAlgebraicStageDerivative_natural

L280 ↗
FoxDifferential.foxAlgebraicStageDerivative_natural
Documentation

Naturality of finite-stage Fox derivative coordinates under \(N \le M\).

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
theorem foxAlgebraicStageDerivative_natural
    {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
    (hNM : N ≤ M) (n : ℕ) (i : X) (w : FreeGroup X) :
    foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n
        (foxAlgebraicStageDerivative (X := X) N n i w) =
      foxAlgebraicStageDerivative (X := X) M n i w
theorem

foxAlgebraicStageGroupAlgebraDerivative_natural

L293 ↗
FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_natural
Documentation

Naturality of finite-stage group-algebra derivative coordinates under \(N \le M\).

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
theorem foxAlgebraicStageGroupAlgebraDerivative_natural
    {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
    (hNM : N ≤ M) (n : ℕ) (i : X)
    (x : MonoidAlgebra (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)) :
    foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n
        (foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i x) =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) M n i
        (foxAlgebraicStageSourceGroupAlgebraMap (X := X) hNM n x)

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