NYLL
Module

SemidirectLift.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift
79 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — semidirect lift

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.

Imports2
Imported by4

Declarations

def

freeProCZCCompletedFoxSemidirectGenerator

L49 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator
Documentation

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

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
def freeProCZCCompletedFoxSemidirectGenerator (φ : X → H) :
    X → ZCCompletedFoxSemidirect C X H
theorem

freeProCZCCompletedFoxSemidirectGenerator_left

L59 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator_left
Documentation

The generator map has the expected left coordinate.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectGenerator_left
    (φ : X → H) (x : X) :
    (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x).left =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)
theorem

freeProCZCCompletedFoxSemidirectGenerator_right

L69 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator_right
Documentation

The generator map has the expected right coordinate.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectGenerator_right
    (φ : X → H) (x : X) :
    (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x).right = φ x
theorem

freeProCZCCompletedFoxSemidirectGenerator_convergesToOneAlongOpenSubgroups_of_finite

L80 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator_convergesToOneAlongOpenSubgroups_of_finite
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectGenerator_convergesToOneAlongOpenSubgroups_of_finite
    [Finite X] (φ : X → H) :
    FamilyConvergesToOneAlongOpenSubgroups
      (G := ZCCompletedFoxSemidirect C X H)
      (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
def

freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

L94 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
def freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (φ : X → H) :
    ClosedSubgroup (ZCCompletedFoxSemidirect C X H)
theorem

freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_hasOpenNormalBasisInClass

L103 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_hasOpenNormalBasisInClass
Documentation

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.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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))
def

freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator

L119 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
def freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (φ : X → H) :
    X →
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))
theorem

freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_val

L134 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_val
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_val
    (φ : X → H) (x : X) :
    (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ x :
      ZCCompletedFoxSemidirect C X H) =
      freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x
theorem

freeProCZCCompletedFoxSemidirectGenerator_mem_closedGeneratedTarget

L144 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGenerator_mem_closedGeneratedTarget
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectGenerator_mem_closedGeneratedTarget
    (φ : X → H) (x : X) :
    freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))
theorem

zcCompletedFoxSemidirectLift_freeGroupLift_mem_closedGeneratedTarget

L158 ↗
FoxDifferential.zcCompletedFoxSemidirectLift_freeGroupLift_mem_closedGeneratedTarget
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem zcCompletedFoxSemidirectLift_freeGroupLift_mem_closedGeneratedTarget
    (φ : X → H) (w : FreeGroup X) :
    zcCompletedFoxSemidirectLift C (FreeGroup.lift φ) w ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))
theorem

freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec

L193 ↗
FoxDifferential.freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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))
theorem

freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel

L211 ↗
FoxDifferential.freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel
Documentation

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.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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))
def

freeProCZCCompletedFoxSemidirectKernelCycleSet

L230 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectKernelCycleSet
Documentation

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.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
def freeProCZCCompletedFoxSemidirectKernelCycleSet (φ : X → H) :
    Set (ZCCompletedFoxSemidirect C X H)
def

freeProCZCCompletedFoxSemidirectBoundaryCycleSet

L248 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectBoundaryCycleSet
Documentation

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.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
def freeProCZCCompletedFoxSemidirectBoundaryCycleSet [Fintype X] (φ : X → H) :
    Set (ZCCompletedFoxSemidirect C X H)
def

freeProCZCCompletedFoxSemidirectGraphWordPoint

L260 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordPoint
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
def freeProCZCCompletedFoxSemidirectGraphWordPoint (φ : X → H) (w : FreeGroup X) :
    ZCCompletedFoxSemidirect C X H
theorem

freeProCZCCompletedFoxSemidirectGraphWordPoint_left

L274 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordPoint_left
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_left
    (φ : X → H) (w : FreeGroup X) :
    (freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w).left =
      zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w
theorem

freeProCZCCompletedFoxSemidirectGraphWordPoint_right

L287 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordPoint_right
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_right
    (φ : X → H) (w : FreeGroup X) :
    (freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w).right =
      FreeGroup.lift φ w
def

freeProCZCCompletedFoxSemidirectGraphWordSet

L297 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordSet
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
def freeProCZCCompletedFoxSemidirectGraphWordSet (φ : X → H) :
    Set (ZCCompletedFoxSemidirect C X H)
theorem

mem_freeProCZCCompletedFoxSemidirectGraphWordSet_iff

L309 ↗
FoxDifferential.mem_freeProCZCCompletedFoxSemidirectGraphWordSet_iff
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
theorem mem_freeProCZCCompletedFoxSemidirectGraphWordSet_iff
    {φ : X → H}
    {y : ZCCompletedFoxSemidirect C X H} :
    y ∈ freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ ↔
      ∃ w : FreeGroup X,
        y = freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w
