Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Basic
ProCGroups/FoxDifferential/Completed/DifferentialModule/TargetQuotient/Basic

ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Basic

2 Theorems | 1 Definition

The principal declarations in this module are:

  • foxAlgebraicStageTargetQuotientContinuousMonoidHom The completed Fox-differential map is continuous with respect to the inverse-limit topology on the completed coefficient modules. - foxAlgebraicStageTargetQuotientContinuousMonoidHom_apply The finite-stage target quotient homomorphism sends a word to its quotient class modulo \(N\). - foxAlgebraicStagePrimePowerSourceCompletedIndex_le_targetQuotientComap The completed free derivative source finite stage \([N,N]N^{ell^a}\) refines every finite stage pulled back from the target quotient \(F/N\). This order comparison lets the completed group-algebra projection for \(\pi: \mathbb{Z}_{\ell}\llbracket F\rrbracket \to \mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) be computed from the completed free derivative source projection.
imports
Imported by

Declarations

Definition FoxDifferential.foxAlgebraicStageTargetQuotientContinuousMonoidHom 
def foxAlgebraicStageTargetQuotientContinuousMonoidHom
    [TopologicalSpace (FreeGroup X)] [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)] :
    ContinuousMonoidHom (FreeGroup X) (foxAlgebraicStageTargetQuotient (X := X) N) where
  toMonoidHom := QuotientGroup.mk' N
  continuous_toFun := continuous_of_discreteTopology

The completed Fox-differential map is continuous with respect to the inverse-limit topology on the completed coefficient modules.

Theorem FoxDifferential.foxAlgebraicStageTargetQuotientContinuousMonoidHom_apply 
omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageTargetQuotientContinuousMonoidHom_apply
    [TopologicalSpace (FreeGroup X)] [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    (w : FreeGroup X) :
    foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N w =
      QuotientGroup.mk' N w

The finite-stage target quotient homomorphism sends a word to its quotient class modulo \(N\).

Show Lean proof
Theorem FoxDifferential.foxAlgebraicStagePrimePowerSourceCompletedIndex_le_targetQuotientComap 
omit [DecidableEq X] [Fact (0 < ℓ)] in
theorem foxAlgebraicStagePrimePowerSourceCompletedIndex_le_targetQuotientComap
    [TopologicalSpace (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
    (hfinite : ∀ a : ℕ,
      Finite (FreeGroup X ⧸
        foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
    (j : PrimePowerCompletedGroupAlgebraIndex
      (foxAlgebraicStageTargetQuotient (X := X) N)) :
    completedGroupAlgebraComapIndex
        (G := FreeGroup X) (H := foxAlgebraicStageTargetQuotient (X := X) N)
        (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N) j.2 ≤
      foxAlgebraicStagePrimePowerSourceCompletedIndex
        (ℓ := ℓ) (X := X) N hfinite j.1

The completed free derivative source finite stage \([N,N]N^{ell^a}\) refines every finite stage pulled back from the target quotient \(F/N\). This order comparison lets the completed group-algebra projection for \(\pi: \mathbb{Z}_{\ell}\llbracket F\rrbracket \to \mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) be computed from the completed free derivative source projection.

Show Lean proof