Module

Existence.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Existence

2 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

existsUnique_freeProCZCCompletedFoxSemidirectLift

Existence and uniqueness of the continuous completed Fox semidirect lift from a free pro-\(C\) source.

existsUnique_freeProCZCCompletedFoxSemidirectLift_components

Componentwise existence and uniqueness of the continuous completed Fox semidirect lift from a free pro-\(C\) source.

Imports2

Imported by2

theorem

existsUnique_freeProCZCCompletedFoxSemidirectLift

L52 ↗

FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLift

Documentation

Existence and uniqueness of 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 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
    {ι : 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,
      Continuous f ∧
        ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x