NYLL
Module

Lift.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Lift
6 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

  • freeProCZCCompletedFoxSemidirectLift_unique

Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique once their generator values are prescribed.

  • freeProCZCCompletedFoxSemidirectLift_unique_of_components

Componentwise uniqueness for continuous completed Fox semidirect lifts from a free pro-\(C\) source.

  • freeProCZCCompletedFoxSemidirectLiftHom_unique

Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique once their generator values are prescribed.

  • freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components

Componentwise uniqueness for continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source.

Imports1
Imported by2

Declarations

theorem

freeProCZCCompletedFoxSemidirectLift_unique

L57 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLift_unique
Documentation

Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique once their generator values are prescribed.

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 ProfiniteTarget
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectLift_unique
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (f : F →* ZCCompletedFoxSemidirect C X H)
    (hf : Continuous f)
    (hgenerator :
      ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x) :
    f = freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ
theorem

freeProCZCCompletedFoxSemidirectLift_unique_of_components

L75 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLift_unique_of_components
Documentation

Componentwise uniqueness for continuous completed Fox semidirect lifts 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 ProfiniteTarget
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectLift_unique_of_components
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (f : F →* ZCCompletedFoxSemidirect C X H)
    (hf : Continuous f)
    (hleft :
      ∀ x : X, (f (ι x)).left =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (hright : ∀ x : X, (f (ι x)).right = φ x) :
    f = freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htarget φ hφ
theorem

freeProCZCCompletedFoxSemidirectLiftHom_unique

L99 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_unique
Documentation

Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique once their generator values are prescribed.

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 ProfiniteTarget
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectLiftHom_unique
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (f : F →ₜ* ZCCompletedFoxSemidirect C X H)
    (hgenerator :
      ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x) :
    f = freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι htarget φ hφ
theorem

freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components

L116 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components
Documentation

Componentwise uniqueness for continuous completed Fox semidirect homomorphisms 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 ProfiniteTarget
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
theorem freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (f : F →ₜ* ZCCompletedFoxSemidirect C X H)
    (hleft :
      ∀ x : X, (f (ι x)).left =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (hright : ∀ x : X, (f (ι x)).right = φ x) :
    f = freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι htarget φ hφ
theorem

existsUnique_freeProCZCCompletedFoxSemidirectLiftHom

L139 ↗
FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftHom
Documentation

Existence and uniqueness of the continuous completed Fox semidirect homomorphism 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 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
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    ∃! f : F →ₜ* ZCCompletedFoxSemidirect C X H,
      ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x
theorem

existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_components

L158 ↗
FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_components
Documentation

Componentwise existence and uniqueness of the continuous completed Fox semidirect homomorphism 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 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_components
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    ∃! f : F →ₜ* ZCCompletedFoxSemidirect C X H,
      (∀ 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.