Idempotent systems

IdempotentSystem.lagda.md

description
Idempotent systems.

open import Cat.Diagram.Monad
open import Cat.Prelude

import Cat.Reasoning
import Cat.Functor.Reasoning
import Cat.Diagram.Idempotent

module Cat.Morphism.Idempotent.System where

Idempotent systems

Let $C$ be a category, $F : C \to C$ be an endofunctor, and $e_{A} : C(F(A), F(A))$ be a family of morphisms in $C$. We say that $e_{A}$ is an idempotent system if for all $f : C(A,B)$, $e_{B} \circ F(f) \circ e_{A} = e_{B} \circ F(f)$.

module _ {o ℓ} {C : Precategory o ℓ} (F : Functor C C) where
  private
    open Cat.Reasoning C
    open Cat.Diagram.Idempotent C
    open Functor F
    module F = Cat.Functor.Reasoning

  is-idempotent-system : (∀ (a : Ob) → Hom (F₀ a) (F₀ a)) → Type _
  is-idempotent-system e = ∀ {a b} (f : Hom a b) → e b ∘ F₁ f ∘ e a ≡ e b ∘ F₁ f

  record Idempotent-system : Type (o ⊔ ℓ) where
    no-eta-equality
    field
      η        : ∀ a → Hom (F₀ a) (F₀ a)
      idem-sys : is-idempotent-system η

Note that every component of an idempotent system is idempotent.

  is-idempotent-system→is-idempotent
    : {e : ∀ (a : Ob) → Hom (F₀ a) (F₀ a)}
    → is-idempotent-system e
    → ∀ a → is-idempotent (e a)
  is-idempotent-system→is-idempotent {e = e} nat-idem a =
    e a ∘ e a         ≡⟨ refl⟩∘⟨ introl F-id ⟩
    e a ∘ F₁ id ∘ e a ≡⟨ nat-idem id ⟩
    e a ∘ F₁ id       ≡⟨ elimr F-id ⟩
    e a               ∎

An idempotent system is split if every component of the family is a split idempotent.

  record Split-idempotent-system : Type (o ⊔ ℓ) where
    field
      S : Ob → Ob
      ηₛ : ∀ a → Hom (S a) (F₀ a)
      ηᵣ : ∀ a → Hom (F₀ a) (S a)
      retracts : ∀ a → ηᵣ a retract-of ηₛ a

    ηₛ-has-retract : ∀ a → has-retract (ηₛ a)
    ηₛ-has-retract a = make-retract (ηᵣ a) (retracts a)

    ηᵣ-has-section : ∀ a → has-section (ηᵣ a)
    ηᵣ-has-section a = make-section (ηₛ a) (retracts a)

    field
      idem-sys : is-idempotent-system (λ a → ηₛ a ∘ ηᵣ a)

    ηᵣ-sys
      : ∀ {a b} (f : Hom a b)
      → ηᵣ b ∘ F₁ f ∘ (ηₛ a ∘ ηᵣ a) ≡ ηᵣ b ∘ F₁ f
    ηᵣ-sys f = has-retract→monic (ηₛ-has-retract _) _ _ $
      ηₛ _ ∘ ηᵣ _ ∘ F₁ f ∘ ηₛ _ ∘ ηᵣ _   ≡⟨ assoc _ _ _ ⟩
      (ηₛ _ ∘ ηᵣ _) ∘ F₁ f ∘ ηₛ _ ∘ ηᵣ _ ≡⟨ idem-sys f ⟩
      (ηₛ _ ∘ ηᵣ _) ∘ F₁ f               ≡˘⟨ assoc _ _ _ ⟩
      ηₛ _ ∘ ηᵣ _ ∘ F₁ f                 ∎

    system : Idempotent-system
    system .Idempotent-system.η a = ηₛ a ∘ ηᵣ a
    system .Idempotent-system.idem-sys = idem-sys

