ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift

57 Theorems | 22 Definitions

The principal declarations in this module are:

freeProCZCCompletedFoxSemidirectGenerator The generator map into the completed Fox semidirect target attached to a basis-value map \(\varphi: X \to H\). - freeProCZCCompletedFoxSemidirectClosedGeneratedTarget The closed subgroup of the completed Fox semidirect target generated by the Fox graph generators. - freeProCZCCompletedFoxSemidirectGenerator_left The generator map has the expected left coordinate. - freeProCZCCompletedFoxSemidirectGenerator_right The generator map has the expected right coordinate.

imports

Imported by

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator

def freeProCZCCompletedFoxSemidirectGenerator (φ : X → H) :
    X → ZCCompletedFoxSemidirect C X H :=
  fun x =>
    { left := Pi.single x (1 : ZCCompletedGroupAlgebra C H)
      right := φ x }

The generator map into the completed Fox semidirect target attached to a basis-value map \(\varphi: X \to H\).

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator_left

omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectGenerator_left
    (φ : X → H) (x : X) :
    (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x).left =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)

The generator map has the expected left coordinate.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator_right

omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectGenerator_right
    (φ : X → H) (x : X) :
    (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x).right = φ x

The generator map has the expected right coordinate.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator_convergesToOneAlongOpenSubgroups_of_finite

omit [TopologicalSpace X]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCCompletedFoxSemidirectGenerator_convergesToOneAlongOpenSubgroups_of_finite
    [Finite X] (φ : X → H) :
    FamilyConvergesToOneAlongOpenSubgroups
      (G := ZCCompletedFoxSemidirect C X H)
      (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)

For a finite generator set, the completed Fox semidirect generator map automatically converges to \(1\).

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (φ : X → H) :
    ClosedSubgroup (ZCCompletedFoxSemidirect C X H) :=
  ProCGroups.Generation.closedSubgroupGenerated
    (G := ZCCompletedFoxSemidirect C X H)
    (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))

The closed subgroup of the completed Fox semidirect target generated by the Fox graph generators.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_hasOpenNormalBasisInClass

omit [TopologicalSpace X] in
theorem freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_hasOpenNormalBasisInClass
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (hAmbient :
      ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H) :
    ProCGroups.ProC.HasOpenNormalBasisInClass C
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))

If the ambient completed Fox semidirect target has an open-normal \(C\)-basis, then so does the closed target generated by the Fox graph generators, by closed-subgroup permanence.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (φ : X → H) :
    X →
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) :=
  ProCGroups.Generation.closedSubgroupGeneratedMap
    (G := ZCCompletedFoxSemidirect C X H)
    (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)

The Fox graph generator map, with codomain restricted to the closed subgroup it generates.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_val

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_val
    (φ : X → H) (x : X) :
    (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ x :
      ZCCompletedFoxSemidirect C X H) =
      freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x

The closed-generated Fox semidirect generator has underlying value equal to the corresponding semidirect generator.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator_mem_closedGeneratedTarget

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectGenerator_mem_closedGeneratedTarget
    (φ : X → H) (x : X) :
    freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))

Each Fox graph generator belongs to the closed subgroup generated by the Fox graph.

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectLift_freeGroupLift_mem_closedGeneratedTarget

omit [TopologicalSpace X] in
theorem zcCompletedFoxSemidirectLift_freeGroupLift_mem_closedGeneratedTarget
    (φ : X → H) (w : FreeGroup X) :
    zcCompletedFoxSemidirectLift C (FreeGroup.lift φ) w ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))

The completed semidirect Fox graph of every abstract free-group word lies in the closed subgroup generated by the Fox graph generators.

Show Lean proof

Theorem FoxDifferential.freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec

omit [TopologicalSpace X] in
theorem freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec
    (φ : X → H) (w : FreeGroup X) :
    ({ left :=
        zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w,
       right := FreeGroup.lift φ w } :
      ZCCompletedFoxSemidirect C X H) ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))