theorem

freeProCZCCompletedFoxSemidirectGraphWordPoint_mem_closedGeneratedTarget

L322 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordPoint_mem_closedGeneratedTarget
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_mem_closedGeneratedTarget
    (φ : X → H) (w : FreeGroup X) :
    freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w ∈
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H))
theorem

freeProCZCCompletedFoxSemidirectGraphWordSet_subset_closedGeneratedTarget

L334 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectGraphWordSet_subset_closedGeneratedTarget
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectGraphWordSet_subset_closedGeneratedTarget
    (φ : X → H) :
    freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))
theorem

closure_freeProCZCFoxSemiGraphWordSet_subset_closedGenTarget

L347 ↗
FoxDifferential.closure_freeProCZCFoxSemiGraphWordSet_subset_closedGenTarget
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem closure_freeProCZCFoxSemiGraphWordSet_subset_closedGenTarget
    (φ : X → H) :
    closure (freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ) ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))
theorem

freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density

L364 ↗
FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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))
theorem

zcFreeGroupFoxBoundary_zcFreeGroupFoxDerivativeVector_of_kernel

L385 ↗
FoxDifferential.zcFreeGroupFoxBoundary_zcFreeGroupFoxDerivativeVector_of_kernel
Documentation

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.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
    [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet

L398 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet
Documentation

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

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet
    [Fintype X] (φ : X → H) :
    freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ ⊆
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ
def

freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup

L415 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup
Documentation

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)\).

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · full declaration
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]
theorem

freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup_coe

L461 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup_coe
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
    [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup_coe
    [Fintype X] (φ : X → H) :
    ((freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup
      (C := C) φ : Subgroup
        (ZCCompletedFoxSemidirect C X H)) : Set
        (ZCCompletedFoxSemidirect C X H)) =
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ
theorem

isClosed_freeProCZCCompletedFoxSemidirectBoundaryCycleSet_of_continuous

L476 ↗
FoxDifferential.isClosed_freeProCZCCompletedFoxSemidirectBoundaryCycleSet_of_continuous
Documentation

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.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] [DecidableEq X] [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · full declaration
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) φ) := by
  have hright_closed :
      IsClosed
        ((fun y : ZCCompletedFoxSemidirect C X H => y.right) ⁻¹'
          ({1} : Set H)) :=
    isClosed_singleton.preimage hright
  have hboundary_closed :
      IsClosed
        ((fun y : ZCCompletedFoxSemidirect C X H =>
            zcFreeGroupFoxBoundary C (FreeGroup.lift φ) y.left) ⁻¹'
          ({0} : Set (ZCCompletedGroupAlgebra C H))) :=
    isClosed_singleton.preimage (hboundary.comp hleft)
  change IsClosed
    (((fun y : ZCCompletedFoxSemidirect C X H => y.right) ⁻¹' ({1} : Set H)) ∩
      ((fun y : ZCCompletedFoxSemidirect C X H =>
        zcFreeGroupFoxBoundary C (FreeGroup.lift φ) y.left) ⁻¹'
          ({0} : Set (ZCCompletedGroupAlgebra C H))))
  exact hright_closed.inter hboundary_closed
theorem

closure_freeProCZCFoxSemiKernelCycleSet_subset_boundaryCycleSet_of_continuous

L515 ↗
FoxDifferential.closure_freeProCZCFoxSemiKernelCycleSet_subset_boundaryCycleSet_of_continuous
Documentation

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.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · full declaration
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) φ := by
  exact
    closure_minimal
      (freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet
        (C := C) φ)
      (isClosed_freeProCZCCompletedFoxSemidirectBoundaryCycleSet_of_continuous
        (C := C) φ hleft hright hboundary)
theorem

closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_iff_density

L544 ↗
FoxDifferential.closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_iff_density
Documentation

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.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
Lean source · full declaration
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) φ) := by
  constructor
  · intro h y hy
    simpa [h] using hy
  · intro hdensity
    ext y
    constructor
    · intro hy
      exact
        closure_freeProCZCFoxSemiKernelCycleSet_subset_boundaryCycleSet_of_continuous
          (C := C) φ hleft hright hboundary hy
    · intro hy
      exact hdensity hy
theorem

freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_closedGeneratedTarget

L577 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_closedGeneratedTarget
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_closedGeneratedTarget
    (φ : X → H) :
    freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))
theorem

closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget

L595 ↗
FoxDifferential.closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget
    (φ : X → H) :
    closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))
theorem

freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density

L613 ↗
FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
Documentation

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.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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))
theorem

freeProCZCFoxClosedGenTarget_mem_of_mem_closure_kernelCycleSet

L630 ↗
FoxDifferential.freeProCZCFoxClosedGenTarget_mem_of_mem_closure_kernelCycleSet
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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))
theorem

freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates

L645 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates
    (φ : X → H) :
    ProCGroups.Generation.TopologicallyGenerates
      (G :=
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
      (Set.range
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
theorem

freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite

L660 ↗
FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
theorem freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
    [Finite X] (φ : X → H) :
    FamilyConvergesToOneAlongOpenSubgroups
      (G :=
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
      (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)
def

freeProCZCCompletedFoxSemidirectLiftToClosedGenerated

L685 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
Documentation

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.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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))
def

freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated

L718 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
Documentation

Continuous homomorphism form of the closed-generated semidirect lift.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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))
theorem

freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_toMonoidHom

L755 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_toMonoidHom
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator

L780 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_surjective

L821 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_surjective
Documentation

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.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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)
def

freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated

L860 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
theorem

freeProCZCFoxSemiLiftViaClosedGen_exists_preimage_of_mem_closedGenTarget

L885 ↗
FoxDifferential.freeProCZCFoxSemiLiftViaClosedGen_exists_preimage_of_mem_closedGenTarget
Documentation

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.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator

L930 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
def

freeProCZCCompletedFoxRightHomViaClosedGenerated

L954 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated
Documentation

The right component of the closed-generated semidirect lift.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
theorem

freeProCZCCompletedFoxRightHomViaClosedGenerated_generator

L978 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
def

freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated

L1003 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · full declaration
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
theorem

freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator

L1040 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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)
def

freeProCZCCompletedFoxSemidirectLift

L1065 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLift
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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
def

freeProCZCCompletedFoxSemidirectLiftHom

L1077 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftHom_toMonoidHom

L1089 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_toMonoidHom
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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φ
theorem

continuous_freeProCZCCompletedFoxSemidirectLift

L1101 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectLift
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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φ)
theorem

freeProCZCCompletedFoxSemidirectLift_generator

L1113 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLift_generator
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftHom_generator

L1126 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_generator
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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
def

freeProCZCCompletedFoxSemidirectLiftOfConvergingSet

L1143 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
Documentation

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.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
def

freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet

L1161 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_toMonoidHom

L1183 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_toMonoidHom
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
theorem

continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet

L1203 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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)
theorem

freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator

L1223 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_surjective

L1247 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_surjective
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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)
def

freeProCZCCompletedFoxRightHomOfConvergingSet

L1278 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomOfConvergingSet
Documentation

The right component of the converging-set semidirect lift.

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
def

freeProCZCCompletedFoxDerivativeVectorOfConvergingSet

L1298 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · full declaration
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
theorem

freeProCZCCompletedFoxRightHomOfConvergingSet_generator

L1335 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomOfConvergingSet_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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
theorem

freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator

L1361 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace X] in
Lean source · statement
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)
def

freeProCZCCompletedFoxSemidirectLiftMorphism

L1390 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
section Categorical
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftMorphism_hom

L1412 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_hom
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
section Categorical
Lean source · statement
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φ
theorem

freeProCZCCompletedFoxSemidirectLiftMorphism_hom_toMonoidHom

L1431 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_hom_toMonoidHom
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
section Categorical
Lean source · statement
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φ
theorem

freeProCZCCompletedFoxSemidirectLiftMorphism_generator

L1447 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
section Categorical
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftMorphism_left_generator

L1466 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_left_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
section Categorical
Lean source · statement
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)
theorem

freeProCZCCompletedFoxSemidirectLiftMorphism_right_generator

L1485 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_right_generator
Documentation

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

Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
section Categorical
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLift_left_generator

L1505 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLift_left_generator
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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)
theorem

freeProCZCCompletedFoxSemidirectLiftHom_left_generator

L1522 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_left_generator
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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)
theorem

freeProCZCCompletedFoxSemidirectLift_right_generator

L1536 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLift_right_generator
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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
theorem

freeProCZCCompletedFoxSemidirectLiftHom_right_generator

L1552 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_right_generator
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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
def

freeProCZCCompletedFoxRightHom

L1564 ↗
FoxDifferential.freeProCZCCompletedFoxRightHom
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · full declaration
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]
theorem

freeProCZCCompletedFoxRightHom_apply

L1582 ↗
FoxDifferential.freeProCZCCompletedFoxRightHom_apply
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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
theorem

freeProCZCCompletedFoxRightHom_generator

L1595 ↗
FoxDifferential.freeProCZCCompletedFoxRightHom_generator
Documentation

The target-group component has the prescribed generator values.

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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
def

freeProCZCCompletedFoxDerivativeVector

L1607 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVector
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · full declaration
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
theorem

freeProCZCCompletedFoxDerivativeVector_generator

L1632 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVector_generator
Documentation

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

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.FreeProC
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
section Lifts
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.