NYLL
Module

Semidirect.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.CoeffMap.Semidirect
4 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

  • foxAlgebraicStageSemidirectCoeffMap

Coefficient-reduction map on finite-stage semidirect Fox targets.

  • foxAlgebraicStageSemidirectCoeffMap_lift

The finite-stage semidirect coefficient map carries the lift at modulus \(m\) to the lift at modulus \(n\).

  • foxAlgebraicStageDerivative_coeffMap

Finite-stage Fox derivative coordinates commute with coefficient reduction.

  • foxAlgebraicStageGroupAlgebraDerivative_powerCoeff_natural

Finite-stage group-algebra derivative coordinates commute with source transition and coefficient reduction.

Imports1
Imported by2

Declarations

def

foxAlgebraicStageSemidirectCoeffMap

L47 ↗
FoxDifferential.foxAlgebraicStageSemidirectCoeffMap
Documentation

Coefficient-reduction map on finite-stage semidirect Fox targets.

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 · full declaration
def foxAlgebraicStageSemidirectCoeffMap
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) :
    FoxAlgebraicStageSemidirect (X := X) N m₀ →*
      FoxAlgebraicStageSemidirect (X := X) N n₀ where
  toFun a :=
    { left := fun i => foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm (a.left i)
      right := a.right }
  map_one' := by
    apply FoxAlgebraicStageSemidirect.ext
    · funext i
      simp only [FoxAlgebraicStageSemidirect.one_left, Pi.zero_apply, map_zero]
    · rfl
  map_mul' a b := by
    apply FoxAlgebraicStageSemidirect.ext
    · funext i
      have hright :
          foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm
              (MonoidAlgebra.single a.right (1 : ModNCompletedCoeff m₀)) =
            MonoidAlgebra.single a.right (1 : ModNCompletedCoeff n₀) := by
        simpa only [map_one] using
          foxAlgebraicStageTargetGroupAlgebraCoeffMap_single_apply
            (X := X) N hnm a.right (1 : ModNCompletedCoeff m₀)
      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]
theorem

foxAlgebraicStageSemidirectCoeffMap_lift

L79 ↗
FoxDifferential.foxAlgebraicStageSemidirectCoeffMap_lift
Documentation

The finite-stage semidirect coefficient map carries the lift at modulus \(m\) to the lift at modulus \(n\).

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
theorem foxAlgebraicStageSemidirectCoeffMap_lift
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) (w : FreeGroup X) :
    foxAlgebraicStageSemidirectCoeffMap (X := X) N hnm
        (foxAlgebraicStageLift (X := X) N m₀ w) =
      foxAlgebraicStageLift (X := X) N n₀ w
theorem

foxAlgebraicStageDerivative_coeffMap

L106 ↗
FoxDifferential.foxAlgebraicStageDerivative_coeffMap
Documentation

Finite-stage Fox derivative coordinates commute with coefficient reduction.

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
theorem foxAlgebraicStageDerivative_coeffMap
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (i : X) (w : FreeGroup X) :
    foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm
        (foxAlgebraicStageDerivative (X := X) N m₀ i w) =
      foxAlgebraicStageDerivative (X := X) N n₀ i w
theorem

foxAlgebraicStageGroupAlgebraDerivative_powerCoeff_natural

L123 ↗
FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_powerCoeff_natural
Documentation

Finite-stage group-algebra derivative coordinates commute with source transition and coefficient reduction.

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
theorem foxAlgebraicStageGroupAlgebraDerivative_powerCoeff_natural
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) (i : X)
    (x : MonoidAlgebra (ModNCompletedCoeff m₀)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N m₀)) :
    foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm
        (foxAlgebraicStageGroupAlgebraDerivative (X := X) N m₀ i x) =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N n₀ i
        (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.