Equivalently, the pair consisting of the completed free Fox derivative vector and the target word value belongs to the closed generated Fox graph.

Show Lean proof

Theorem FoxDifferential.freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel

omit [TopologicalSpace X] in
theorem freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel
    (φ : X → H) {w : FreeGroup X} (hw : FreeGroup.lift φ w = 1) :
    ({ left :=
        zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w,
       right := (1 : H) } :
      ZCCompletedFoxSemidirect C X H) ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))

If an abstract free-group word maps trivially to the target group, its completed Fox derivative vector gives a genuine cycle point \((D w, 1)\) in the closed generated Fox graph.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectKernelCycleSet

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectKernelCycleSet (φ : X → H) :
    Set (ZCCompletedFoxSemidirect C X H) :=
  { y | ∃ w : FreeGroup X, FreeGroup.lift φ w = 1 ∧
      y =
        ({ left :=
            zcFreeGroupFoxDerivativeVector C
              (FreeGroup.lift φ) w,
           right := (1 : H) } :
          ZCCompletedFoxSemidirect C X H) }

The algebraic kernel-word cycle points in the completed Fox semidirect product. These are the points \((D w, 1)\) obtained from abstract free-group words whose target value is 1. The remaining density step for the completed Fox cycles is formulated using the closure of this set.

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectBoundaryCycleSet

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectBoundaryCycleSet [Fintype X] (φ : X → H) :
    Set (ZCCompletedFoxSemidirect C X H) :=
  { y | y.right = 1 ∧
      zcFreeGroupFoxBoundary C (FreeGroup.lift φ) y.left = 0 }

The completed Fox boundary-cycle set inside the completed Fox semidirect product. Its points are exactly the pairs \((v,1)\) whose coordinate vector is killed by the source-shaped completed Fox boundary. The remaining density step can be expressed as saying that this boundary-cycle set is contained in the closure of the algebraic kernel-word cycle set.

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordPoint

omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
def freeProCZCCompletedFoxSemidirectGraphWordPoint (φ : X → H) (w : FreeGroup X) :
    ZCCompletedFoxSemidirect C X H :=
  { left :=
      zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w,
    right := FreeGroup.lift φ w }

The genuine completed Fox graph point \((D w, \varphi(w))\) attached to an abstract free-group word.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordPoint_left

omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_left
    (φ : X → H) (w : FreeGroup X) :
    (freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w).left =
      zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w

The left component of a semidirect graph-word point is the completed free-group Fox derivative vector of the word.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordPoint_right

omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_right
    (φ : X → H) (w : FreeGroup X) :
    (freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w).right =
      FreeGroup.lift φ w

The right component of a semidirect graph-word point is \(\mathrm{FreeGroup.lift}(\varphi)(w)\).

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordSet

omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
def freeProCZCCompletedFoxSemidirectGraphWordSet (φ : X → H) :
    Set (ZCCompletedFoxSemidirect C X H) :=
  { y | ∃ w : FreeGroup X,
      y = freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w }

The set of all completed Fox graph points attached to abstract free-group words.

Theorem FoxDifferential.mem_freeProCZCCompletedFoxSemidirectGraphWordSet_iff

omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem mem_freeProCZCCompletedFoxSemidirectGraphWordSet_iff
    {φ : X → H}
    {y : ZCCompletedFoxSemidirect C X H} :
    y ∈ freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ ↔
      ∃ w : FreeGroup X,
        y = freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w

Membership in the completed Fox semidirect graph word set is equivalent to the displayed coordinate condition.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordPoint_mem_closedGeneratedTarget

omit [TopologicalSpace X] in
theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_mem_closedGeneratedTarget
    (φ : X → H) (w : FreeGroup X) :
    freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))

Every completed graph-word point lies in the closed subgroup generated by the Fox graph generators.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordSet_subset_closedGeneratedTarget

omit [TopologicalSpace X] in
theorem freeProCZCCompletedFoxSemidirectGraphWordSet_subset_closedGeneratedTarget
    (φ : X → H) :
    freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

