NYLL
Module

DiscreteGenerators.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Free.DiscreteGenerators
4 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — free — discrete generators

The principal declarations in this module are:

  • existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators

Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

  • existsUnique_freeProCZCFoxSemiLiftHom_components_of_discreteGenerators

Componentwise continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

  • existsUnique_freeProCZCCompletedFoxSemidirectLift_of_discreteGenerators

Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

  • existsUnique_freeProCZCFoxSemiLift_components_of_discreteGenerators

Componentwise continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

Imports2
Imported by2

Declarations

theorem

existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators

L60 ↗
FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators
Documentation

Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

Source context 16 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 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]
variable [DiscreteTopology 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 existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H) :
    ∃! f : F →ₜ* ZCCompletedFoxSemidirect C X H,
      ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x
theorem

existsUnique_freeProCZCFoxSemiLiftHom_components_of_discreteGenerators

L74 ↗
FoxDifferential.existsUnique_freeProCZCFoxSemiLiftHom_components_of_discreteGenerators
Documentation

Componentwise continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

Source context 16 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 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]
variable [DiscreteTopology 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 existsUnique_freeProCZCFoxSemiLiftHom_components_of_discreteGenerators
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H) :
    ∃! f : F →ₜ* ZCCompletedFoxSemidirect C X H,
      (∀ x : X, (f (ι x)).left =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H)) ∧
      ∀ x : X, (f (ι x)).right = φ x
theorem

existsUnique_freeProCZCCompletedFoxSemidirectLift_of_discreteGenerators

L90 ↗
FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLift_of_discreteGenerators
Documentation

Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

Source context 16 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 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]
variable [DiscreteTopology 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 existsUnique_freeProCZCCompletedFoxSemidirectLift_of_discreteGenerators
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H) :
    ∃! f : F →* ZCCompletedFoxSemidirect C X H,
      Continuous f ∧
        ∀ x : X, f (ι x) =
          freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x
theorem

existsUnique_freeProCZCFoxSemiLift_components_of_discreteGenerators

L106 ↗
FoxDifferential.existsUnique_freeProCZCFoxSemiLift_components_of_discreteGenerators
Documentation

Componentwise continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

Source context 16 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 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]
variable [DiscreteTopology 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 existsUnique_freeProCZCFoxSemiLift_components_of_discreteGenerators
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H) :
    ∃! f : F →* ZCCompletedFoxSemidirect C X H,
      Continuous f ∧
        (∀ x : X, (f (ι x)).left =
          Pi.single x (1 : ZCCompletedGroupAlgebra C H)) ∧
        ∀ x : X, (f (ι x)).right = φ x

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