Module

Coefficient.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.OnGroup.Coefficient

2 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — derivative — on group — coefficient

The principal declarations in this module are:

foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom

The completed target coefficient homomorphism is associated to the quotient \(\mathrm{FreeGroup}(X) \to F/N\). It sends a word to the corresponding group-like element of the prime-power completed group algebra of the target quotient.

foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom_apply

The finite Fox-stage target coefficient homomorphism into the prime-power completed coefficients is evaluated by the corresponding finite-stage coefficient map.

Imports4

Imported by2

def

foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom

L49 ↗

FoxDifferential.foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom

Documentation

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 foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)] :
    FreeGroup X →*
      PrimePowerCompletedGroupAlgebra ℓ (foxAlgebraicStageTargetQuotient (X := X) N) where
  toFun w :=
    primePowerCompletedGroupAlgebraOf (ell := ℓ)
      (H := foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w)
  map_one' := by
    simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one, primePowerCompletedGroupAlgebraOf_one]
  map_mul' u v := by
    rw [← primePowerCompletedGroupAlgebraOf_mul (ell := ℓ)
      (H := foxAlgebraicStageTargetQuotient (X := X) N)]
    rfl

theorem

foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom_apply

L71 ↗

FoxDifferential.foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom_apply