The graph-word set lies in the closed subgroup generated by the Fox graph generators.

Show Lean proof

Theorem FoxDifferential.closure_freeProCZCFoxSemiGraphWordSet_subset_closedGenTarget

omit [TopologicalSpace X] in
theorem closure_freeProCZCFoxSemiGraphWordSet_subset_closedGenTarget
    (φ : X → H) :
    closure (freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ) ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

The closure of the graph-word set remains in the closed generated Fox graph target.

Show Lean proof

Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density

omit [TopologicalSpace X] in
theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density
    [Fintype X] (φ : X → H)
    (hdensity :
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
        closure (freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ)) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

Graph-word density places every completed boundary cycle in the closed generated Fox graph target.

Show Lean proof

Theorem FoxDifferential.zcFreeGroupFoxBoundary_zcFreeGroupFoxDerivativeVector_of_kernel

omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
    [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem zcFreeGroupFoxBoundary_zcFreeGroupFoxDerivativeVector_of_kernel
    [Fintype X] (φ : X → H) {w : FreeGroup X}
    (hw : FreeGroup.lift φ w = 1) :
    zcFreeGroupFoxBoundary C (FreeGroup.lift φ)
        (zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w) = 0

A kernel word has zero completed Fox boundary. This is the completed Fox fundamental formula applied before taking closures: if \(w\) maps to \(1\), then the Euler boundary of its Fox derivative vector is zero.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet

omit [TopologicalSpace X] in
omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet
    [Fintype X] (φ : X → H) :
    freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ ⊆
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ

Every algebraic kernel-word cycle point is an actual completed Fox boundary cycle.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup
    [Fintype X] (φ : X → H) :
    Subgroup (ZCCompletedFoxSemidirect C X H) where
  carrier := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ
  one_mem' := by
    constructor
    · rfl
    · simp only [ZCCompletedFoxSemidirect.one_left, map_zero]
  mul_mem' := by
    intro a b ha hb
    rcases ha with ⟨ha_right, ha_boundary⟩
    rcases hb with ⟨hb_right, hb_boundary⟩
    constructor
    · simp only [ZCCompletedFoxSemidirect.mul_right, ha_right, hb_right, mul_one]
    · calc
        zcFreeGroupFoxBoundary C (FreeGroup.lift φ) (a * b).left
            = zcFreeGroupFoxBoundary C (FreeGroup.lift φ)
                (a.left + b.left) := by
                simp only [ZCCompletedFoxSemidirect.mul_left, ha_right, map_one, one_smul, map_add]
        _ = zcFreeGroupFoxBoundary C (FreeGroup.lift φ) a.left +
              zcFreeGroupFoxBoundary C (FreeGroup.lift φ) b.left := by
                rw [map_add]
        _ = 0 := by
                simp only [ha_boundary, hb_boundary, add_zero]
  inv_mem' := by
    intro a ha
    rcases ha with ⟨ha_right, ha_boundary⟩
    constructor
    · simp only [ZCCompletedFoxSemidirect.inv_right, ha_right, inv_one]
    · calc
        zcFreeGroupFoxBoundary C (FreeGroup.lift φ) a⁻¹.left
            = zcFreeGroupFoxBoundary C (FreeGroup.lift φ) (-a.left) := by
                simp only [ZCCompletedFoxSemidirect.inv_left, ha_right, inv_one, map_one,
                    one_smul, map_neg]
        _ = -zcFreeGroupFoxBoundary C (FreeGroup.lift φ) a.left := by
                rw [map_neg]
        _ = 0 := by
                simp only [ha_boundary, neg_zero]

The boundary-cycle points form an actual subgroup of the completed Fox semidirect product. Algebraically this is the additive kernel of the source-shaped completed Fox boundary, embedded as the right-trivial subgroup \((v,1)\).

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup_coe

omit [TopologicalSpace X] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
    [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup_coe
    [Fintype X] (φ : X → H) :
    ((freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup
      (C := C) φ : Subgroup
        (ZCCompletedFoxSemidirect C X H)) : Set
        (ZCCompletedFoxSemidirect C X H)) =
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ

The \(\mathbb{Z}_C\)-completed differential-module boundary is the finite-stage boundary obtained from the source and target coordinates.

Show Lean proof

Theorem FoxDifferential.isClosed_freeProCZCCompletedFoxSemidirectBoundaryCycleSet_of_continuous

omit [TopologicalSpace X] [DecidableEq X] [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem isClosed_freeProCZCCompletedFoxSemidirectBoundaryCycleSet_of_continuous
    [Fintype X] [T1Space H]
    [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
    [T1Space (ZCCompletedGroupAlgebra C H)]
    (φ : X → H)
    (hleft :
      Continuous
        (fun y : ZCCompletedFoxSemidirect C X H => y.left))
    (hright :
      Continuous
        (fun y : ZCCompletedFoxSemidirect C X H => y.right))
    (hboundary :
      Continuous
        (zcFreeGroupFoxBoundary C (FreeGroup.lift φ))) :
    IsClosed (freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ)

The completed Fox boundary-cycle set is closed whenever the two semidirect projections and the source-shaped completed Fox boundary are continuous. This is the topological half of the density frontier: algebraic kernel-word cycles stay inside actual boundary cycles after taking closure.

Show Lean proof

Theorem FoxDifferential.closure_freeProCZCFoxSemiKernelCycleSet_subset_boundaryCycleSet_of_continuous

omit [TopologicalSpace X] in
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem closure_freeProCZCFoxSemiKernelCycleSet_subset_boundaryCycleSet_of_continuous
    [Fintype X] [T1Space H]
    [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
    [T1Space (ZCCompletedGroupAlgebra C H)]
    (φ : X → H)
    (hleft :
      Continuous
        (fun y : ZCCompletedFoxSemidirect C X H => y.left))
    (hright :
      Continuous
        (fun y : ZCCompletedFoxSemidirect C X H => y.right))
    (hboundary :
      Continuous
        (zcFreeGroupFoxBoundary C (FreeGroup.lift φ))) :
    closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) ⊆
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ

Closure of algebraic kernel-word cycle points remains inside the actual completed Fox boundary-cycle set, assuming the displayed boundary-cycle set is topologically closed.

Show Lean proof

Theorem FoxDifferential.closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_iff_density

omit [TopologicalSpace X] in
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_iff_density
    [Fintype X] [T1Space H]
    [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
    [T1Space (ZCCompletedGroupAlgebra C H)]
    {φ : X → H}
    (hleft :
      Continuous
        (fun y : ZCCompletedFoxSemidirect C X H => y.left))
    (hright :
      Continuous
        (fun y : ZCCompletedFoxSemidirect C X H => y.right))
    (hboundary :
      Continuous
        (zcFreeGroupFoxBoundary C (FreeGroup.lift φ))) :
    closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) =
        freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ↔
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
        closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)

With the continuity inputs in place, the remaining density statement is equivalently the claim that the closure of algebraic kernel-word cycle points is exactly the boundary-cycle set.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_closedGeneratedTarget

omit [TopologicalSpace X] in
theorem freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_closedGeneratedTarget
    (φ : X → H) :
    freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

Every algebraic kernel-word cycle point lies in the closed generated Fox graph target.

Show Lean proof

Theorem FoxDifferential.closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget

omit [TopologicalSpace X] in
theorem closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget
    (φ : X → H) :
    closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

The closure of algebraic kernel-word cycle points is still contained in the closed generated Fox graph target.

Show Lean proof

Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density

omit [TopologicalSpace X] in
theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
    [Fintype X] (φ : X → H)
    (hdensity :
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
        closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

If the boundary-cycle set is dense in the algebraic kernel-word closure, then every completed Fox boundary cycle belongs to the closed subgroup generated by the Fox graph.

Show Lean proof

Theorem FoxDifferential.freeProCZCFoxClosedGenTarget_mem_of_mem_closure_kernelCycleSet

omit [TopologicalSpace X] in
theorem freeProCZCFoxClosedGenTarget_mem_of_mem_closure_kernelCycleSet
    (φ : X → H)
    {y : ZCCompletedFoxSemidirect C X H}
    (hy :
      y ∈ closure
        (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)) :
    y ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))

Pointwise form of the closure step for algebraic kernel-word cycle points.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates

omit [TopologicalSpace X] in
theorem freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates
    (φ : X → H) :
    ProCGroups.Generation.TopologicallyGenerates
      (G :=
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
      (Set.range
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))

The restricted Fox graph generators topologically generate their closed generated target.

Show Lean proof

Theorem FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite

omit [TopologicalSpace X] in
theorem freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
    [Finite X] (φ : X → H) :
    FamilyConvergesToOneAlongOpenSubgroups
      (G :=
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
      (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)

For a finite generator set, the restricted Fox graph generators converge to \(1\).

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectLiftToClosedGenerated

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    F →*
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) := by
  letI : CompactSpace
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
        (ZCCompletedFoxSemidirect C X H)) := by
    exact
      (show IsClosed
          (((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
            (C := C) φ : Subgroup (ZCCompletedFoxSemidirect C X H)) :
              Set (ZCCompletedFoxSemidirect C X H))) from
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C) φ).isClosed').isClosedEmbedding_subtypeVal.compactSpace
  exact hι.lift htarget
    (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)
    hφconv
    (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates (C := C) φ)

