module Cat.Allegory.Instances.Mat where

Frame-valued matricesπŸ”—

Let be a frame: it could be the frame of opens of a locale, for example. It turns out that has enough structure that we can define an allegory, where the objects are sets, and the morphisms are given by valued in

The identity matrix has an entry at position iff which we can express independently of whether is decidable by saying that the identity matrix has entry The composition of and has entry given by

which is easily seen to be an analogue of the which implements composition when matrices take values in a ring. The infinite distributive law is applied frequently to establish that this is, indeed, a category:

  Mat : Precategory (lsuc o) o
  Mat .Ob          = Set o
  Mat .Hom A B     = ∣ A ∣ β†’ ∣ B ∣ β†’ ⌞ L ⌟
  Mat .Hom-set x y = hlevel!

  Mat .id x y              = ⋃ Ξ» (_ : x ≑ y) β†’ top
  Mat ._∘_ {y = y} M N i j = ⋃ Ξ» k β†’ N i k ∩ M k j

  Mat .idr M = ext Ξ» i j β†’
    ⋃ (Ξ» k β†’ ⋃ (Ξ» _ β†’ top) ∩ M k j) β‰‘βŸ¨ ⋃-apαΆ  (Ξ» k β†’ ∩-comm βˆ™ ⋃-distribl _ _) βŸ©β‰‘
    ⋃ (Ξ» k β†’ ⋃ (Ξ» _ β†’ M k j ∩ top)) β‰‘βŸ¨ ⋃-apαΆ  (Ξ» k β†’ ⋃-apαΆ  Ξ» i β†’ ∩-idr) βŸ©β‰‘
    ⋃ (Ξ» k β†’ ⋃ (Ξ» _ β†’ M k j))       β‰‘βŸ¨ ⋃-twice _ βŸ©β‰‘
    ⋃ (Ξ» (k , _) β†’ M k j)           β‰‘βŸ¨ ⋃-singleton (contr _ Singleton-is-contr) βŸ©β‰‘
    M i j                           ∎
  Mat .idl M = ext Ξ» i j β†’
    ⋃ (Ξ» k β†’ M i k ∩ ⋃ (Ξ» _ β†’ top)) β‰‘βŸ¨ ⋃-apαΆ  (Ξ» k β†’ ⋃-distribl _ _) βŸ©β‰‘
    ⋃ (Ξ» k β†’ ⋃ (Ξ» _ β†’ M i k ∩ top)) β‰‘βŸ¨ ⋃-apαΆ  (Ξ» k β†’ ⋃-apαΆ  Ξ» j β†’ ∩-idr) βŸ©β‰‘
    ⋃ (Ξ» x β†’ ⋃ (Ξ» _ β†’ M i x))       β‰‘βŸ¨ ⋃-twice _ βŸ©β‰‘
    ⋃ (Ξ» (k , _) β†’ M i k)           β‰‘βŸ¨ ⋃-singleton (contr _ (Ξ» p i β†’ p .snd (~ i) , Ξ» j β†’ p .snd (~ i ∨ j))) βŸ©β‰‘
    M i j                           ∎

  Mat .assoc M N O = ext Ξ» i j β†’
    ⋃ (Ξ» k β†’ ⋃ (Ξ» l β†’ O i l ∩ N l k) ∩ M k j)   β‰‘βŸ¨ ⋃-apαΆ  (Ξ» k β†’ ⋃-distribr _ _) βŸ©β‰‘
    ⋃ (Ξ» k β†’ ⋃ (Ξ» l β†’ (O i l ∩ N l k) ∩ M k j)) β‰‘βŸ¨ ⋃-twice _ βŸ©β‰‘
    ⋃ (Ξ» (k , l) β†’ (O i l ∩ N l k) ∩ M k j)     β‰‘βŸ¨ ⋃-apαΆ  (Ξ» _ β†’ sym ∩-assoc) βŸ©β‰‘
    ⋃ (Ξ» (k , l) β†’ O i l ∩ (N l k ∩ M k j))     β‰‘βŸ¨ ⋃-apⁱ Γ—-swap βŸ©β‰‘
    ⋃ (Ξ» (l , k) β†’ O i l ∩ (N l k ∩ M k j))     β‰‘Λ˜βŸ¨ ⋃-twice _ βŸ©β‰‘Λ˜
    ⋃ (Ξ» l β†’ ⋃ (Ξ» k β†’ O i l ∩ (N l k ∩ M k j))) β‰‘βŸ¨ ⋃-apαΆ  (Ξ» k β†’ sym (⋃-distribl _ _)) βŸ©β‰‘
    ⋃ (Ξ» l β†’ O i l ∩ ⋃ (Ξ» k β†’ N l k ∩ M k j))   ∎

Most of the structure of an allegory now follows directly from the fact that frames are also meet semilattices: the ordering, duals, and intersections are all computed pointwise. The only thing which requires a bit more algebra is the verification of the modular law:

  Matrices : Allegory (lsuc o) o (o βŠ” β„“)
  Matrices .A.cat = Mat
  Matrices .A._≀_ M N = βˆ€ i j β†’ M i j ≀ N i j

  Matrices .A.≀-thin          = hlevel!
  Matrices .A.≀-refl i j      = ≀-refl
  Matrices .A.≀-trans p q i j = ≀-trans (p i j) (q i j)
  Matrices .A.≀-antisym p q   = ext Ξ» i j β†’ ≀-antisym (p i j) (q i j)
  Matrices .A._β—†_ p q i j     = ⋃≀⋃ (Ξ» k β†’ βˆ©β‰€βˆ© (q i k) (p k j))

  Matrices .A._† M i j     = M j i
  Matrices .A.dual-≀ x i j = x j i
  Matrices .A.dual M       = refl
  Matrices .A.dual-∘       = ext Ξ» i j β†’ ⋃-apαΆ  Ξ» k β†’ ∩-comm

  Matrices .A._∩_ M N i j    = M i j ∩ N i j
  Matrices .A.∩-le-l i j     = βˆ©β‰€l
  Matrices .A.∩-le-r i j     = βˆ©β‰€r
  Matrices .A.∩-univ p q i j = ∩-universal _ (p i j) (q i j)

  Matrices .A.modular f g h i j =
    ⋃ (Ξ» k β†’ f i k ∩ g k j) ∩ h i j                     =⟨ ⋃-distribr _ _ βˆ™ ⋃-apαΆ  (Ξ» _ β†’ sym ∩-assoc) ⟩=
    ⋃ (Ξ» k β†’ f i k ∩ (g k j ∩ h i j))                   =⟨ ⋃-apαΆ  (Ξ» k β†’ apβ‚‚ _∩_ refl ∩-comm) ⟩=
    ⋃ (Ξ» k β†’ f i k ∩ h i j ∩ g k j)                     β‰€βŸ¨ ⋃≀⋃ (Ξ» i β†’ ∩-universal _ (βˆ©β‰€βˆ©r (⋃-inj j)) (≀-trans βˆ©β‰€r βˆ©β‰€r)) βŸ©β‰€
    ⋃ (Ξ» k β†’ (f i k ∩ ⋃ (Ξ» l β†’ h i l ∩ g k l)) ∩ g k j) β‰€βˆŽ