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

ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Surjective

3 Theorems | 1 Definition

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraMap_targetQuotient_lift A noncomputable lift of a completed target group-algebra coefficient to the source completed group algebra. The defining equation is \(\mathrm{primePowerCompletedGroupAlgebraMap\_targetQuotient\_lift\_spec}\). - foxAlgebraicStageTargetQuotientContinuousMonoidHom_surjective The quotient homomorphism \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective. This specialized form is used to lift coefficients from \(\mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) to \(\mathbb{Z}_{\ell}\llbracket F\rrbracket\) in the completed Fox derivative. - primePowerCompletedGroupAlgebraMap_targetQuotient_surjective The completed group-algebra map attached to \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective. This is the coefficient-lifting input for the surjectivity half of \(K/KI \to L\). - primePowerCompletedGroupAlgebraMap_targetQuotient_lift_spec The chosen coefficient lift maps back to the prescribed completed target coefficient.
import
Imported by

Declarations

Theorem FoxDifferential.foxAlgebraicStageTargetQuotientContinuousMonoidHom_surjective 
omit [DecidableEq X] in
theorem foxAlgebraicStageTargetQuotientContinuousMonoidHom_surjective
    [TopologicalSpace (FreeGroup X)] [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)] :
    Function.Surjective
      (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)

The quotient homomorphism \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective. This specialized form is used to lift coefficients from \(\mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) to \(\mathbb{Z}_{\ell}\llbracket F\rrbracket\) in the completed Fox derivative.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraMap_targetQuotient_surjective 
omit [DecidableEq X] in
theorem primePowerCompletedGroupAlgebraMap_targetQuotient_surjective
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)] :
    Function.Surjective
      (primePowerCompletedGroupAlgebraMap
        (ℓ := ℓ) (G := FreeGroup X)
        (H := foxAlgebraicStageTargetQuotient (X := X) N)
        (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N))

The completed group-algebra map attached to \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective. This is the coefficient-lifting input for the surjectivity half of \(K/KI \to L\).

Show Lean proof
Definition FoxDifferential.primePowerCompletedGroupAlgebraMap_targetQuotient_lift 
def primePowerCompletedGroupAlgebraMap_targetQuotient_lift
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
    (a : PrimePowerCompletedGroupAlgebra ℓ (foxAlgebraicStageTargetQuotient (X := X) N)) :
    PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X) :=
  Classical.choose
    (primePowerCompletedGroupAlgebraMap_targetQuotient_surjective
      (ℓ := ℓ) (X := X) N a)

A noncomputable lift of a completed target group-algebra coefficient to the source completed group algebra. The defining equation is \(\mathrm{primePowerCompletedGroupAlgebraMap\_targetQuotient\_lift\_spec}\).

Theorem FoxDifferential.primePowerCompletedGroupAlgebraMap_targetQuotient_lift_spec 
omit [DecidableEq X] in
@[simp]
theorem primePowerCompletedGroupAlgebraMap_targetQuotient_lift_spec
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
    (a : PrimePowerCompletedGroupAlgebra ℓ (foxAlgebraicStageTargetQuotient (X := X) N)) :
    primePowerCompletedGroupAlgebraMap
        (ℓ := ℓ) (G := FreeGroup X)
        (H := foxAlgebraicStageTargetQuotient (X := X) N)
        (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
        (primePowerCompletedGroupAlgebraMap_targetQuotient_lift
          (ℓ := ℓ) (X := X) N a) = a

The chosen coefficient lift maps back to the prescribed completed target coefficient.

Show Lean proof