The completed Fox semidirect lift into the closed target generated by the graph generators. This is the converging-set version needed when the graph generators do not generate the whole semidirect product.

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    F →ₜ*
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) := by
  letI : CompactSpace
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
        (ZCCompletedFoxSemidirect C X H)) := by
    exact
      (show IsClosed
          (((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
            (C := C) φ : Subgroup (ZCCompletedFoxSemidirect C X H)) :
              Set (ZCCompletedFoxSemidirect C X H))) from
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C) φ).isClosed').isClosedEmbedding_subtypeVal.compactSpace
  exact hι.liftHom htarget
    (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)
    hφconv
    (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates (C := C) φ)

Continuous homomorphism form of the closed-generated semidirect lift.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_toMonoidHom

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_toMonoidHom
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    (freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
        (C := C) hι φ htarget hφconv).toMonoidHom =
      freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
        (C := C) hι φ htarget hφconv

Forgetting continuity from the closed-generated semidirect lift homomorphism recovers the underlying closed-generated semidirect lift.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator

omit [TopologicalSpace X] in
@[simp 900]
theorem freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
    (x : X) :
    freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
        (C := C) hι φ htarget hφconv (ι x) =
      freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ x

The closed-generated semidirect lift sends each free pro-\(C\) generator to the corresponding closed-generated Fox semidirect generator.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_surjective

