NYLL
Module

Rules.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Free.Rules
13 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — free — rules

The principal declarations in this module are:

  • freeProCZCCompletedFoxRightHomContinuousMonoidHom

The right component of the completed free pro-\(C\) Fox lift is bundled as a continuous homomorphism.

  • freeProCZCCompletedFoxDerivativeVectorContinuousMap

The completed free pro-\(C\) Fox derivative vector is bundled as a continuous map; it is a crossed differential, not a homomorphism.

  • freeProCZCCompletedFoxRightHomContinuousMonoidHom_toMonoidHom

The bundled right homomorphism has the expected underlying monoid homomorphism.

  • freeProCZCCompletedFoxRightHomContinuousMonoidHom_apply

Evaluation of the bundled right homomorphism.

Imports2
Imported by4

Declarations

def

freeProCZCCompletedFoxRightHomContinuousMonoidHom

L58 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomContinuousMonoidHom
Documentation

The right component of the completed free pro-\(C\) Fox lift is bundled as a continuous homomorphism.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
Lean source · full declaration
def freeProCZCCompletedFoxRightHomContinuousMonoidHom : F →ₜ* H where
  toMonoidHom := freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ
  continuous_toFun :=
    continuous_freeProCZCCompletedFoxRightHom (C := C) X H hι htarget φ hφ
theorem

freeProCZCCompletedFoxRightHomContinuousMonoidHom_toMonoidHom

L65 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomContinuousMonoidHom_toMonoidHom
Documentation

The bundled right homomorphism has the expected underlying monoid homomorphism.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
Lean source · statement
theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_toMonoidHom :
    (freeProCZCCompletedFoxRightHomContinuousMonoidHom
      (C := C) hι htarget φ hφ).toMonoidHom =
      freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ
theorem

freeProCZCCompletedFoxRightHomContinuousMonoidHom_apply

L73 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomContinuousMonoidHom_apply
Documentation

Evaluation of the bundled right homomorphism.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
Lean source · statement
theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_apply (g : F) :
    freeProCZCCompletedFoxRightHomContinuousMonoidHom
        (C := C) hι htarget φ hφ g =
      freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ g
theorem

freeProCZCCompletedFoxRightHomContinuousMonoidHom_generator

L81 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomContinuousMonoidHom_generator
Documentation

The bundled right homomorphism has the prescribed generator values.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
Lean source · statement
theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_generator (x : X) :
    freeProCZCCompletedFoxRightHomContinuousMonoidHom
        (C := C) hι htarget φ hφ (ι x) = φ x
def

freeProCZCCompletedFoxDerivativeVectorContinuousMap

L90 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVectorContinuousMap
Documentation

The completed free pro-\(C\) Fox derivative vector is bundled as a continuous map; it is a crossed differential, not a homomorphism.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
Lean source · full declaration
def freeProCZCCompletedFoxDerivativeVectorContinuousMap :
    ContinuousMap F (ZCFreeFoxCoordinates C (X := X) (H := H)) where
  toFun := freeProCZCCompletedFoxDerivativeVector (C := C) hι htarget φ hφ
  continuous_toFun :=
    continuous_freeProCZCCompletedFoxDerivativeVector (C := C) X H hι htarget φ hφ
theorem

freeProCZCCompletedFoxDerivativeVectorContinuousMap_apply

L98 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVectorContinuousMap_apply
Documentation

Evaluation of the bundled continuous completed Fox derivative vector.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
Lean source · statement
theorem freeProCZCCompletedFoxDerivativeVectorContinuousMap_apply (g : F) :
    freeProCZCCompletedFoxDerivativeVectorContinuousMap
        (C := C) hι htarget φ hφ g =
      freeProCZCCompletedFoxDerivativeVector (C := C) hι htarget φ hφ g
theorem

freeProCZCCompletedFoxDerivativeVectorContinuousMap_generator

L106 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVectorContinuousMap_generator
Documentation

The bundled continuous completed Fox derivative vector has the prescribed generator values.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
Lean source · statement
theorem freeProCZCCompletedFoxDerivativeVectorContinuousMap_generator (x : X) :
    freeProCZCCompletedFoxDerivativeVectorContinuousMap
        (C := C) hι htarget φ hφ (ι x) =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)
theorem

zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift

L117 ↗
FoxDifferential.zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift
Documentation

