Split idempotent

open import category-theory.category

module category-theory.split-idempotent {o h} (𝒞 : Category o h) where

open import foundations.universe
open import foundations.identity-type
open import foundations.identity-type-reasoning
open import foundations.groupoid-laws
open import foundations.functions-are-functors
open import foundations.sigma-type
open import foundations.product-type
open import category-theory.idempotent-morphism 𝒞
open import category-theory.isomorphism 𝒞
open Category 𝒞

private variable A : Ob

record isSplitIdempotent (f : Hom A A) : Type (o ⊔ h) where
  field
    B : Ob
    s : Hom B A
    r : Hom A B
    sr＝f : s ∘ r ＝ f
    rs＝id : r ∘ s ＝ id B

private variable f : Hom A A

上記の定義はfが冪等射であることを含意する。

isSplitIdempotent⇒isIdempotent : isSplitIdempotent f → isIdempotent f
isSplitIdempotent⇒isIdempotent {f = f} S =
    f ∘ f
  ＝⟨ ap (_∘ f) (sym sr＝f) ⟩
    (s ∘ r) ∘ f
  ＝⟨ ap ((s ∘ r) ∘_) (sym sr＝f) ⟩
    (s ∘ r) ∘ (s ∘ r)
  ＝⟨ assoc ⟩
    s ∘ (r ∘ (s ∘ r))
  ＝⟨ ap (s ∘_) (sym assoc) ⟩
    s ∘ ((r ∘ s) ∘ r)
  ＝⟨ ap (λ w → s ∘ (w ∘ r)) rs＝id ⟩
    s ∘ (id B ∘ r)
  ＝⟨ ap (s ∘_) (identˡ r) ⟩
    s ∘ r
  ＝⟨ sr＝f ⟩
    f
  ∎
  where open isSplitIdempotent S

Splittingは同型を除いて一意である。

module UniquenessOfSplitting {f : Hom A A} (S T : isSplitIdempotent f) where
  private
    module S = isSplitIdempotent S
    module T = isSplitIdempotent T

  i : Hom S.B T.B
  i = T.r ∘ S.s

  iso : isIso i
  iso = record
    { g = S.r ∘ T.s
    ; invˡ =
        (S.r ∘ T.s) ∘ (T.r ∘ S.s)
      ＝⟨ assoc ⟩
        S.r ∘ (T.s ∘ (T.r ∘ S.s))
      ＝⟨ ap (S.r ∘_) (sym assoc) ⟩
        S.r ∘ ((T.s ∘ T.r) ∘ S.s)
      ＝⟨ ap (λ w → S.r ∘ (w ∘ S.s)) T.sr＝f ⟩
        S.r ∘ (f ∘ S.s)
      ＝⟨ ap (λ w → S.r ∘ (w ∘ S.s)) (sym S.sr＝f) ⟩
        S.r ∘ ((S.s ∘ S.r) ∘ S.s)
      ＝⟨ ap (S.r ∘_) assoc ⟩
        S.r ∘ (S.s ∘ (S.r ∘ S.s))
      ＝⟨ ap (λ w → S.r ∘ (S.s ∘ w)) S.rs＝id ⟩
        S.r ∘ (S.s ∘ id S.B)
      ＝⟨ ap (S.r ∘_) (identʳ _) ⟩
        S.r ∘ S.s
      ＝⟨ S.rs＝id ⟩
        id S.B
      ∎
    ; invʳ =
        (T.r ∘ S.s) ∘ (S.r ∘ T.s)
      ＝⟨ assoc ⟩
        T.r ∘ (S.s ∘ (S.r ∘ T.s))
      ＝⟨ ap (T.r ∘_) (sym assoc) ⟩
        T.r ∘ ((S.s ∘ S.r) ∘ T.s)
      ＝⟨ ap (λ w → T.r ∘ (w ∘ T.s)) S.sr＝f ⟩
        T.r ∘ (f ∘ T.s)
      ＝⟨ ap (λ w → T.r ∘ (w ∘ T.s)) (sym T.sr＝f) ⟩
        T.r ∘ ((T.s ∘ T.r) ∘ T.s)
      ＝⟨ ap (T.r ∘_) assoc ⟩
        T.r ∘ (T.s ∘ (T.r ∘ T.s))
      ＝⟨ ap (λ w → T.r ∘ (T.s ∘ w)) T.rs＝id ⟩
        T.r ∘ (T.s ∘ id T.B)
      ＝⟨ ap (T.r ∘_) (identʳ _) ⟩
        T.r ∘ T.s
      ＝⟨ T.rs＝id ⟩
        id T.B
      ∎
    }

  module iso = isIso iso

  ps : S.s ∘ iso.g ＝ T.s
  ps =
      S.s ∘ iso.g
    ＝⟨ sym assoc ⟩
      (S.s ∘ S.r) ∘ T.s
    ＝⟨ ap (_∘ T.s) S.sr＝f ⟩
      f ∘ T.s
    ＝⟨ ap (_∘ T.s) (sym T.sr＝f) ⟩
      (T.s ∘ T.r) ∘ T.s
    ＝⟨ assoc ⟩
      T.s ∘ (T.r ∘ T.s)
    ＝⟨ ap (T.s ∘_) T.rs＝id ⟩
      T.s ∘ id T.B
    ＝⟨ identʳ _ ⟩
      T.s
    ∎

  pr : i ∘ S.r ＝ T.r
  pr =
      i ∘ S.r
    ＝⟨ assoc ⟩
      T.r ∘ (S.s ∘ S.r)
    ＝⟨ ap (T.r ∘_) S.sr＝f ⟩
      T.r ∘ f
    ＝⟨ ap (T.r ∘_) (sym T.sr＝f) ⟩
      T.r ∘ (T.s ∘ T.r)
    ＝⟨ sym assoc ⟩
      (T.r ∘ T.s) ∘ T.r
    ＝⟨ ap (_∘ T.r) T.rs＝id ⟩
      id T.B ∘ T.r
    ＝⟨ identˡ _ ⟩
      T.r
    ∎

以上より、univalent categoryにおいてはisSplitIdempotentが命題であるということが示せる。(この証明はいずれ書きます。)