Derivative.lean

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φ := by
  have hgenerator :
      ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x := by
    intro x
    apply ZCCompletedFoxSemidirect.ext
    · exact hleft x
    · exact hright x
  have hf_eq := hι.lift_unique htarget
    (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ hf hgenerator
  funext g
  rw [hf_eq]
  rfl

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 := by
  have hleft :
      ∀ x : X,
        (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
          (X := X) ψ delta (ι x)).left =
          Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
    intro x
    exact hbasis x
  have hright :
      ∀ x : X,
        (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
          (X := X) ψ delta (ι x)).right = ψ (ι x) := by
    intro x
    rfl
  have hunique := freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect
    (C := C) hι htarget (fun x : X => ψ (ι x))
    (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
      (C := C) hι ψ delta hcontinuous hbasis)
    (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
      (X := X) ψ delta)
    hcontinuous hleft hright
  simpa using hunique

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

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) := by
  apply MonoidHom.ext
  intro g
  have hgenerator :
      ∀ x : X,
        freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
            (X := X) ψ delta (ι x) =
          freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x)) x := by
    intro x
    apply ZCCompletedFoxSemidirect.ext
    · exact hbasis x
    · rfl
  have hsemidirect := hι.lift_unique htarget
    (freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x)))
    (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
      (C := C) hι ψ delta hcontinuous hbasis)
    (f := freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
      (X := X) ψ delta)
    hcontinuous hgenerator
  change ψ g =
    ((hι.lift htarget
      (freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x)))
      (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
        (C := C) hι ψ delta hcontinuous hbasis)) g).right
  exact congrArg
    (fun f : F →* ZCCompletedFoxSemidirect C X H => (f g).right) hsemidirect