omit [TopologicalSpace X] in
theorem freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_surjective
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    [T2Space
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))]
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    Function.Surjective
      (freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
        (C := C) hι φ htarget hφconv)

The closed-generated semidirect lift is surjective onto the closed target generated by the Fox graph generators. This is the mathematically valid replacement for the generally false claim that the Fox graph generators fill the whole completed semidirect product: the universal map from the free pro-\(C\) group is onto exactly the closed subgroup generated by those graph generators.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    F →* ZCCompletedFoxSemidirect C X H :=
  (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
        (ZCCompletedFoxSemidirect C X H)).subtype.comp
    (freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
      (C := C) hι φ htarget hφconv)

The lift through the closed generated subgroup, composed with the inclusion into the full completed Fox semidirect product.

Theorem FoxDifferential.freeProCZCFoxSemiLiftViaClosedGen_exists_preimage_of_mem_closedGenTarget

omit [TopologicalSpace X] in
theorem freeProCZCFoxSemiLiftViaClosedGen_exists_preimage_of_mem_closedGenTarget
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    [T2Space
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))]
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
    {y : ZCCompletedFoxSemidirect C X H}
    (hy : y ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))) :
    ∃ g : F,
      freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
        (C := C) hι φ htarget hφconv g = y

Elementwise form of the semidirect lift theorem, formulated in the ambient completed Fox semidirect product. Every element of the closed Fox graph target has a preimage under the free pro-\(C\) semidirect lift.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
    (x : X) :
    freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
        (C := C) hι φ htarget hφconv (ι x) =
      freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x

