ℤ-Functors (#1068)

* use improved ringsolver

* delete one more line

* get started

* functorial action

* identity action

* Zar latt presheaf

* ring structure on global section

* unit and conunit of adjunction

* new approach

* reorganize and tidy up

* def affine cover

* remove FP stuff

* collect TODOs

* refacor

* standard basic opens

* more cleaning up

* Structure sheaf

* requested changes

Cubical/Algebra/DistLattice.agda

@@ -2,3 +2,4 @@
 module Cubical.Algebra.DistLattice where
 
 open import Cubical.Algebra.DistLattice.Base public
+open import Cubical.Algebra.DistLattice.Properties public

Cubical/Algebra/DistLattice/Properties.agda

@@ -0,0 +1,55 @@
+{-# OPTIONS --safe --lossy-unification #-}
+module Cubical.Algebra.DistLattice.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.HalfAdjoint
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.SIP
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Structures.Axioms
+open import Cubical.Structures.Auto
+open import Cubical.Structures.Macro
+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
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ where
+  open LatticeHoms
+
+  compDistLatticeHom : (L : DistLattice ℓ) (M : DistLattice ℓ') (N : DistLattice ℓ'')
+                  → DistLatticeHom L M → DistLatticeHom M N → DistLatticeHom L N
+  compDistLatticeHom L M N = compLatticeHom {L = DistLattice→Lattice L} {DistLattice→Lattice M} {DistLattice→Lattice N}
+
+  _∘dl_ : {L : DistLattice ℓ} {M : DistLattice ℓ'} {N : DistLattice ℓ''}
+        → DistLatticeHom M N → DistLatticeHom L M → DistLatticeHom L N
+  g ∘dl f = compDistLatticeHom _ _ _ f g
+
+  compIdDistLatticeHom : {L M : DistLattice ℓ} (f : DistLatticeHom L M)
+                    → compDistLatticeHom _ _ _ (idDistLatticeHom L) f ≡ f
+  compIdDistLatticeHom = compIdLatticeHom
+
+  idCompDistLatticeHom : {L M : DistLattice ℓ} (f : DistLatticeHom L M)
+                    → compDistLatticeHom _ _ _ f (idDistLatticeHom M) ≡ f
+  idCompDistLatticeHom = idCompLatticeHom
+
+  compAssocDistLatticeHom : {L M N U : DistLattice ℓ}
+                         (f : DistLatticeHom L M) (g : DistLatticeHom M N) (h : DistLatticeHom N U)
+                       → compDistLatticeHom _ _ _ (compDistLatticeHom _ _ _ f g) h
+                       ≡ compDistLatticeHom _ _ _ f (compDistLatticeHom _ _ _ g h)
+  compAssocDistLatticeHom = compAssocLatticeHom

Cubical/Algebra/Lattice/Base.agda

@@ -194,6 +194,19 @@ isPropIsLatticeHom R f S = isOfHLevelRetractFromIso 1 IsLatticeHomIsoΣ
   open LatticeStr S
 
 
+isSetLatticeHom : (A : Lattice ℓ) (B : Lattice ℓ') → isSet (LatticeHom A B)
+isSetLatticeHom A B = isSetΣSndProp (isSetΠ λ _ → is-set) (λ f → isPropIsLatticeHom (snd A) f (snd B))
+  where
+  open LatticeStr (str B) using (is-set)
+
+isSetLatticeEquiv : (A : Lattice ℓ) (B : Lattice ℓ') → isSet (LatticeEquiv A B)
+isSetLatticeEquiv A B = isSetΣSndProp (isOfHLevel≃ 2 A.is-set B.is-set)
+                                      (λ e → isPropIsLatticeHom (snd A) (fst e) (snd B))
+  where
+  module A = LatticeStr (str A)
+  module B = LatticeStr (str B)
+
+
 𝒮ᴰ-Lattice : DUARel (𝒮-Univ ℓ) LatticeStr ℓ
 𝒮ᴰ-Lattice =
   𝒮ᴰ-Record (𝒮-Univ _) IsLatticeEquiv

Cubical/Algebra/Lattice/Properties.agda

@@ -2,6 +2,7 @@
 module Cubical.Algebra.Lattice.Properties where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.HalfAdjoint
 open import Cubical.Foundations.HLevels
@@ -25,7 +26,7 @@ open import Cubical.Relation.Binary.Order.Poset
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' ℓ'' ℓ''' : Level
 
 module LatticeTheory (L' : Lattice ℓ) where
  private L = fst L'
@@ -81,7 +82,7 @@ module Order (L' : Lattice ℓ) where
  ∧≤LCancelJoin x y = ≤m→≤j _ _ (∧≤LCancel x y)
 
 
-module _ {L M : Lattice ℓ} (φ ψ : LatticeHom L M) where
+module _ {L : Lattice ℓ} {M : Lattice ℓ'} (φ ψ : LatticeHom L M) where
  open LatticeStr ⦃...⦄
  open IsLatticeHom
  private
@@ -93,3 +94,38 @@ module _ {L M : Lattice ℓ} (φ ψ : LatticeHom L M) where
 
  LatticeHom≡f : fst φ ≡ fst ψ → φ ≡ ψ
  LatticeHom≡f = Σ≡Prop λ f → isPropIsLatticeHom _ f _
+
+
+
+module LatticeHoms where
+  open IsLatticeHom
+
+  compIsLatticeHom : {A : Lattice ℓ} {B : Lattice ℓ'} {C : Lattice ℓ''}
+    {g : ⟨ B ⟩ → ⟨ C ⟩} {f : ⟨ A ⟩ → ⟨ B ⟩}
+    → IsLatticeHom (B .snd) g (C .snd)
+    → IsLatticeHom (A .snd) f (B .snd)
+    → IsLatticeHom (A .snd) (g ∘ f) (C .snd)
+  compIsLatticeHom {g = g} {f} gh fh .pres0 = cong g (fh .pres0) ∙ gh .pres0
+  compIsLatticeHom {g = g} {f} gh fh .pres1 = cong g (fh .pres1) ∙ gh .pres1
+  compIsLatticeHom {g = g} {f} gh fh .pres∨l x y = cong g (fh .pres∨l x y) ∙ gh .pres∨l (f x) (f y)
+  compIsLatticeHom {g = g} {f} gh fh .pres∧l x y = cong g (fh .pres∧l x y) ∙ gh .pres∧l (f x) (f y)
+
+
+  compLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} {N : Lattice ℓ''}
+              → LatticeHom L M → LatticeHom M N → LatticeHom L N
+  fst (compLatticeHom f g) x = g .fst (f .fst x)
+  snd (compLatticeHom f g) = compIsLatticeHom (g .snd) (f .snd)
+
+  _∘l_ : {L : Lattice ℓ} {M : Lattice ℓ'} {N : Lattice ℓ''} → LatticeHom M N → LatticeHom L M → LatticeHom L N
+  _∘l_ = flip compLatticeHom
+
+  compIdLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} (φ : LatticeHom L M) → compLatticeHom (idLatticeHom L) φ ≡ φ
+  compIdLatticeHom φ = LatticeHom≡f _ _ refl
+
+  idCompLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} (φ : LatticeHom L M) → compLatticeHom φ (idLatticeHom M) ≡ φ
+  idCompLatticeHom φ = LatticeHom≡f _ _ refl
+
+  compAssocLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} {N : Lattice ℓ''} {U : Lattice ℓ'''}
+                   → (φ : LatticeHom L M) (ψ : LatticeHom M N) (χ : LatticeHom N U)
+                   → compLatticeHom (compLatticeHom φ ψ) χ ≡ compLatticeHom φ (compLatticeHom ψ χ)
+  compAssocLatticeHom _ _ _ = LatticeHom≡f _ _ refl

Cubical/Algebra/ZariskiLattice/UniversalProperty.agda

@@ -315,3 +315,63 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where
   open Join ZariskiLattice
   ⋁D≡ : {n : ℕ} (α : FinVec R n) → ⋁ (D ∘ α) ≡ [ n , α ]
   ⋁D≡ _ = funExt⁻ (cong fst ZLUniversalPropCorollary) _
+
+-- the lattice morphism induced by a ring morphism
+module _ {A B : CommRing ℓ} (φ : CommRingHom A B) where
+
+ open ZarLat
+ open ZarLatUniversalProp
+ open IsZarMap
+ open CommRingStr ⦃...⦄
+ open DistLatticeStr ⦃...⦄
+ open IsRingHom
+ private
+   instance
+     _ = A .snd
+     _ = B .snd
+     _ = (ZariskiLattice A) .snd
+     _ = (ZariskiLattice B) .snd
+
+ Dcomp : A .fst → ZL B
+ Dcomp f = D B (φ .fst f)
+
+ isZarMapDcomp : IsZarMap A (ZariskiLattice B) Dcomp
+ pres0 isZarMapDcomp = cong (D B) (φ .snd .pres0) ∙ isZarMapD B .pres0
+ pres1 isZarMapDcomp = cong (D B) (φ .snd .pres1) ∙ isZarMapD B .pres1
+ ·≡∧ isZarMapDcomp f g = cong (D B) (φ .snd .pres· f g)
+                    ∙ isZarMapD B .·≡∧ (φ .fst f) (φ .fst g)
+ +≤∨ isZarMapDcomp f g =
+   let open JoinSemilattice
+             (Lattice→JoinSemilattice (DistLattice→Lattice (ZariskiLattice B)))
+   in subst (λ x → x ≤ (Dcomp f) ∨l (Dcomp g))
+            (sym (cong (D B) (φ .snd .pres+ f g)))
+            (isZarMapD B .+≤∨ (φ .fst f) (φ .fst g))
+
+ inducedZarLatHom : DistLatticeHom (ZariskiLattice A) (ZariskiLattice B)
+ inducedZarLatHom = ZLHasUniversalProp A (ZariskiLattice B) Dcomp isZarMapDcomp .fst .fst
+
+-- functoriality
+module _ (A : CommRing ℓ) where
+  open ZarLat
+  open ZarLatUniversalProp
+
+  inducedZarLatHomId : inducedZarLatHom (idCommRingHom A)
+                     ≡ idDistLatticeHom (ZariskiLattice A)
+  inducedZarLatHomId =
+    cong fst
+      (ZLHasUniversalProp A (ZariskiLattice A) (Dcomp (idCommRingHom A))
+                                               (isZarMapDcomp (idCommRingHom A)) .snd
+        (idDistLatticeHom (ZariskiLattice A) , refl))
+
+module _ {A B C : CommRing ℓ} (φ : CommRingHom A B) (ψ : CommRingHom B C) where
+  open ZarLat
+  open ZarLatUniversalProp
+
+  inducedZarLatHomSeq : inducedZarLatHom (ψ ∘cr φ)
+                      ≡ inducedZarLatHom ψ ∘dl inducedZarLatHom φ
+  inducedZarLatHomSeq =
+    cong fst
+      (ZLHasUniversalProp A (ZariskiLattice C) (Dcomp (ψ ∘cr φ))
+                                               (isZarMapDcomp (ψ ∘cr φ)) .snd
+        (inducedZarLatHom ψ ∘dl inducedZarLatHom φ , funExt (λ _ → ∨lRid _)))
+    where open DistLatticeStr (ZariskiLattice C .snd)

Cubical/Categories/Instances/DistLattices.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Instances.DistLattices where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+
+open import Cubical.Algebra.Lattice
+open import Cubical.Algebra.DistLattice
+
+open import Cubical.Categories.Category
+
+open Category
+
+
+DistLatticesCategory : ∀ {ℓ} → Category (ℓ-suc ℓ) ℓ
+ob DistLatticesCategory                     = DistLattice _
+Hom[_,_] DistLatticesCategory               = DistLatticeHom
+id DistLatticesCategory {L}                 = idDistLatticeHom L
+_⋆_ DistLatticesCategory {L} {M} {N}        = compDistLatticeHom L M N
+⋆IdL DistLatticesCategory {L} {M}           = compIdDistLatticeHom {L = L} {M}
+⋆IdR DistLatticesCategory {L} {M}           = idCompDistLatticeHom {L = L} {M}
+⋆Assoc DistLatticesCategory {L} {M} {N} {O} = compAssocDistLatticeHom {L = L} {M} {N} {O}
+isSetHom DistLatticesCategory = isSetLatticeHom _ _

Cubical/Categories/Instances/Lattices.agda

@@ -0,0 +1,22 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Instances.Lattices where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+
+open import Cubical.Algebra.Lattice
+
+open import Cubical.Categories.Category
+
+open Category
+open LatticeHoms
+
+LatticesCategory : ∀ {ℓ} → Category (ℓ-suc ℓ) ℓ
+ob LatticesCategory       = Lattice _
+Hom[_,_] LatticesCategory = LatticeHom
+id LatticesCategory {L}   = idLatticeHom L
+_⋆_ LatticesCategory      = compLatticeHom
+⋆IdL LatticesCategory     = compIdLatticeHom
+⋆IdR LatticesCategory     = idCompLatticeHom
+⋆Assoc LatticesCategory   = compAssocLatticeHom
+isSetHom LatticesCategory = isSetLatticeHom _ _