The existence of a split idempotent system induces a new endofunctor on $C$, which we call the idempotent restriction of $F$.

  module _ (e : Split-idempotent-system) where
    open Split-idempotent-system e

    Idem : Functor C C
    Idem .Functor.F₀ = S 
    Idem .Functor.F₁ f = ηᵣ _ ∘ F₁ f ∘ ηₛ _
    Idem .Functor.F-id =
      ηᵣ _ ∘ F₁ id ∘ ηₛ _ ≡⟨ refl⟩∘⟨ eliml F-id ⟩
      ηᵣ _ ∘ ηₛ _         ≡⟨ retracts _ ⟩
      id ∎
    Idem .Functor.F-∘ f g =
      ηᵣ _ ∘ F₁ (f ∘ g) ∘ ηₛ _                    ≡⟨ extendl (pushr (F-∘ _ _)) ⟩
      (ηᵣ _ ∘ F₁ f) ∘ (F₁ g ∘ ηₛ _)               ≡⟨ pushl (sym (ηᵣ-sys f) ∙ pushr (assoc _ _ _)) ⟩
      (ηᵣ _ ∘ F₁ f ∘ ηₛ _) ∘ (ηᵣ _ ∘ F₁ g ∘ ηₛ _) ∎

Monadic Idempotent Systems

Let $e$ be an idempotent system on a monad $(M, \eta, \mu)$. We say that $e$ is monadic if:

• $e_{A} \circ \eta_{A} = \eta_{A}$, and
• $e_{A} \circ \mu_{A} \circ M(e_{A}) = e_{A} \circ \mu_A$, and
• $e_{A} \circ \mu_{A} \circ e_{M(A)} = e_{A} \circ \mu_A$

module _
  {o ℓ} {C : Precategory o ℓ}
  (monad : Monad C)
  where
  open Cat.Reasoning C
  open Monad monad
  open _=>_

  record is-monadic-idempotent-system (e : Idempotent-system M) : Type (o ⊔ ℓ) where
    no-eta-equality
    private
      module e = Idempotent-system e
    field
      unit-sys : ∀ a → e.η a ∘ unit.η a ≡ unit.η a
      mult-sys-inner : ∀ a → e.η a ∘ mult.η a ∘ M₁ (e.η a) ≡ e.η a ∘ mult.η a
      mult-sys-outer : ∀ a → e.η a ∘ mult.η a ∘ e.η (M₀ a) ≡ e.η a ∘ mult.η a

A split idempotent system is split monadic if it is monadic, and comes equipped with the following interchange law for every section/rectraction pair $(s_{a}, r_{a})$:

• $M(s_a) \circ s_{S(a)} \circ r_{S(a)} \circ M(r_{a}) = s_{M(a)} \circ r_{M(a)} \circ M(s_{a}) \circ M(r_{a})$

  record is-split-monadic-idempotent-system (e : Split-idempotent-system M) : Type (o ⊔ ℓ) where
    no-eta-equality
    open Split-idempotent-system e
    field
      is-monadic : is-monadic-idempotent-system system

    open is-monadic-idempotent-system is-monadic public
    field
      interchange : ∀ a → (M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ (ηᵣ (S a) ∘ M₁ (ηᵣ a)) ≡ (ηₛ (M₀ a) ∘ ηᵣ (M₀ a)) ∘ M₁ (ηₛ a ∘ ηᵣ a)

    ηᵣ-mult-inner : ∀ a → ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ _ ∘ ηᵣ _) ≡ ηᵣ a ∘ mult.η a
    ηᵣ-mult-inner a = has-retract→monic (ηₛ-has-retract _) _ _ $
      ηₛ a ∘ ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ a ∘ ηᵣ a)   ≡⟨ assoc _ _ _ ⟩
      (ηₛ a ∘ ηᵣ a) ∘ mult.η a ∘ M₁ (ηₛ a ∘ ηᵣ a) ≡⟨ mult-sys-inner a ⟩
      (ηₛ a ∘ ηᵣ a) ∘ mult.η a                    ≡˘⟨ assoc _ _ _ ⟩
      ηₛ a ∘ ηᵣ a ∘ mult.η a                      ∎

    ηᵣ-mult-outer : ∀ a → ηᵣ a ∘ mult.η a ∘ ηₛ _ ∘ ηᵣ _ ≡ ηᵣ a ∘ mult.η a
    ηᵣ-mult-outer a = has-retract→monic (ηₛ-has-retract _) _ _ $
      ηₛ a ∘ ηᵣ a ∘ mult.η a ∘ ηₛ (M₀ a) ∘ ηᵣ (M₀ a)   ≡⟨ assoc _ _ _ ⟩
      (ηₛ a ∘ ηᵣ a) ∘ mult.η a ∘ ηₛ (M₀ a) ∘ ηᵣ (M₀ a) ≡⟨ mult-sys-outer a ⟩
      (ηₛ a ∘ ηᵣ a) ∘ mult.η a                         ≡˘⟨ assoc _ _ _ ⟩
      ηₛ a ∘ ηᵣ a ∘ mult.η a                           ∎