The closed-generated semidirect lift into the ambient semidirect product sends each free pro-\(C\) generator to the corresponding Fox semidirect generator.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxRightHomViaClosedGenerated
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    F →* H :=
  (ZCCompletedFoxSemidirect.rightMonoidHom C X H).comp
    (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
      (C := C) hι φ htarget hφconv)

The right component of the closed-generated semidirect lift.

Theorem FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated_generator

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxRightHomViaClosedGenerated_generator
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
    (x : X) :
    freeProCZCCompletedFoxRightHomViaClosedGenerated
        (C := C) hι φ htarget hφconv (ι x) = φ x

The right component of the closed-generated semidirect lift sends each generator to its prescribed value \(\varphi(x)\).

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C
        (freeProCZCCompletedFoxRightHomViaClosedGenerated
          (C := C) hι φ htarget hφconv))
      (ZCFreeFoxCoordinates C (X := X) (H := H)) where
  toFun g :=
    (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
      (C := C) hι φ htarget hφconv g).left
  map_mul' g h := by
    have hmul := congrArg ZCCompletedFoxSemidirect.left
      (map_mul
        (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
          (C := C) hι φ htarget hφconv) g h)
    simpa only [ZCCompletedFoxSemidirect.mul_left,
      freeProCZCCompletedFoxRightHomViaClosedGenerated,
      scalarCrossedAction_apply, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_comp,
      Function.comp_apply, ZCCompletedFoxSemidirect.rightMonoidHom_apply] using hmul

The scalar crossed homomorphism given by the left component of the closed-generated semidirect lift.

Theorem FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
    (x : X) :
    freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
        (C := C) hι φ htarget hφconv (ι x) =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)

The derivative-vector component of the closed-generated semidirect lift has standard basis value at each generator.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectLift

def freeProCZCCompletedFoxSemidirectLift
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    F →* ZCCompletedFoxSemidirect C X H :=
  hι.lift htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ

The continuous completed Fox semidirect lift from a free pro-\(C\) source.

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom

def freeProCZCCompletedFoxSemidirectLiftHom
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    F →ₜ* ZCCompletedFoxSemidirect C X H :=
  hι.liftHom htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ

The continuous homomorphism form of the completed Fox semidirect lift from a free pro-\(C\) source.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_toMonoidHom

@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftHom_toMonoidHom
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    (freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι htarget φ hφ).toMonoidHom =
      freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ

Forgetting continuity from the continuous semidirect lift gives the underlying semidirect lift.

Show Lean proof

Theorem FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectLift

theorem continuous_freeProCZCCompletedFoxSemidirectLift
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    Continuous (freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ)

The free pro-\(C\) semidirect lift is continuous.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLift_generator

@[simp]
theorem freeProCZCCompletedFoxSemidirectLift_generator
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ (ι x) =
      freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x

The free pro-\(C\) semidirect lift has the prescribed completed Fox generator values.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_generator

@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftHom_generator
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι htarget φ hφ (ι x) =
      freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x

The continuous semidirect lift has the prescribed completed Fox generator values.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectLiftOfConvergingSet

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
    F →* ZCCompletedFoxSemidirect C X H :=
  hι.lift htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
    hφconv hφgen

The completed Fox semidirect lift from a converging-set free pro-\(C\) source. The generator map into the semidirect target is required to converge to \(1\) and topologically generate the target, matching the universal property of a free pro-\(C\) group on a converging set.

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
    F →ₜ* ZCCompletedFoxSemidirect C X H :=
  hι.liftHom htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
    hφconv hφgen

Continuous homomorphism form of the converging-set completed Fox semidirect lift.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_toMonoidHom

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_toMonoidHom
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
    (freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
        (C := C) hι htarget φ hφconv hφgen).toMonoidHom =
      freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
        (C := C) hι htarget φ hφconv hφgen

