Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Lift
ProCGroups/FoxDifferential/Completed/FreeProC/Uniqueness/Lift

ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Lift

6 Theorems

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.
import
Imported by

Declarations

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLift_unique 
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φ

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

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLift_unique_of_components 
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φ

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

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_unique 
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φ

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

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components 
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φ

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

Show Lean proof
Theorem FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftHom 
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

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

Show Lean proof
Theorem FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_components 
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

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

Show Lean proof