ProCGroups.FoxDifferential.Completed.Continuous.Free.DiscreteGenerators

4 Theorems

The principal declarations in this module are:

existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis. - existsUnique_freeProCZCFoxSemiLiftHom_components_of_discreteGenerators Componentwise continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis. - existsUnique_freeProCZCCompletedFoxSemidirectLift_of_discreteGenerators Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis. - existsUnique_freeProCZCFoxSemiLift_components_of_discreteGenerators Componentwise continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

imports

Imported by

Theorem FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators

theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H) :
    ∃! f : F →ₜ* ZCCompletedFoxSemidirect C X H,
      ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x

Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

Show Lean proof

Theorem FoxDifferential.existsUnique_freeProCZCFoxSemiLiftHom_components_of_discreteGenerators

theorem existsUnique_freeProCZCFoxSemiLiftHom_components_of_discreteGenerators
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H) :
    ∃! 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 continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

Show Lean proof

Theorem FoxDifferential.existsUnique_freeProCZCCompletedFoxSemidirectLift_of_discreteGenerators

theorem existsUnique_freeProCZCCompletedFoxSemidirectLift_of_discreteGenerators
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H) :
    ∃! f : F →* ZCCompletedFoxSemidirect C X H,
      Continuous f ∧
        ∀ x : X, f (ι x) =
          freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x

Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

Show Lean proof

Theorem FoxDifferential.existsUnique_freeProCZCFoxSemiLift_components_of_discreteGenerators

theorem existsUnique_freeProCZCFoxSemiLift_components_of_discreteGenerators
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H) :
    ∃! 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 continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete generators, without a separate generator-continuity hypothesis.

Show Lean proof

ProCGroups.FoxDifferential.Completed.Continuous.Free.DiscreteGenerators

Declarations