Forgetting continuity from the converging-set semidirect lift homomorphism gives the unbundled lift.

Show Lean proof

Theorem FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet

omit [TopologicalSpace X] in
theorem continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
    Continuous (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
        (C := C) hι htarget φ hφconv hφgen)

The completed Fox semidirect lift associated to a converging generator family is continuous.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
    (x : X) :
    freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
        (C := C) hι htarget φ hφconv hφgen (ι x) =
      freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x

The converging-set semidirect lift has the prescribed generator values.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_surjective

omit [TopologicalSpace X] in
theorem freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_surjective
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
    Function.Surjective
      (freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
        (C := C) hι htarget φ hφconv hφgen)

The converging-set semidirect lift is surjective once its prescribed generator values topologically generate the semidirect target.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxRightHomOfConvergingSet

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxRightHomOfConvergingSet
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
    F →* H :=
  (ZCCompletedFoxSemidirect.rightMonoidHom C X H).comp
    (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
      (C := C) hι htarget φ hφconv hφgen)

The right component of the converging-set semidirect lift.

Definition FoxDifferential.freeProCZCCompletedFoxDerivativeVectorOfConvergingSet

omit [TopologicalSpace X] in
def freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
    ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C
        (freeProCZCCompletedFoxRightHomOfConvergingSet
          (C := C) hι htarget φ hφconv hφgen))
      (ZCFreeFoxCoordinates C (X := X) (H := H)) where
  toFun g :=
    (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
      (C := C) hι htarget φ hφconv hφgen g).left
  map_mul' g h := by
    have hmul := congrArg ZCCompletedFoxSemidirect.left
      (map_mul
        (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
          (C := C) hι htarget φ hφconv hφgen) g h)
    simpa only [ZCCompletedFoxSemidirect.mul_left,
      freeProCZCCompletedFoxRightHomOfConvergingSet,
      ZCCompletedFoxSemidirect.rightMonoidHom,
      scalarCrossedAction_apply, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_comp,
      MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply] using hmul

The scalar crossed homomorphism given by the left component of the converging-set semidirect lift.

Theorem FoxDifferential.freeProCZCCompletedFoxRightHomOfConvergingSet_generator

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxRightHomOfConvergingSet_generator
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
    (x : X) :
    freeProCZCCompletedFoxRightHomOfConvergingSet
        (C := C) hι htarget φ hφconv hφgen (ι x) = φ x

The right component of the converging-set semidirect lift sends each generator to its prescribed value \(\varphi(x)\).

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator

omit [TopologicalSpace X] in
@[simp]
theorem freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator
    {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
    (x : X) :
    freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
        (C := C) hι htarget φ hφconv hφgen (ι x) =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)

The derivative-vector component of the converging-set semidirect lift has standard basis value at each generator.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism

def freeProCZCCompletedFoxSemidirectLiftMorphism
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
      ProCGrp.of C
        (ProfiniteGrp.of
          (ZCCompletedFoxSemidirect C X H))
        hTargetC :=
  CategoryTheory.ObjectProperty.homMk
    (ProfiniteGrp.ofHom
      (freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι hTargetC φ hφ))

The categorical completed Fox semidirect lift from a free pro-\(C\) source is bundled as a morphism in ProCGrp.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_hom

@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftMorphism_hom
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    ProCGrp.continuousHom
      (freeProCZCCompletedFoxSemidirectLiftMorphism
        (C := C) hFC hTargetC hι φ hφ) =
      freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι hTargetC φ hφ

The underlying continuous homomorphism of the categorical completed Fox semidirect lift is the free pro-\(C\) continuous homomorphism supplied by liftHom.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_hom_toMonoidHom

@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftMorphism_hom_toMonoidHom
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    (ProCGrp.continuousHom
      (freeProCZCCompletedFoxSemidirectLiftMorphism
        (C := C) hFC hTargetC hι φ hφ)).toMonoidHom =
      freeProCZCCompletedFoxSemidirectLift
        (C := C) hι hTargetC φ hφ

