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

ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Morphism

4 Theorems

The principal declarations in this module are:

  • freeProCZCCompletedFoxSemidirectLiftMorphism_unique Categorical completed Fox semidirect morphisms from a free pro-\(C\) source are unique once their generator values are prescribed. - freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components Componentwise uniqueness for categorical completed Fox semidirect morphisms from a free pro-\(C\) source. - existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism Existence and uniqueness of the categorical completed Fox semidirect morphism from a free pro-\(C\) source. - existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism_components Componentwise existence and uniqueness of the categorical completed Fox semidirect morphism from a free pro-\(C\) source.
import
Imported by

Declarations

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_unique 
theorem freeProCZCCompletedFoxSemidirectLiftMorphism_unique
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (f :
      ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
        ProCGrp.of C
          (ProfiniteGrp.of
            (ZCCompletedFoxSemidirect C X H))
          hTargetC)
    (hgenerator :
      ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x) :
    f = freeProCZCCompletedFoxSemidirectLiftMorphism
      (C := C) hFC hTargetC hι φ hφ

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

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components 
theorem freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (f :
      ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
        ProCGrp.of C
          (ProfiniteGrp.of
            (ZCCompletedFoxSemidirect C X H))
          hTargetC)
    (hleft :
      ∀ x : X, (f (ι x)).left =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (hright : ∀ x : X, (f (ι x)).right = φ x) :
    f = freeProCZCCompletedFoxSemidirectLiftMorphism
      (C := C) hFC hTargetC hι φ hφ

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

Show Lean proof
Theorem FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism 
theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    ∃! f :
      ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
        ProCGrp.of C
          (ProfiniteGrp.of
            (ZCCompletedFoxSemidirect C X H))
          hTargetC,
      ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x

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

Show Lean proof
Theorem FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism_components 
theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism_components
    (hFC : ProCGroups.ProC.HasOpenNormalBasisInClass C (F))
    (hTargetC : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (ZCCompletedFoxSemidirect C X H))
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    ∃! f :
      ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
        ProCGrp.of C
          (ProfiniteGrp.of
            (ZCCompletedFoxSemidirect C X H))
          hTargetC,
      (∀ x : X, (f (ι x)).left =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H)) ∧
      ∀ x : X, (f (ι x)).right = φ x

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

Show Lean proof