NYLL
Module

Morphism.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Morphism
4 declarations indexed from sourceView source ↗

Module documentation

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

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.

Imports1
Imported by2

Declarations

theorem

freeProCZCCompletedFoxSemidirectLiftMorphism_unique

L54 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_unique
Documentation

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

Source context 16 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 [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace
  (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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φ
theorem

freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components

L84 ↗
FoxDifferential.freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components
Documentation

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

Source context 16 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 [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace
  (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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φ
theorem

existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism

L114 ↗
FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism
Documentation

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

Source context 16 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 [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace
  (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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
theorem

existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism_components

L140 ↗
FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism_components
Documentation

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

Source context 16 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 [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace
  (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
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

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.