From 09ed1f3eb8e59311ebb1dc47ec53c363c33a3125 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia?= Date: Thu, 10 Aug 2023 07:44:21 -0300 Subject: [PATCH] defn: Allegory of matrices with values in a frame (#248) --- src/1Lab/Type/Pi.lagda.md | 11 +++ src/1Lab/Type/Sigma.lagda.md | 7 ++ src/Cat/Allegory/Instances/Mat.lagda.md | 115 ++++++++++++++++++++++++ src/Order/Frame/Reasoning.lagda.md | 49 ++++++++++ 4 files changed, 182 insertions(+) create mode 100644 src/Cat/Allegory/Instances/Mat.lagda.md diff --git a/src/1Lab/Type/Pi.lagda.md b/src/1Lab/Type/Pi.lagda.md index 72dd0a8bf..76395483b 100644 --- a/src/1Lab/Type/Pi.lagda.md +++ b/src/1Lab/Type/Pi.lagda.md @@ -176,3 +176,14 @@ hetero-homotopy≃homotopy {A = A} {B} {f} {g} = Iso→Equiv isom where j (h (SinglP-is-contr A x₀ .paths (x₁ , p) j .snd)) ``` + + diff --git a/src/1Lab/Type/Sigma.lagda.md b/src/1Lab/Type/Sigma.lagda.md index 8bb2d0df4..03ef364c0 100644 --- a/src/1Lab/Type/Sigma.lagda.md +++ b/src/1Lab/Type/Sigma.lagda.md @@ -279,5 +279,12 @@ infixr 4 _,ₚ_ Σ-swap₂ .snd .is-eqv y = contr (f .fst) (f .snd) where f = strict-fibres _ y -- agda can actually infer the inverse here, which is neat + +×-swap + : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} + → (A × B) ≃ (B × A) +×-swap .fst (x , y) = y , x +×-swap .snd .is-eqv y = contr (f .fst) (f .snd) where + f = strict-fibres _ y ``` --> diff --git a/src/Cat/Allegory/Instances/Mat.lagda.md b/src/Cat/Allegory/Instances/Mat.lagda.md new file mode 100644 index 000000000..41afaf64f --- /dev/null +++ b/src/Cat/Allegory/Instances/Mat.lagda.md @@ -0,0 +1,115 @@ + + +```agda +module Cat.Allegory.Instances.Mat where +``` + +# Frame-valued matrices + +Let $L$ be a [frame]: it could be the frame of opens of a locale, for +example. It turns out that $L$ has enough structure that we can define +an [allegory], where the objects are sets, and the morphisms $A \rel B$ +are given by $A \times B$-matrices valued in $L$. + +[frame]: Order.Frame.html +[allegory]: Cat.Allegory.Base.html + + + +The identity matrix has an entry $\top$ at position $(i, j)$ iff $i = +j$, which we can express independently of whether $i = j$ is decidable +by saying that the identity matrix has $(i,j)$th entry $\bigvee_{i = j} +\top$. The composition of $M : B \rel C$ and $N : A \rel B$ has $(a,c)$th +entry given by + +$$ +\bigvee_{b : B} N(a,b) \wedge M(b,c) \text{,} +$$ + +which is easily seen to be an analogue of the $\sum_{b = 0}^{B} +N(a,b)M(b,c)$ 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: + +```agda + 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 = funext² λ i j → + ⋃ (λ k → ⋃ (λ _ → top) ∩ M k j) ≡⟨ ⋃-apᶠ (λ k → ∩-commutative ∙ ⋃-distrib _ _) ⟩ + ⋃ (λ k → ⋃ (λ _ → M k j ∩ top)) ≡⟨ ⋃-apᶠ (λ k → ap ⋃ (funext λ i → ∩-idr)) ⟩ + ⋃ (λ k → ⋃ (λ _ → M k j)) ≡⟨ ⋃-twice _ ⟩ + ⋃ (λ (k , _) → M k j) ≡⟨ ⋃-singleton (contr _ Singleton-is-contr) ⟩ + M i j ∎ + Mat .idl M = funext² λ i j → + ⋃ (λ k → M i k ∩ ⋃ (λ _ → top)) ≡⟨ ⋃-apᶠ (λ k → ⋃-distrib _ _) ⟩ + ⋃ (λ 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 = funext² λ i j → + ⋃ (λ k → ⋃ (λ l → O i l ∩ N l k) ∩ M k j) ≡⟨ ⋃-apᶠ (λ k → ⋃-distribʳ) ⟩ + ⋃ (λ 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 ⋃ (funext λ k → sym (⋃-distrib _ _)) ⟩ + ⋃ (λ 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 [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: + +[semilattices]: Order.Semilattice.html + +```agda + 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 = funext² λ 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-∘ = funext² λ i j → ⋃-apᶠ λ k → ∩-commutative + + 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 = ∩-univ _ (p i j) (q i j) + + Matrices .A.modular f g h i j = + ⋃ (λ k → f i k ∩ g k j) ∩ h i j =⟨ ⋃-distribʳ ∙ ⋃-apᶠ (λ _ → sym ∩-assoc) ⟩ + ⋃ (λ k → f i k ∩ (g k j ∩ h i j)) =⟨ ⋃-apᶠ (λ k → ap₂ _∩_ refl ∩-commutative) ⟩ + ⋃ (λ k → f i k ∩ (h i j ∩ g k j)) ≤⟨ ⋃≤⋃ (λ i → ∩-univ _ (∩-univ _ ∩≤l (≤-trans ∩≤r (⋃-colimiting _ _))) (≤-trans ∩≤r ∩≤r)) ⟩ + ⋃ (λ k → (f i k ∩ ⋃ (λ l → h i l ∩ g k l)) ∩ g k j) ≤∎ +``` diff --git a/src/Order/Frame/Reasoning.lagda.md b/src/Order/Frame/Reasoning.lagda.md index 0c852c5bc..1bb1f6cc0 100644 --- a/src/Order/Frame/Reasoning.lagda.md +++ b/src/Order/Frame/Reasoning.lagda.md @@ -3,6 +3,7 @@ open import Cat.Prelude open import Order.Diagram.Lub +open import Order.Diagram.Glb open import Order.Semilattice open import Order.Frame open import Order.Base @@ -74,4 +75,52 @@ But this result relies on the cocontinuity of meets. ⋃ (λ i → ⋃ F ∩ G i) ≡⟨ ap ⋃ (funext λ i → ∩-commutative ∙ ⋃-distrib (G i) F) ⟩ ⋃ (λ i → ⋃ λ j → G i ∩ F j) ≡⟨ ⋃-product F G ⟩ ⋃ (λ i → F (i .fst) ∩ G (i .snd)) ∎ + +⋃-twice + : ∀ {I : Type ℓ} {J : I → Type ℓ} (F : (i : I) → J i → ⌞ B ⌟) + → ⋃ (λ i → ⋃ λ j → F i j) + ≡ ⋃ {I = Σ I J} (λ p → F (p .fst) (p .snd)) +⋃-twice F = ≤-antisym + (⋃-universal _ (λ i → ⋃-universal _ (λ j → ⋃-colimiting _ _))) + (⋃-universal _ λ (i , j) → ≤-trans (⋃-colimiting j _) (⋃-colimiting i _)) + +⋃-ap + : ∀ {I I′ : Type ℓ} {f : I → ⌞ B ⌟} {g : I′ → ⌞ B ⌟} + → (e : I ≃ I′) + → (∀ i → f i ≡ g (e .fst i)) + → ⋃ f ≡ ⋃ g +⋃-ap e p = ap₂ (λ I f → ⋃ {I = I} f) (ua e) (ua→ p) + +-- raised i for "index", raised f for "family" +⋃-apⁱ : ∀ {I I′ : Type ℓ} {f : I′ → ⌞ B ⌟} (e : I ≃ I′) → ⋃ (λ i → f (e .fst i)) ≡ ⋃ f +⋃-apᶠ : ∀ {I : Type ℓ} {f g : I → ⌞ B ⌟} → (∀ i → f i ≡ g i) → ⋃ f ≡ ⋃ g + +⋃-apⁱ e = ⋃-ap e (λ i → refl) +⋃-apᶠ p = ⋃-ap (_ , id-equiv) p + +⋃-singleton + : ∀ {I : Type ℓ} {f : I → ⌞ B ⌟} + → (p : is-contr I) + → ⋃ f ≡ f (p .centre) +⋃-singleton {f = f} p = ≤-antisym + (⋃-universal _ (λ i → sym ∩-idempotent ∙ ap₂ _∩_ refl (ap f (sym (p .paths _))))) + (⋃-colimiting _ _) + +⋃-distribʳ + : ∀ {I : Type ℓ} {f : I → ⌞ B ⌟} {x} + → ⋃ f ∩ x ≡ ⋃ (λ i → f i ∩ x) +⋃-distribʳ = ∩-commutative ∙ ⋃-distrib _ _ ∙ ap ⋃ (funext λ _ → ∩-commutative) + +⋃≤⋃ + : ∀ {I : Type ℓ} {f g : I → ⌞ B ⌟} + → (∀ i → f i ≤ g i) + → ⋃ f ≤ ⋃ g +⋃≤⋃ p = ⋃-universal _ (λ i → ≤-trans (p i) (⋃-colimiting _ _)) + +∩≤∩ + : ∀ {x y x' y'} + → x ≤ x' + → y ≤ y' + → (x ∩ y) ≤ (x' ∩ y') +∩≤∩ p q = ∩-univ _ (≤-trans ∩≤l p) (≤-trans ∩≤r q) ```