ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Existence

2 Theorems

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.

imports

Imported by

Theorem FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLift

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

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

Show Lean proof

Theorem FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLift_components

theorem existsUnique_freeProCZCCompletedFoxSemidirectLift_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,
      Continuous f ∧
        (∀ x : X, (f (ι x)).left =
          Pi.single x (1 : ZCCompletedGroupAlgebra C H)) ∧
        ∀ x : X, (f (ι x)).right = φ x

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Existence

Declarations