ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Derivative

4 Theorems

The principal declarations in this module are:

freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect Any continuous semidirect lift with the prescribed generator components has the canonical free pro-\(C\) completed Fox derivative vector as its left component. - freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDifferential Continuous completed crossed differentials on a free pro-\(C\) source are uniquely determined by their standard generator values, provided their semidirect graph is continuous. - freeProCZCCompletedCrossedDifferential_ext Extensionality for continuous completed crossed differentials on a free pro-\(C\) source. The continuity hypotheses are put on the associated semidirect homomorphisms, which is the form used by the completed Fox construction before the target topology is fully structural. - freeProCZCCompletedFoxRightHom_eq_of_continuousCrossedDifferential The coefficient homomorphism of a continuous completed crossed differential agrees with the right component of the canonical free pro-\(C\) semidirect lift.

import

ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom

Imported by

Theorem FoxDifferential.freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect

theorem freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect
    {ι : 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) :
    (fun g : F => (f g).left) =
      freeProCZCCompletedFoxDerivativeVector
        (C := C) hι htarget φ hφ

Any continuous semidirect lift with the prescribed generator components has the canonical free pro-\(C\) completed Fox derivative vector as its left component.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDifferential

theorem freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDifferential
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hcontinuous :
      Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
        (X := X) ψ delta))
    (hbasis :
      ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
    (fun g : F => delta g) =
      fun g : F =>
        freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htarget (fun x : X => ψ (ι x))
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
            (C := C) hι ψ delta hcontinuous hbasis) g

Continuous completed crossed differentials on a free pro-\(C\) source are uniquely determined by their standard generator values, provided their semidirect graph is continuous.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedCrossedDifferential_ext

omit [DecidableEq X] in
theorem freeProCZCCompletedCrossedDifferential_ext
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (ψ : F →* H)
    (delta epsilon :
      ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
        (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous :
      Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
        (X := X) ψ delta))
    (hepsilon_continuous :
      Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
        (X := X) ψ epsilon))
    (hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
    delta = epsilon

Extensionality for continuous completed crossed differentials on a free pro-\(C\) source. The continuity hypotheses are put on the associated semidirect homomorphisms, which is the form used by the completed Fox construction before the target topology is fully structural.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxRightHom_eq_of_continuousCrossedDifferential

theorem freeProCZCCompletedFoxRightHom_eq_of_continuousCrossedDifferential
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hcontinuous :
      Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
        (X := X) ψ delta))
    (hbasis :
      ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
    ψ =
      freeProCZCCompletedFoxRightHom
        (C := C) hι htarget (fun x : X => ψ (ι x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
          (C := C) hι ψ delta hcontinuous hbasis)

The coefficient homomorphism of a continuous completed crossed differential agrees with the right component of the canonical free pro-\(C\) semidirect lift.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Derivative

Declarations