{-# OPTIONS --without-K --safe #-}

-- The scalars of a monoidal category are the endomorphisms of the unit object.
-- They form a monoid under composition, with natural left and right actions on
-- the morphisms of the category. These actions define natural transformations
-- of the identity functor.
-- See https://ncatlab.org/nlab/show/scalar for this terminology
-- in dagger-, compact-, and closed monoidal categories, where scalars are
-- discussed as the endomorphism ring of the tensor unit. The same page cites
-- Abramsky and Coecke, "A categorical semantics of quantum protocols", §6
-- (LiCS 2004, arXiv:quant-ph/0402130, doi:10.1109/LICS.2004.1319636),
-- where scalars are C(I,I) for the tensor unit I.
-- By the Eckmann–Hilton argument, the scalars are commutative under composition.

open import Categories.Category.Core using (Category)
open import Categories.Category.Monoidal.Core using (Monoidal)

module Categories.Category.Monoidal.Scalars
    {o ℓ e} {𝒞 : Category o ℓ e} (M : Monoidal 𝒞) where

open import Algebra.Bundles using (Monoid; CommutativeMonoid)

open import Categories.Object.Endomorphism 𝒞 using (Endo; Endo-∘-Monoid)
open import Categories.Functor using () renaming (id to idF)
open import Categories.NaturalTransformation
  using (NaturalTransformation; ntHelper; _∘ᵥ_) renaming (id to idNT)
open import Categories.NaturalTransformation.Equivalence using (_≃_)
open import Categories.Category.Monoidal.Reasoning M
open import Categories.Category.Monoidal.Utilities M using (module Shorthands)
import Categories.Category.Monoidal.Properties M as MonoidalProps
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open Monoidal M
open Shorthands
open MonoidalProps.Kelly's

Scalar : Set _
Scalar = Endo unit

private
  Scalar-Base-Monoid : Monoid _ _
  Scalar-Base-Monoid = Endo-∘-Monoid unit

  variable
    A B C : Obj
    s t : Scalar

open Monoid Scalar-Base-Monoid public using () renaming (_∙_ to _·ₛ_; ε to idₛ)

module Action where
  infixl  _·ˡ_ _·ʳ_

  _·ˡ_ : Scalar → A ⇒ B → A ⇒ B
  s ·ˡ f = λ⇒ ∘ (s ⊗₁ f) ∘ λ⇐

  _·ʳ_ : A ⇒ B → Scalar → A ⇒ B
  f ·ʳ s = ρ⇒ ∘ (f ⊗₁ s) ∘ ρ⇐

  ·ˡ-resp-≈ : {f g : A ⇒ B} → s ≈ t → f ≈ g → s ·ˡ f ≈ t ·ˡ g
  ·ˡ-resp-≈ s≈t f≈g = ∘-resp-≈ʳ (∘-resp-≈ˡ (s≈t ⟩⊗⟨ f≈g))

  ·ʳ-resp-≈ : {f g : A ⇒ B} → f ≈ g → s ≈ t → f ·ʳ s ≈ g ·ʳ t
  ·ʳ-resp-≈ f≈g s≈t = ∘-resp-≈ʳ (∘-resp-≈ˡ (f≈g ⟩⊗⟨ s≈t))

  id-·ˡ : ∀ {f : A ⇒ B} → idₛ ·ˡ f ≈ f
  id-·ˡ {f = f} = begin
    λ⇒ ∘ (idₛ ⊗₁ f) ∘ λ⇐  ≈⟨ pullˡ unitorˡ-commute-from ⟩
    (f ∘ λ⇒) ∘ λ⇐         ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
    f                     ∎

  id-·ʳ : ∀ {f : A ⇒ B} → f ·ʳ idₛ ≈ f
  id-·ʳ {f = f} = begin
    ρ⇒ ∘ (f ⊗₁ idₛ) ∘ ρ⇐  ≈⟨ pullˡ unitorʳ-commute-from ⟩
    (f ∘ ρ⇒) ∘ ρ⇐         ≈⟨ cancelʳ unitorʳ.isoʳ ⟩
    f                     ∎

  ·ˡ-∘ : ∀ {f : B ⇒ C} {g : A ⇒ B} →
    (s ·ₛ t) ·ˡ (f ∘ g) ≈ (s ·ˡ f) ∘ (t ·ˡ g)
  ·ˡ-∘ {s = s} {t} {f} {g} = begin
    λ⇒ ∘ ((s ·ₛ t) ⊗₁ (f ∘ g)) ∘ λ⇐                   ≈⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ ⟩
    λ⇒ ∘ ((s ⊗₁ f) ∘ ((t ⊗₁ g) ∘ λ⇐))                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ unitorˡ.isoˡ ⟩
    λ⇒ ∘ ((s ⊗₁ f) ∘ (λ⇐ ∘ (λ⇒ ∘ ((t ⊗₁ g) ∘ λ⇐))))   ≈⟨ assoc²εβ ⟩
    (λ⇒ ∘ ((s ⊗₁ f) ∘ λ⇐)) ∘ (λ⇒ ∘ ((t ⊗₁ g) ∘ λ⇐))   ∎

  ·ʳ-∘ : ∀ {f : B ⇒ C} {g : A ⇒ B} →
    (f ∘ g) ·ʳ (s ·ₛ t) ≈ (f ·ʳ s) ∘ (g ·ʳ t)
  ·ʳ-∘ {s = s} {t} {f} {g} = begin
    ρ⇒ ∘ ((f ∘ g) ⊗₁ (s ·ₛ t)) ∘ ρ⇐                   ≈⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ ⟩
    ρ⇒ ∘ ((f ⊗₁ s) ∘ ((g ⊗₁ t) ∘ ρ⇐))                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ unitorʳ.isoˡ ⟩
    ρ⇒ ∘ ((f ⊗₁ s) ∘ (ρ⇐ ∘ (ρ⇒ ∘ ((g ⊗₁ t) ∘ ρ⇐))))   ≈⟨ assoc²εβ ⟩
    (ρ⇒ ∘ ((f ⊗₁ s) ∘ ρ⇐)) ∘ (ρ⇒ ∘ ((g ⊗₁ t) ∘ ρ⇐))   ∎

  unit-merge : ∀ {f : A ⇒ unit} {g : B ⇒ unit} →
    f ∘ ρ⇒ ∘ (id ⊗₁ g) ≈ λ⇒ ∘ (f ⊗₁ g)
  unit-merge {f = f} {g} = begin
    f ∘ ρ⇒ ∘ (id ⊗₁ g)              ≈⟨ pullˡ (⟺ unitorʳ-commute-from) ⟩
    (ρ⇒ ∘ (f ⊗₁ id)) ∘ (id ⊗₁ g)    ≈⟨ pullʳ merge₂ʳ ⟩
    ρ⇒ ∘ (f ⊗₁ (id ∘ g))            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ identityˡ ⟩
    ρ⇒ ∘ (f ⊗₁ g)                   ≈⟨ coherence₃ ⟩∘⟨refl ⟨
    λ⇒ ∘ (f ⊗₁ g)                   ∎

open Action public

-- Scalars are commutative: the Eckmann–Hilton argument.
-- See https://ncatlab.org/nlab/show/Eckmann-Hilton+argument for this.
-- On C(I,I) composition and tensor are unital operations that interchange (by
-- bifunctoriality of ⊗), so they coincide and commute (B. Eckmann & P. Hilton,
-- "Group-like structures in general categories I", Math. Ann. 145 (1962) 227–255).
-- Concretely the two actions agree on scalars (the unitors coincide on the unit),
-- while `s ·ʳ t` is `s ∘ t` and `s ·ˡ t` is `t ∘ s`.
module Eckmann-Hilton where
  -- The two actions agree on a scalar: the unitors coincide on the unit.
  ·ʳ≈·ˡ : s ·ʳ t ≈ s ·ˡ t
  ·ʳ≈·ˡ = ⟺ coherence₃ ⟩∘⟨ refl⟩∘⟨ ⟺ coherence-inv₃

  private
    -- A scalar sandwiched between the unitors in either slot is itself: swap the
    -- unitors by coherence₃ and apply id-·ˡ / id-·ʳ.
    absorbᵣ : ρ⇒ ∘ (id ⊗₁ s) ∘ ρ⇐ ≈ s
    absorbᵣ {s} = begin
      ρ⇒ ∘ (id ⊗₁ s) ∘ ρ⇐  ≈⟨ ·ʳ≈·ˡ ⟩
      λ⇒ ∘ (id ⊗₁ s) ∘ λ⇐  ≈⟨ id-·ˡ ⟩
      s                    ∎

    absorbₗ : λ⇒ ∘ (s ⊗₁ id) ∘ λ⇐ ≈ s
    absorbₗ {s} = begin
      λ⇒ ∘ (s ⊗₁ id) ∘ λ⇐  ≈⟨ ·ʳ≈·ˡ ⟨
      ρ⇒ ∘ (s ⊗₁ id) ∘ ρ⇐  ≈⟨ id-·ʳ ⟩
      s                    ∎

  -- Acting by a scalar on a scalar is composition: slide the acting scalar out
  -- past its unitor; the other unitor absorbs the scalar acted on.
  ·ʳ-scalar : s ·ʳ t ≈ s ∘ t
  ·ʳ-scalar {s} {t} = begin
    ρ⇒ ∘ (s ⊗₁ t) ∘ ρ⇐                 ≈⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
    ρ⇒ ∘ (s ⊗₁ id) ∘ (id ⊗₁ t) ∘ ρ⇐    ≈⟨ pullˡ unitorʳ-commute-from ⟩
    (s ∘ ρ⇒) ∘ (id ⊗₁ t) ∘ ρ⇐          ≈⟨ pullʳ absorbᵣ ⟩
    s ∘ t                              ∎

  ·ˡ-scalar : s ·ˡ t ≈ t ∘ s
  ·ˡ-scalar {s} {t} = begin
    λ⇒ ∘ (s ⊗₁ t) ∘ λ⇐                 ≈⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩
    λ⇒ ∘ (id ⊗₁ t) ∘ (s ⊗₁ id) ∘ λ⇐    ≈⟨ pullˡ unitorˡ-commute-from ⟩
    (t ∘ λ⇒) ∘ (s ⊗₁ id) ∘ λ⇐          ≈⟨ pullʳ absorbₗ ⟩
    t ∘ s                              ∎

  -- Eckmann–Hilton: s ∘ t = s ·ʳ t = s ·ˡ t = t ∘ s.
  scalar-comm : (s t : Scalar) → s ·ₛ t ≈ t ·ₛ s
  scalar-comm s t = begin
    s ∘ t   ≈˘⟨ ·ʳ-scalar ⟩
    s ·ʳ t  ≈⟨ ·ʳ≈·ˡ ⟩
    s ·ˡ t  ≈⟨ ·ˡ-scalar ⟩
    t ∘ s   ∎

  -- The scalars form a commutative monoid under composition.
  Scalar-Monoid : CommutativeMonoid _ _
  Scalar-Monoid = record
    { Carrier = Scalar
    ; _≈_ = _≈_
    ; _∙_ = _·ₛ_
    ; ε   = idₛ
    ; isCommutativeMonoid = record
      { isMonoid = Monoid.isMonoid Scalar-Base-Monoid
      ; comm     = scalar-comm
      }
    }

open Eckmann-Hilton public

-- Scalars act naturally on every object through the identity functor.
module NaturalAction where
  private abstract
    commute : (f : A ⇒ B) → (s ·ˡ id) ∘ f ≈ f ∘ (s ·ˡ id)
    commute {s = s} f = begin
      (s ·ˡ id) ∘ f           ≈⟨ refl⟩∘⟨ id-·ˡ ⟨
      (s ·ˡ id) ∘ (idₛ ·ˡ f)  ≈⟨ ·ˡ-∘ ⟨
      (s ·ₛ idₛ) ·ˡ (id ∘ f)  ≈⟨ ·ˡ-resp-≈ (scalar-comm s idₛ) (⟺ id-comm) ⟩
      (idₛ ·ₛ s) ·ˡ (f ∘ id)  ≈⟨ ·ˡ-∘ ⟩
      (idₛ ·ˡ f) ∘ (s ·ˡ id)  ≈⟨ id-·ˡ ⟩∘⟨refl ⟩
      f ∘ (s ·ˡ id)           ∎

  Scale⟦_⟧ : Scalar → NaturalTransformation (idF {C = 𝒞}) idF
  Scale⟦ s ⟧ = ntHelper record
    { η = λ _ → s ·ˡ id
    ; commute = commute
    }

  -- Scale⟦_⟧ is a monoid homomorphism to the natural transformations of the identity functor
  Scale-id : Scale⟦ idₛ ⟧ ≃ idNT
  Scale-id = id-·ˡ

  Scale-·ₛ : Scale⟦ s ·ₛ t ⟧ ≃ Scale⟦ s ⟧ ∘ᵥ Scale⟦ t ⟧
  Scale-·ₛ = ·ˡ-resp-≈ Equiv.refl (⟺ identityˡ) ○ ·ˡ-∘

  Scale-unit : NaturalTransformation.η Scale⟦ s ⟧ unit ≈ s
  Scale-unit = ·ˡ-scalar ○ identityˡ

  -- Scale⟦_⟧ is an injective/faithful monoid homomorphism
  Scale-injective : Scale⟦ s ⟧ ≃ Scale⟦ t ⟧ → s ≈ t
  Scale-injective Scale-s≈t = ⟺ Scale-unit ○ Scale-s≈t ○ Scale-unit

open NaturalAction public