The underlying homomorphism of the categorical completed Fox semidirect lift is the unbundled completed Fox semidirect lift.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_generator

@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftMorphism_generator
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    freeProCZCCompletedFoxSemidirectLiftMorphism
      (C := C) hFC hTargetC hι φ hφ (ι x) =
      freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x

The categorical completed Fox semidirect lift has the prescribed generator values.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_left_generator

@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftMorphism_left_generator
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    (freeProCZCCompletedFoxSemidirectLiftMorphism
      (C := C) hFC hTargetC hι φ hφ (ι x)).left =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)

The left component of the categorical completed Fox semidirect lift has the standard Fox coordinate on each generator.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_right_generator

@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftMorphism_right_generator
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    (freeProCZCCompletedFoxSemidirectLiftMorphism
      (C := C) hFC hTargetC hι φ hφ (ι x)).right = φ x

The right component of the categorical completed Fox semidirect lift has the prescribed generator value.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLift_left_generator

@[simp]
theorem freeProCZCCompletedFoxSemidirectLift_left_generator
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    (freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ (ι x)).left =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)

The left component of the free pro-\(C\) semidirect lift has the standard Fox coordinate on each generator.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_left_generator

@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftHom_left_generator
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    (freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι htarget φ hφ (ι x)).left =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)

The left component of the continuous free pro-\(C\) semidirect lift has the standard Fox coordinate on each generator.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLift_right_generator

@[simp]
theorem freeProCZCCompletedFoxSemidirectLift_right_generator
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    (freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ (ι x)).right = φ x

The right component of the free pro-\(C\) semidirect lift has the prescribed generator value.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_right_generator

@[simp]
theorem freeProCZCCompletedFoxSemidirectLiftHom_right_generator
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    (freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι htarget φ hφ (ι x)).right = φ x

The right component of the continuous free pro-\(C\) semidirect lift has the prescribed generator value.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxRightHom

def freeProCZCCompletedFoxRightHom
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    F →* H where
  toFun g := (freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ g).right
  map_one' := by
    simp only [map_one, ZCCompletedFoxSemidirect.one_right]
  map_mul' g h := by
    simp only [map_mul, ZCCompletedFoxSemidirect.mul_right]

The target-group component of the continuous completed Fox semidirect lift.

Theorem FoxDifferential.freeProCZCCompletedFoxRightHom_apply

@[simp]
theorem freeProCZCCompletedFoxRightHom_apply
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (g : F) :
    freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ g =
      (freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ g).right

The right component of the continuous completed Fox semidirect lift is the associated homomorphism.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxRightHom_generator

@[simp]
theorem freeProCZCCompletedFoxRightHom_generator
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ (ι x) = φ x

The target-group component has the prescribed generator values.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxDerivativeVector

def freeProCZCCompletedFoxDerivativeVector
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C
        (freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ))
      (ZCFreeFoxCoordinates C (X := X) (H := H)) where
  toFun g :=
    (freeProCZCCompletedFoxSemidirectLift
      (C := C) hι htarget φ hφ g).left
  map_mul' g h := by
    have hmul := congrArg ZCCompletedFoxSemidirect.left
      (map_mul (freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ) g h)
    simpa only [ZCCompletedFoxSemidirect.mul_left, freeProCZCCompletedFoxRightHom,
      scalarCrossedAction_apply, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_mk,
      OneHom.coe_mk] using hmul

The completed Fox derivative is the scalar crossed homomorphism obtained from the left component of the continuous free pro-\(C\) semidirect lift.

Theorem FoxDifferential.freeProCZCCompletedFoxDerivativeVector_generator

@[simp]
theorem freeProCZCCompletedFoxDerivativeVector_generator
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (x : X) :
    freeProCZCCompletedFoxDerivativeVector
        (C := C) hι htarget φ hφ (ι x) =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)

The free pro-\(C\) completed Fox derivative vector has the standard coordinate value on generators.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift

Declarations