If $e$ is split monadic, then the idempotent restriction of $M$ along $e$ inherits the monadic structure of $M$. The proof of this is quite brutal though!

  module _
    (e : Split-idempotent-system M)
    (monadic : is-split-monadic-idempotent-system e)
    where
    private
      open Split-idempotent-system e
      open is-split-monadic-idempotent-system monadic
      module M = Cat.Functor.Reasoning M

    Idem-monad : Monad C
    Idem-monad .Monad.M = Idem M e
    Idem-monad .Monad.unit .η a = ηᵣ a ∘ unit.η a
    Idem-monad .Monad.unit .is-natural x y f =
      (ηᵣ y ∘ unit.η y) ∘ f  ≡⟨ pullr (unit.is-natural x y f) ⟩
      ηᵣ y ∘ M₁ f ∘ unit.η x ≡⟨ extendl (sym (ηᵣ-sys f) ∙ pushr (assoc _ _ _)) ⟩
      (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ (ηᵣ x ∘ unit.η x) ∎
    Idem-monad .Monad.mult .η a = ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ a) ∘ ηₛ (S a)
    Idem-monad .Monad.mult .is-natural x y f =
      (ηᵣ y ∘ mult.η y ∘ M₁ (ηₛ y) ∘ ηₛ (S y)) ∘ (ηᵣ (S y) ∘ M₁ (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ ηₛ (S x))             ≡⟨ (refl⟩∘⟨ pushη) ⟩
      (ηᵣ y ∘ mult.η y ∘ M₁ (ηₛ y) ∘ ηₛ (S y)) ∘ ((ηᵣ (S y) ∘ M₁ (ηᵣ y)) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x)) ≡⟨ extendr (extendr (extendl (interchange y))) ⟩
      (ηᵣ y ∘ mult.η y ∘ ηₛ (M₀ y) ∘ ηᵣ (M₀ y)) ∘ (M₁ (ηₛ y ∘ ηᵣ y) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x))      ≡⟨ (ηᵣ-mult-outer _ ⟩∘⟨refl) ⟩
      (ηᵣ y ∘ mult.η y) ∘ (M₁ (ηₛ y ∘ ηᵣ y) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                              ≡⟨ pulll (sym (assoc _ _ _) ∙ ηᵣ-mult-inner _) ⟩
      (ηᵣ y ∘ mult.η y) ∘ (M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                                                 ≡⟨ extendr (extendl (mult.is-natural _ _ _)) ⟩
      (ηᵣ y ∘ M₁ f) ∘ (mult.η x ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                                                      ≡˘⟨ ηᵣ-sys f ⟩∘⟨refl ⟩
      (ηᵣ y ∘ M₁ f ∘ ηₛ x ∘ ηᵣ x) ∘ (mult.η x ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                                        ≡⟨ extendr (extendr (sym (assoc _ _ _))) ⟩
      (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ (ηᵣ x ∘ mult.η x ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                                        ∎
      where
        pushη : ηᵣ (S y) ∘ M₁ (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ ηₛ (S x) ≡ (ηᵣ (S y) ∘ M₁ (ηᵣ y)) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x)
        pushη = pushr $
          M₁ (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ ηₛ (S x)      ≡⟨ pushl (M-∘ _ _) ⟩
          M₁ (ηᵣ y) ∘ M₁ (M₁ f ∘ ηₛ x) ∘ ηₛ (S x) ≡⟨ refl⟩∘⟨ (pushl (M-∘ _ _)) ⟩
          M₁ (ηᵣ y) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x) ∎
    Idem-monad .Monad.left-ident =
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ (ηᵣ _ ∘ M₁ (ηᵣ _ ∘ unit.η _) ∘ ηₛ _)        ≡⟨ refl⟩∘⟨ (pushr (pushl (M-∘ _ _))) ⟩
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ ((ηᵣ _ ∘ M₁ (ηᵣ _)) ∘ M₁ (unit.η _) ∘ ηₛ _) ≡⟨ extendr (extendr (extendl (interchange _))) ⟩
      (ηᵣ _ ∘ mult.η _ ∘ (ηₛ _ ∘ ηᵣ _)) ∘ (M₁ (ηₛ _ ∘ ηᵣ _) ∘ M₁ (unit.η _) ∘ ηₛ _)      ≡⟨ ap₂ _∘_ (ηᵣ-mult-outer _) (M.pulll (unit-sys _)) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (M₁ (unit.η _) ∘ ηₛ _)                                         ≡⟨ cancel-inner left-ident ⟩
      ηᵣ _ ∘ ηₛ _                                                                        ≡⟨ retracts _ ⟩
      id                                                                                 ∎
    Idem-monad .Monad.right-ident =
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ (ηᵣ _ ∘ unit.η _) ≡⟨ extendr (extendr (pullr (assoc _ _ _ ∙ unit-sys _))) ⟩
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _)) ∘ unit.η _                 ≡⟨ extendr (pullr (sym (unit .is-natural _ _ _))) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (unit.η _ ∘ ηₛ _)                    ≡⟨ cancel-inner right-ident ⟩
      ηᵣ _ ∘ ηₛ _                                              ≡⟨ retracts _ ⟩
      id                                                       ∎
    Idem-monad .Monad.mult-assoc =
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ (ηᵣ _ ∘ M₁ (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ ηₛ _)                  ≡⟨ refl⟩∘⟨ pushη ⟩
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ ((ηᵣ _ ∘ M₁ (ηᵣ _)) ∘ M₁ (mult.η _) ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _) ≡⟨ extendr (extendr (extendl (interchange _))) ⟩
      (ηᵣ _ ∘ mult.η _ ∘ ηₛ _ ∘ ηᵣ _) ∘ (M₁ (ηₛ _ ∘ ηᵣ _) ∘ M₁ (mult.η _) ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _)        ≡⟨ ap₂ _∘_ (ηᵣ-mult-outer _) refl ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (M₁ (ηₛ _ ∘ ηᵣ _) ∘ M₁ (mult.η _) ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _)                      ≡⟨ pulll (sym (assoc _ _ _ ) ∙ ηᵣ-mult-inner _) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (M₁ (mult.η _) ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _)                                         ≡⟨ extendr (extendl mult-assoc) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (mult.η _ ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _)                                              ≡⟨ (refl⟩∘⟨ extendl (mult.is-natural _ _ _)) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (M₁ (ηₛ _) ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                                                   ≡⟨ pushl (sym (ηᵣ-mult-outer _) ∙ assoc _ _ _) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (ηₛ _ ∘ ηᵣ _) ∘ (M₁ (ηₛ _) ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                                   ≡⟨ (refl⟩∘⟨ extendl (sym (idem-sys _))) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (ηₛ _ ∘ ηᵣ _) ∘ ((M₁ (ηₛ _) ∘ ηₛ _ ∘ ηᵣ _) ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                   ≡⟨ pulll (sym (assoc _ _ _) ∙ ηᵣ-mult-outer _) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ ((M₁ (ηₛ _) ∘ ηₛ _ ∘ ηᵣ _) ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                                   ≡⟨ cat! C ⟩
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                                     ∎
      where
        pushη
          : ∀ {a}
          → ηᵣ (S a) ∘ M₁ (ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ ηₛ (S (S a))
          ≡ (ηᵣ (S a) ∘ M₁ (ηᵣ a)) ∘ M₁ (mult.η a) ∘ M₁ (M₁ (ηₛ a)) ∘ M₁ (ηₛ (S a)) ∘ ηₛ (S (S a))
        pushη {a = a} = pushr $
          M₁ (ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ ηₛ (S (S a))                ≡⟨ pushl (M-∘ _ _) ⟩
          M₁ (ηᵣ a) ∘ M₁ (mult.η a ∘ M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ ηₛ (S (S a))           ≡⟨ (refl⟩∘⟨ pushl (M-∘ _ _)) ⟩
          (M₁ (ηᵣ a) ∘ M₁ (mult.η a) ∘ M₁ (M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ ηₛ (S (S a)))    ≡⟨ (refl⟩∘⟨ (refl⟩∘⟨ pushl (M-∘ _ _))) ⟩
          M₁ (ηᵣ a) ∘ M₁ (mult.η a) ∘ M₁ (M₁ (ηₛ a)) ∘ M₁ (ηₛ (S a)) ∘ ηₛ (S (S a)) ∎

Examples

Clearly, both sorting and deduplicating give rise to split idempotent systems. Moreover, they are both split monadic.

Notes

It feels like the interchange law should come from somewhere else?

Interesting!