open import Cat.Allegory.Base
open import Cat.Prelude

open import Order.Frame
open import Order.Base

import Order.Frame.Reasoning

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

module _ {o β : Level} (L : Frame o β) where
open Order.Frame.Reasoning (L .snd)
open Precategory
private module A = Allegory


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 2

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 1
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