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

ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom

3 Theorems | 1 Definition

The principal declarations in this module are:

  • freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential A completed crossed differential and its coefficient homomorphism combine into a semidirect homomorphism. - freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_left The semidirect homomorphism attached to a crossed differential has \(\delta\) as its left component. - freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_right The semidirect homomorphism attached to a crossed differential has \(\psi\)s its right component. - continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential If a crossed-differential semidirect homomorphism is continuous and has the standard generator coordinates, then the corresponding semidirect generator map is continuous.
import
Imported by

Declarations

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential 
def freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H))) :
    F →* ZCCompletedFoxSemidirect C X H where
  toFun g := { left := delta g, right := ψ g }
  map_one' := by
    apply ZCCompletedFoxSemidirect.ext
    · exact delta.map_one
    · simp only [map_one, ZCCompletedFoxSemidirect.one_right]
  map_mul' g h := by
    apply ZCCompletedFoxSemidirect.ext
    · exact delta.map_mul g h
    · simp only [map_mul, ZCCompletedFoxSemidirect.mul_right]

A completed crossed differential and its coefficient homomorphism combine into a semidirect homomorphism.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_left 
omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] [DecidableEq X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_left
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (g : F) :
    (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
      (X := X) ψ delta g).left = delta g

The semidirect homomorphism attached to a crossed differential has \(\delta\) as its left component.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_right 
omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] [DecidableEq X]
  [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_right
    (ψ : F →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (g : F) :
    (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
      (X := X) ψ delta g).right = ψ g

The semidirect homomorphism attached to a crossed differential has \(\psi\)s its right component.

Show Lean proof
Theorem FoxDifferential.continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential 
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
    {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
    (ψ : 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)) :
    Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x)))

If a crossed-differential semidirect homomorphism is continuous and has the standard generator coordinates, then the corresponding semidirect generator map is continuous.

Show Lean proof