NYLL
Module

Continuity.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Free.Continuity
15 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — free — continuity

The principal declarations in this module are:

  • continuous_freeProCZCCompletedFoxSemidirectGenerator

The completed Fox semidirect generator map is continuous when both component maps are continuous.

  • continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete

The completed Fox semidirect generator map is continuous for a discrete generating space.

  • continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential

A crossed-differential graph into the completed Fox semidirect target is continuous when both its component maps are continuous.

  • continuous_freeProCZCCompletedFoxRightHom

The target-group component of the free pro-\(C\) completed Fox semidirect lift is continuous.

Imports2
Imported by4

Declarations

theorem

continuous_freeProCZCCompletedFoxSemidirectGenerator

L44 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectGenerator
Documentation

The completed Fox semidirect generator map is continuous when both component maps are continuous.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · full declaration
theorem continuous_freeProCZCCompletedFoxSemidirectGenerator
    [TopologicalSpace X]
    (φ : X → H)
    (hleft : Continuous (fun x : X =>
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)))
    (hφ : Continuous φ) :
    Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) := by
  rw [continuous_induced_rng]
  exact hleft.prodMk hφ
theorem

continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete

L55 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
Documentation

The completed Fox semidirect generator map is continuous for a discrete generating space.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
    [TopologicalSpace X] [DiscreteTopology X] (φ : X → H) :
    Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
theorem

continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential

L71 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
Documentation

A crossed-differential graph into the completed Fox semidirect target is continuous when both its component maps are continuous.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit
  [DecidableEq X] [IsTopologicalGroup F]
  [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
Lean source · statement
theorem continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ) :
    Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
      (C := C) (X := X) (F := F) (H := H) ψ delta)
theorem

continuous_freeProCZCCompletedFoxRightHom

L90 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxRightHom
Documentation

The target-group component of the free pro-\(C\) completed Fox semidirect lift is continuous.

Source context 16 commands

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

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

continuous_freeProCZCCompletedFoxRightHomOfConvergingSet

L107 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxRightHomOfConvergingSet
Documentation

The right component of the converging-set completed Fox semidirect lift is continuous.

Source context 17 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
section ProfiniteTarget
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_freeProCZCCompletedFoxRightHomOfConvergingSet
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      ProCGroups.FreeProC.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 (freeProCZCCompletedFoxRightHomOfConvergingSet
      (C := C) hι htarget φ hφconv hφgen)
theorem

freeProCZCCompletedFoxRightHomOfConvergingSet_eq_lift

L140 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomOfConvergingSet_eq_lift
Documentation

The right component of the converging-set semidirect Fox lift is exactly the universal free-pro-\(C\) lift of its generator values.

Source context 19 commands

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

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

continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated

L174 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
Documentation

The closed-generated completed Fox semidirect lift is continuous as a map to the full semidirect target.

Source context 17 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
section ProfiniteTarget
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_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    Continuous (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
      (C := C) hι φ htarget hφconv)
theorem

continuous_freeProCZCCompletedFoxRightHomViaClosedGenerated

L202 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxRightHomViaClosedGenerated
Documentation

The right component of the closed-generated completed Fox semidirect lift is continuous.

Source context 17 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
section ProfiniteTarget
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_freeProCZCCompletedFoxRightHomViaClosedGenerated
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    Continuous (freeProCZCCompletedFoxRightHomViaClosedGenerated
      (C := C) hι φ htarget hφconv)
theorem

freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift

L236 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift
Documentation

The right component of the closed-generated semidirect Fox lift is the universal free-pro-\(C\) lift of its generator values.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
section ProfiniteTarget
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
section ProfiniteCodomain
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
omit
  [TopologicalSpace X] in
Lean source · statement
theorem freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
    (hφHconv : ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups (G := H) φ)
    (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
    freeProCZCCompletedFoxRightHomViaClosedGenerated
        (C := C) hι φ htarget hφconv =
      hι.lift hH φ hφHconv hφHgen
theorem

freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom

L269 ↗
FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
Documentation

The right component of the closed-generated semidirect Fox lift is the intended continuous homomorphism with the same generator values.

Source context 19 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
section ProfiniteTarget
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
section ProfiniteCodomain
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
omit
  [TopologicalSpace X] in
Lean source · statement
theorem freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
    (hφHconv : ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups (G := H) φ)
    (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
    (ψ : F →ₜ* H)
    (hψ_gen : ∀ x : X, ψ (ι x) = φ x) :
    freeProCZCCompletedFoxRightHomViaClosedGenerated
        (C := C) hι φ htarget hφconv =
      ψ.toMonoidHom
theorem

continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated

L310 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
Documentation

The derivative-vector component of the closed-generated semidirect lift is continuous.

Source context 17 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
section ProfiniteTarget
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_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    Continuous (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
      (C := C) hι φ htarget hφconv)
theorem

continuous_freeProCZCCompletedFoxDerivativeVector

L338 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxDerivativeVector
Documentation

The completed Fox derivative-vector component of the free pro-\(C\) semidirect lift is continuous.

Source context 16 commands

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

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

continuous_freeProCZCCompletedFoxDerivativeVectorOfConvergingSet

L358 ↗
FoxDifferential.continuous_freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
Documentation

The derivative-vector component of the converging-set completed Fox semidirect lift is continuous.

Source context 17 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
section ProfiniteTarget
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_freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      ProCGroups.FreeProC.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 (freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
      (C := C) hι htarget φ hφconv hφgen)
theorem

continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff

L387 ↗
FoxDifferential.continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff
Documentation

The semidirect generator map attached to a continuous crossed differential is continuous once the component maps are continuous.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
Lean source · full declaration
theorem continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
    (hbasis :
      ∀ x : X, delta (ι x) =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
    Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x))) :=
  continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
    (C := C) hι ψ delta
    (continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
      (C := C) (X := X) (F := F) (H := H)
      ψ delta hdelta_continuous hψ_continuous)
    hbasis
theorem

freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDiff_components

L414 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDiff_components
Documentation

Continuous completed crossed differentials with continuous coefficient homomorphism are uniquely identified with the canonical free pro-\(C\) completed Fox derivative vector.

Source context 16 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
section ProfiniteTarget
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · full declaration
theorem freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDiff_components
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
    (hbasis :
      ∀ x : X, delta (ι x) =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
    (fun g : F => delta g) =
      fun g : F =>
        freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htarget (fun x : X => ψ (ι x))
          (continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff
            (C := C) X H hι ψ delta hdelta_continuous hψ_continuous hbasis) g :=
  freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDifferential
    (C := C) hι htarget ψ delta
    (continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
      (C := C) (X := X) (F := F) (H := H)
      ψ delta hdelta_continuous hψ_continuous)
    hbasis

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