ProCGroups.FoxDifferential.Completed.Continuous.Magnus.ClosedGeneratedVector

4 Theorems | 2 Definitions

This module bundles the completed Fox derivative vector as a scalar crossed homomorphism, first over pro-\(C\) integers and then over the presented coefficient ring. It also records the closed-generation and Magnus-reduction identities used by the completed Magnus injectivity argument.

imports

Imported by

Definition CrowellExactSequence.freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

def freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard
              (C := C) sourceData hbasis i)) : Subgroup
            (FoxDifferential.ZCCompletedFoxSemidirect
              C (ULift.{u} (Fin r)) H))) :
    FoxDifferential.ScalarCrossedHom
      (FoxDifferential.zcCompletedGroupAlgebraScalar C
        (FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated
          (C := C)
          (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard
              (C := C) sourceData hbasis i))
          htarget
          (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
            (C := C)
            (fun i : ULift.{u} (Fin r) =>
              psi (freeProCChosenULiftFamilyOfBasisCard
                (C := C) sourceData hbasis i)))))
      (FoxDifferential.ZCFreeFoxCoordinates
        C (X := ULift.{u} (Fin r)) (H := H)) :=
  let hfree :=
    freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
  let φ : ULift.{u} (Fin r) → H := fun i =>
    psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i)
  let hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
            (C := C) φ : Subgroup
              (FoxDifferential.ZCCompletedFoxSemidirect
                C (ULift.{u} (Fin r)) H)))
        (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
          (C := C) φ) :=
    FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
      (C := C) φ
  FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
    (C := C) hfree φ htarget hφconv

The closed-generated continuous Fox derivative vector attached to a finite chosen free pro-\(C\) basis and a presentation map.

Theorem CrowellExactSequence.freeProC_closedGeneratedTarget_mem_of_freeGroupFoxDerivativeVector_kernel

omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
theorem freeProC_closedGeneratedTarget_mem_of_freeGroupFoxDerivativeVector_kernel
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    {w : FreeGroup (ULift.{u} (Fin r))}
    (hw :
      FreeGroup.lift
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard
              (C := C) sourceData hbasis i)) w = 1) :
    ({ left :=
        FoxDifferential.zcFreeGroupFoxDerivativeVector C
          (FreeGroup.lift
            (fun i : ULift.{u} (Fin r) =>
              psi (freeProCChosenULiftFamilyOfBasisCard
                (C := C) sourceData hbasis i))) w,
       right := (1 : H) } :
      FoxDifferential.ZCCompletedFoxSemidirect C
        (ULift.{u} (Fin r)) H) ∈
      (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C)
        (fun i : ULift.{u} (Fin r) =>
          psi (freeProCChosenULiftFamilyOfBasisCard
            (C := C) sourceData hbasis i)) : Subgroup
          (FoxDifferential.ZCCompletedFoxSemidirect C
            (ULift.{u} (Fin r)) H))

An abstract kernel word for the chosen finite free basis gives a genuine cycle point in the closed-generated Fox graph target. This is the algebraic source of the completed cycle-lifting step: before passing to closures, every relation word \(w\) with target value \(1\) contributes \((D w, 1)\) to the closed-generated graph.

Show Lean proof

Theorem CrowellExactSequence.freeProCCompletedFoxRightHomViaClosedGeneratedProCInteger_eq

omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
theorem freeProCCompletedFoxRightHomViaClosedGeneratedProCInteger_eq
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard
              (C := C) sourceData hbasis i)) : Subgroup
            (FoxDifferential.ZCCompletedFoxSemidirect
              C (ULift.{u} (Fin r)) H))) :
    FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated
        (C := C)
        (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
        (fun i : ULift.{u} (Fin r) =>
          psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))
        htarget
        (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
          (C := C)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))) =
      psi.toMonoidHom

The right component of the closed-generated Fox graph attached to the chosen lifted finite basis is the original presentation map; the two continuous homomorphisms agree on every chosen free generator.

Show Lean proof

Definition CrowellExactSequence.freeProCCompletedFoxDerivativeVectorForPresentation

omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
def freeProCCompletedFoxDerivativeVectorForPresentation
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard
              (C := C) sourceData hbasis i)) : Subgroup
            (FoxDifferential.ZCCompletedFoxSemidirect
              C (ULift.{u} (Fin r)) H))) :
    FoxDifferential.ScalarCrossedHom
      (FoxDifferential.zcCompletedGroupAlgebraScalar
        C psi.toMonoidHom)
      (FoxDifferential.ZCFreeFoxCoordinates
        C (X := ULift.{u} (Fin r)) (H := H)) where
  toFun :=
    freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
      (H := H) (C := C) sourceData hbasis psi htarget
  map_mul' := by
    intro g h
    let X : Type u := ULift.{u} (Fin r)
    let ι : X → sourceData.carrier :=
      freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
    let hfree :=
      freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree
        (C := C) sourceData hbasis
    let φ : X → H := fun i => psi (ι i)
    let hφconv :
        ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
          (G :=
            (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
              (C := C) φ : Subgroup
                (FoxDifferential.ZCCompletedFoxSemidirect C X H)))
          (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
            (C := C) φ) :=
      FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
        (C := C) φ
    have hright :
        FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated
            (C := C) hfree φ htarget hφconv =
          psi.toMonoidHom := by
      simpa [X, ι, hfree, φ, hφconv] using
        freeProCCompletedFoxRightHomViaClosedGeneratedProCInteger_eq
          (H := H) (C := C) hForm sourceData hbasis psi hpsi htarget
    have hD :=
      (FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
        (C := C) hfree φ htarget hφconv).map_mul g h
    rw [← hright]
    exact hD

The closed-generated continuous Fox derivative vector, bundled with the original presentation map as its coefficient homomorphism.

Theorem CrowellExactSequence.continuous_freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
theorem continuous_freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard
              (C := C) sourceData hbasis i)) : Subgroup
            (FoxDifferential.ZCCompletedFoxSemidirect
              C (ULift.{u} (Fin r)) H))) :
    Continuous
      (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
        (H := H) (C := C) sourceData hbasis psi htarget)

The closed-generated continuous Fox derivative vector is continuous.

Show Lean proof

Theorem CrowellExactSequence.freeProC_zcUnivDiff_kernel_le_closedCommutator_of_closedGenFoxVector

omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
theorem freeProC_zcUnivDiff_kernel_le_closedCommutator_of_closedGenFoxVector
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard
              (C := C) sourceData hbasis i)) : Subgroup
            (FoxDifferential.ZCCompletedFoxSemidirect
              C (ULift.{u} (Fin r)) H)))
    (hDker :
      ∀ n : ProfiniteKernelSubgroup psi,
        freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
            (H := H) (C := C) sourceData hbasis psi htarget n.1 = 0 →
          n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
    ∀ n : ProfiniteKernelSubgroup psi,
      FoxDifferential.zcUniversalDifferential
          C psi.toMonoidHom n.1 = 0 →
        n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)

Universal completed Magnus-kernel reduction for the closed-generated continuous Fox vector. After this reduction, the remaining paper statement is exactly the concrete continuous Magnus kernel for the completed Fox derivative vector.

Show Lean proof

ProCGroups.FoxDifferential.Completed.Continuous.Magnus.ClosedGeneratedVector

Declarations