Open subschemes

Cubical/Algebra/DistLattice/BigOps.agda

@@ -1,5 +1,5 @@
--- define ⋁ and ⋀ as the bigOps of a Ring when interpreted
--- as an additive/multiplicative monoid
+-- define ⋁ and ⋀ as the bigOps of a DistLattice when interpreted
+-- as a join/meet semilattice
 
 {-# OPTIONS --safe #-}
 module Cubical.Algebra.DistLattice.BigOps where
@@ -34,7 +34,7 @@ open import Cubical.Relation.Binary.Order.Poset
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' : Level
 
 module KroneckerDelta (L' : DistLattice ℓ) where
  private
@@ -107,6 +107,15 @@ module Join (L' : DistLattice ℓ) where
  ≤-⋁Ext = ≤-bigOpExt
 
 
+module JoinMap {L : DistLattice ℓ} {L' : DistLattice ℓ'} (φ : DistLatticeHom L L') where
+  private module L = Join L
+  private module L' = Join L'
+  open BigOpMap (LatticeHom→JoinSemilatticeHom φ)
+
+  pres⋁ : {n : ℕ} (U : FinVec ⟨ L ⟩ n) → φ .fst (L.⋁ U) ≡ L'.⋁ (φ .fst ∘ U)
+  pres⋁ = presBigOp
+
+
 module Meet (L' : DistLattice ℓ) where
  private
   L = fst L'

Cubical/Algebra/DistLattice/Downset.agda

@@ -0,0 +1,70 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.DistLattice.Downset where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Powerset
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Algebra.Semigroup
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.CommMonoid
+open import Cubical.Algebra.Semilattice
+open import Cubical.Algebra.Lattice
+open import Cubical.Algebra.DistLattice.Base
+
+open import Cubical.Relation.Binary.Order.Poset
+
+open Iso
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module DistLatticeDownset (L' : DistLattice ℓ) where
+
+  open DistLatticeStr ⦃...⦄
+  open PosetStr ⦃...⦄ hiding (is-set)
+  open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L'))
+  open MeetSemilattice (Lattice→MeetSemilattice (DistLattice→Lattice L')) hiding (_≤_ ; IndPoset)
+  open LatticeTheory (DistLattice→Lattice L')
+  open Order (DistLattice→Lattice L')
+  open IsLatticeHom
+
+  -- importing other downset related stuff
+  open PosetDownset IndPoset public
+
+  private
+    L = L' .fst
+    LPoset = IndPoset
+    instance
+      _ = L' .snd
+      _ = LPoset .snd
+
+  ↓ᴰᴸ : L → DistLattice ℓ
+  fst (↓ᴰᴸ u) = ↓ u
+  DistLatticeStr.0l (snd (↓ᴰᴸ u)) = 0l , ∨lLid u
+  DistLatticeStr.1l (snd (↓ᴰᴸ u)) = u , is-refl u
+  DistLatticeStr._∨l_ (snd (↓ᴰᴸ u)) (v , v≤u) (w , w≤u) =
+    v ∨l w , ∨lIsMax _ _ _ v≤u w≤u
+  DistLatticeStr._∧l_ (snd (↓ᴰᴸ u)) (v , v≤u) (w , _) =
+    v ∧l w , is-trans _ _ _ (≤m→≤j _ _ (∧≤RCancel _ _)) v≤u
+  DistLatticeStr.isDistLattice (snd (↓ᴰᴸ u)) = makeIsDistLattice∧lOver∨l
+    (isSetΣSndProp is-set λ _ → is-prop-valued _ _)
+    (λ _ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∨lAssoc _ _ _))
+    (λ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∨lRid _))
+    (λ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∨lComm _ _))
+    (λ _ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∧lAssoc _ _ _))
+    (λ (_ , v≤u) → Σ≡Prop (λ _ → is-prop-valued _ _) (≤j→≤m _ _ v≤u))
+    (λ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∧lComm _ _))
+    (λ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∧lAbsorb∨l _ _))
+    (λ _ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∧lLdist∨l _ _ _))
+
+  toDownHom : (u : L) → DistLatticeHom L' (↓ᴰᴸ u)
+  fst (toDownHom u) w = (u ∧l w) , ≤m→≤j _ _ (∧≤RCancel _ _)
+  pres0 (snd (toDownHom u)) = Σ≡Prop (λ _ → is-prop-valued _ _) (0lRightAnnihilates∧l _)
+  pres1 (snd (toDownHom u)) = Σ≡Prop (λ _ → is-prop-valued _ _) (∧lRid _)
+  pres∨l (snd (toDownHom u)) v w = Σ≡Prop (λ _ → is-prop-valued _ _) (∧lLdist∨l _ _ _)
+  pres∧l (snd (toDownHom u)) v w = Σ≡Prop (λ _ → is-prop-valued _ _) (∧lLdist∧l u v w)

Cubical/Algebra/Lattice/Base.agda

@@ -231,5 +231,19 @@ LatticePath = ∫ 𝒮ᴰ-Lattice .UARel.ua
 Lattice→JoinSemilattice : Lattice ℓ → Semilattice ℓ
 Lattice→JoinSemilattice (A , latticestr _ _ _ _ L) = semilattice _ _ _ (L .IsLattice.joinSemilattice )
 
+LatticeHom→JoinSemilatticeHom : {L : Lattice ℓ} {L' : Lattice ℓ'}
+   → LatticeHom L L'
+   → SemilatticeHom (Lattice→JoinSemilattice L) (Lattice→JoinSemilattice L')
+fst (LatticeHom→JoinSemilatticeHom φ) = fst φ
+IsMonoidHom.presε (snd (LatticeHom→JoinSemilatticeHom φ)) = φ .snd .IsLatticeHom.pres0
+IsMonoidHom.pres· (snd (LatticeHom→JoinSemilatticeHom φ)) = φ .snd .IsLatticeHom.pres∨l
+
 Lattice→MeetSemilattice : Lattice ℓ → Semilattice ℓ
 Lattice→MeetSemilattice (A , latticestr _ _ _ _ L) = semilattice _ _ _ (L .IsLattice.meetSemilattice )
+
+LatticeHom→MeetSemilatticeHom : {L : Lattice ℓ} {L' : Lattice ℓ'}
+   → LatticeHom L L'
+   → SemilatticeHom (Lattice→MeetSemilattice L) (Lattice→MeetSemilattice L')
+fst (LatticeHom→MeetSemilatticeHom φ) = fst φ
+IsMonoidHom.presε (snd (LatticeHom→MeetSemilatticeHom φ)) = φ .snd .IsLatticeHom.pres1
+IsMonoidHom.pres· (snd (LatticeHom→MeetSemilatticeHom φ)) = φ .snd .IsLatticeHom.pres∧l

Cubical/Algebra/Lattice/Properties.agda

@@ -29,24 +29,41 @@ private
     ℓ ℓ' ℓ'' ℓ''' : Level
 
 module LatticeTheory (L' : Lattice ℓ) where
- private L = fst L'
- open LatticeStr (snd L')
+  private L = fst L'
+  open LatticeStr (snd L')
+
+  0lLeftAnnihilates∧l : ∀ (x : L) → 0l ∧l x ≡ 0l
+  0lLeftAnnihilates∧l x = 0l ∧l x          ≡⟨ cong (0l ∧l_) (sym (∨lLid _)) ⟩
+                           0l ∧l (0l ∨l x) ≡⟨ ∧lAbsorb∨l _ _ ⟩
+                           0l ∎
+
+  0lRightAnnihilates∧l : ∀ (x : L) → x ∧l 0l ≡ 0l
+  0lRightAnnihilates∧l _ = ∧lComm _ _ ∙ 0lLeftAnnihilates∧l _
+
+  1lLeftAnnihilates∨l : ∀ (x : L) → 1l ∨l x ≡ 1l
+  1lLeftAnnihilates∨l x = 1l ∨l x          ≡⟨ cong (1l ∨l_) (sym (∧lLid _)) ⟩
+                           1l ∨l (1l ∧l x) ≡⟨ ∨lAbsorb∧l _ _ ⟩
+                           1l ∎
 
- 0lLeftAnnihilates∧l : ∀ (x : L) → 0l ∧l x ≡ 0l
- 0lLeftAnnihilates∧l x = 0l ∧l x          ≡⟨ cong (0l ∧l_) (sym (∨lLid _)) ⟩
-                          0l ∧l (0l ∨l x) ≡⟨ ∧lAbsorb∨l _ _ ⟩
-                          0l ∎
+  1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l
+  1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _
 
- 0lRightAnnihilates∧l : ∀ (x : L) → x ∧l 0l ≡ 0l
- 0lRightAnnihilates∧l _ = ∧lComm _ _ ∙ 0lLeftAnnihilates∧l _
 
- 1lLeftAnnihilates∨l : ∀ (x : L) → 1l ∨l x ≡ 1l
- 1lLeftAnnihilates∨l x = 1l ∨l x          ≡⟨ cong (1l ∨l_) (sym (∧lLid _)) ⟩
-                          1l ∨l (1l ∧l x) ≡⟨ ∨lAbsorb∧l _ _ ⟩
-                          1l ∎
+  ∧lCommAssocl : ∀ x y z → x ∧l (y ∧l z) ≡ y ∧l (x ∧l z)
+  ∧lCommAssocl x y z = ∧lAssoc x y z ∙∙ congL _∧l_ (∧lComm x y) ∙∙ sym (∧lAssoc y x z)
 
- 1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l
- 1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _
+  ∧lCommAssocr : ∀ x y z → (x ∧l y) ∧l z ≡ (x ∧l z) ∧l y
+  ∧lCommAssocr x y z = sym (∧lAssoc x y z) ∙∙ congR _∧l_ (∧lComm y z) ∙∙ ∧lAssoc x z y
+
+  ∧lCommAssocr2 : ∀ x y z → (x ∧l y) ∧l z ≡ (z ∧l y) ∧l x
+  ∧lCommAssocr2 x y z = ∧lCommAssocr _ _ _ ∙∙ congL _∧l_ (∧lComm _ _) ∙∙ ∧lCommAssocr _ _ _
+
+  ∧lCommAssocSwap : ∀ x y z w → (x ∧l y) ∧l (z ∧l w) ≡ (x ∧l z) ∧l (y ∧l w)
+  ∧lCommAssocSwap x y z w =
+    ∧lAssoc (x ∧l y) z w ∙∙ congL _∧l_ (∧lCommAssocr x y z) ∙∙ sym (∧lAssoc (x ∧l z) y w)
+
+  ∧lLdist∧l : ∀ x y z → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l (x ∧l z)
+  ∧lLdist∧l x y z = congL _∧l_ (sym (∧lIdem _)) ∙ ∧lCommAssocSwap x x y z
 
 
 
@@ -81,6 +98,9 @@ module Order (L' : Lattice ℓ) where
  ∧≤LCancelJoin : ∀ x y → x ∧l y ≤j y
  ∧≤LCancelJoin x y = ≤m→≤j _ _ (∧≤LCancel x y)
 
+ ∧≤RCancelJoin : ∀ x y → x ∧l y ≤j x
+ ∧≤RCancelJoin x y = ≤m→≤j _ _ (∧≤RCancel x y)
+
 
 module _ {L : Lattice ℓ} {M : Lattice ℓ'} (φ ψ : LatticeHom L M) where
  open LatticeStr ⦃...⦄