Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.Continuous.Free.Continuity
ProCGroups/FoxDifferential/Completed/Continuous/Free/Continuity

ProCGroups.FoxDifferential.Completed.Continuous.Free.Continuity

15 Theorems

The principal declarations in this module are:

  • continuous_freeProCZCCompletedFoxSemidirectGenerator The completed Fox semidirect generator map is continuous when both component maps are continuous. - continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete The completed Fox semidirect generator map is continuous for a discrete generating space. - continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential A crossed-differential graph into the completed Fox semidirect target is continuous when both its component maps are continuous. - continuous_freeProCZCCompletedFoxRightHom The target-group component of the free pro-\(C\) completed Fox semidirect lift is continuous.
imports
Imported by

Declarations

Theorem FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectGenerator 
theorem continuous_freeProCZCCompletedFoxSemidirectGenerator
    [TopologicalSpace X]
    (φ : X → H)
    (hleft : Continuous (fun x : X =>
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)))
    (hφ : Continuous φ) :
    Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)

The completed Fox semidirect generator map is continuous when both component maps are continuous.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete 
theorem continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
    [TopologicalSpace X] [DiscreteTopology X] (φ : X → H) :
    Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)

The completed Fox semidirect generator map is continuous for a discrete generating space.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential 
omit
  [DecidableEq X] [IsTopologicalGroup F]
  [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
theorem continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ) :
    Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
      (C := C) (X := X) (F := F) (H := H) ψ delta)

A crossed-differential graph into the completed Fox semidirect target is continuous when both its component maps are continuous.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxRightHom 
theorem continuous_freeProCZCCompletedFoxRightHom
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    Continuous (freeProCZCCompletedFoxRightHom
      (C := C) hι htarget φ hφ)

The target-group component of the free pro-\(C\) completed Fox semidirect lift is continuous.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxRightHomOfConvergingSet 
omit
  [TopologicalSpace X] in
theorem continuous_freeProCZCCompletedFoxRightHomOfConvergingSet
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
    Continuous (freeProCZCCompletedFoxRightHomOfConvergingSet
      (C := C) hι htarget φ hφconv hφgen)

The right component of the converging-set completed Fox semidirect lift is continuous.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxRightHomOfConvergingSet_eq_lift 
omit
  [TopologicalSpace X] in
theorem freeProCZCCompletedFoxRightHomOfConvergingSet_eq_lift
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
    (hφHconv : ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups (G := H) φ)
    (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
    freeProCZCCompletedFoxRightHomOfConvergingSet
        (C := C) hι htarget φ hφconv hφgen =
      hι.lift hH φ hφHconv hφHgen

The right component of the converging-set semidirect Fox lift is exactly the universal free-pro-\(C\) lift of its generator values.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated 
omit
  [TopologicalSpace X] in
theorem continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    Continuous (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
      (C := C) hι φ htarget hφconv)

The closed-generated completed Fox semidirect lift is continuous as a map to the full semidirect target.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxRightHomViaClosedGenerated 
omit
  [TopologicalSpace X] in
theorem continuous_freeProCZCCompletedFoxRightHomViaClosedGenerated
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    Continuous (freeProCZCCompletedFoxRightHomViaClosedGenerated
      (C := C) hι φ htarget hφconv)

The right component of the closed-generated completed Fox semidirect lift is continuous.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift 
omit
  [TopologicalSpace X] in
theorem freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
    (hφHconv : ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups (G := H) φ)
    (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
    freeProCZCCompletedFoxRightHomViaClosedGenerated
        (C := C) hι φ htarget hφconv =
      hι.lift hH φ hφHconv hφHgen

The right component of the closed-generated semidirect Fox lift is the universal free-pro-\(C\) lift of its generator values.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom 
omit
  [TopologicalSpace X] in
theorem freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
    (hφHconv : ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups (G := H) φ)
    (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
    (ψ : F →ₜ* H)
    (hψ_gen : ∀ x : X, ψ (ι x) = φ x) :
    freeProCZCCompletedFoxRightHomViaClosedGenerated
        (C := C) hι φ htarget hφconv =
      ψ.toMonoidHom

The right component of the closed-generated semidirect Fox lift is the intended continuous homomorphism with the same generator values.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated 
omit
  [TopologicalSpace X] in
theorem continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (φ : X → H)
    (htarget :
      ProCGroups.ProC.HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
    Continuous (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
      (C := C) hι φ htarget hφconv)

The derivative-vector component of the closed-generated semidirect lift is continuous.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxDerivativeVector 
theorem continuous_freeProCZCCompletedFoxDerivativeVector
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
    Continuous (freeProCZCCompletedFoxDerivativeVector
      (C := C) hι htarget φ hφ)

The completed Fox derivative-vector component of the free pro-\(C\) semidirect lift is continuous.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxDerivativeVectorOfConvergingSet 
omit
  [TopologicalSpace X] in
theorem continuous_freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (φ : X → H)
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := ZCCompletedFoxSemidirect C X H)
        (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := ZCCompletedFoxSemidirect C X H)
        (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
    Continuous (freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
      (C := C) hι htarget φ hφconv hφgen)

The derivative-vector component of the converging-set completed Fox semidirect lift is continuous.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff 
theorem continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
    (hbasis :
      ∀ x : X, delta (ι x) =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
    Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x)))

The semidirect generator map attached to a continuous crossed differential is continuous once the component maps are continuous.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDiff_components 
theorem freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDiff_components
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
    (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_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff
            (C := C) X H hι ψ delta hdelta_continuous hψ_continuous hbasis) g

Continuous completed crossed differentials with continuous coefficient homomorphism are uniquely identified with the canonical free pro-\(C\) completed Fox derivative vector.

Show Lean proof