Restricting the continuous completed Fox derivative to the abstract free group generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
Lean source · statement
theorem zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift
    (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVector C
        ((freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ).comp
          (FreeGroup.lift ι)) w =
      freeProCZCCompletedFoxDerivativeVector
        (C := C) hι htarget φ hφ ((FreeGroup.lift ι) w)
theorem

zcFreeFoxDerivVec_eq_freeProCCompletedFoxDerivVec_comp_lift_mapTarget

L158 ↗
FoxDifferential.zcFreeFoxDerivVec_eq_freeProCCompletedFoxDerivVec_comp_lift_mapTarget
Documentation

Source restriction and target naturality for the continuous completed Fox derivative.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
Lean source · statement
theorem zcFreeFoxDerivVec_eq_freeProCCompletedFoxDerivVec_comp_lift_mapTarget
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    (η : H →ₜ* K) (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVector C
        (η.toMonoidHom.comp
          ((freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ).comp
            (FreeGroup.lift ι))) w =
      zcFreeFoxCoordinatesMap (X := X) C hC η
        (freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htarget φ hφ ((FreeGroup.lift ι) w))
theorem

zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift

L200 ↗
FoxDifferential.zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift
Documentation

Restricting the converging-set continuous completed Fox derivative to the abstract free group generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.

Source context 21 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCConvergingSetCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι :
  ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφconv :
  ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
    (G := ZCCompletedFoxSemidirect C X H)
    (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
variable (hφgen :
  ProCGroups.Generation.TopologicallyGenerates
    (G := ZCCompletedFoxSemidirect C X H)
    (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
omit [TopologicalSpace X] in
Lean source · statement
theorem zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift
    (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVector C
        ((freeProCZCCompletedFoxRightHomOfConvergingSet
            (C := C) hι htarget φ hφconv hφgen).comp
          (FreeGroup.lift ι)) w =
      freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
        (C := C) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w)
theorem

zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift_mapTarget

L248 ↗
FoxDifferential.zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift_mapTarget
Documentation

Source restriction and target naturality for the converging-set continuous completed Fox derivative.

Source context 21 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCConvergingSetCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι :
  ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
variable (φ : X → H)
variable (hφconv :
  ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
    (G := ZCCompletedFoxSemidirect C X H)
    (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
variable (hφgen :
  ProCGroups.Generation.TopologicallyGenerates
    (G := ZCCompletedFoxSemidirect C X H)
    (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
omit [TopologicalSpace X] in
Lean source · statement
theorem zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift_mapTarget
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    (η : H →ₜ* K) (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVector C
        (η.toMonoidHom.comp
          ((freeProCZCCompletedFoxRightHomOfConvergingSet
              (C := C) hι htarget φ hφconv hφgen).comp
            (FreeGroup.lift ι))) w =
      zcFreeFoxCoordinatesMap (X := X) C hC η
        (freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
          (C := C) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w))
theorem

zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift

L292 ↗
FoxDifferential.zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift
Documentation

Restricting the closed-generated continuous completed Fox derivative to the abstract free group generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.

Source context 20 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCClosedGeneratedCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι :
  ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
variable (φ : X → H)
variable (htarget :
  ProCGroups.ProC.HasOpenNormalBasisInClass C
    (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
        (ZCCompletedFoxSemidirect C X H)))
variable (hφconv :
  ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
    (G :=
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)))
    (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
omit [TopologicalSpace X] in
Lean source · statement
theorem zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift
    (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVector C
        ((freeProCZCCompletedFoxRightHomViaClosedGenerated
            (C := C) hι φ htarget hφconv).comp
          (FreeGroup.lift ι)) w =
      freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
        (C := C) hι φ htarget hφconv ((FreeGroup.lift ι) w)
theorem

zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift_mapTarget

L340 ↗
FoxDifferential.zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift_mapTarget
Documentation

Source restriction and target naturality for the closed-generated continuous completed Fox derivative.

Source context 20 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F H : Type u}
variable [TopologicalSpace X] [DecidableEq X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FreeProCClosedGeneratedCompletedRules
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable {ι : X → F}
variable (hι :
  ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
variable (φ : X → H)
variable (htarget :
  ProCGroups.ProC.HasOpenNormalBasisInClass C
    (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
        (ZCCompletedFoxSemidirect C X H)))
variable (hφconv :
  ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
    (G :=
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)))
    (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
omit [TopologicalSpace X] in
Lean source · statement
theorem zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift_mapTarget
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    (η : H →ₜ* K) (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVector C
        (η.toMonoidHom.comp
          ((freeProCZCCompletedFoxRightHomViaClosedGenerated
              (C := C) hι φ htarget hφconv).comp
            (FreeGroup.lift ι))) w =
      zcFreeFoxCoordinatesMap (X := X) C hC η
        (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
          (C := C) hι φ htarget hφconv ((FreeGroup.lift ι) w))

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