Algebraic geometry directory

Cubical/Algebra/CommRing/Localisation/InvertingElements.agda

@@ -279,6 +279,40 @@ module InvertingElementsBase (R' : CommRing ℓ) where
                 PT.rec (PisProp s) λ (n , p) → subst P (sym p) (base n)
 
 
+
+ -- A more specialized universal property.
+ -- (Just ask f to become invertible, not all its powers.)
+ module UniversalProp (f : R) where
+   open S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) public
+   open CommRingHomTheory
+
+   invElemUniversalProp : (A : CommRing ℓ) (φ : CommRingHom R' A)
+                        → (φ .fst f ∈ A ˣ)
+                        → ∃![ χ ∈ CommRingHom R[1/ f ]AsCommRing A ]
+                            (fst χ) ∘ (fst /1AsCommRingHom) ≡ (fst φ)
+   invElemUniversalProp A φ φf∈Aˣ =
+     S⁻¹RHasUniversalProp A φ
+       (powersPropElim (λ _ → ∈-isProp _ _)
+       (λ n → subst-∈ (A ˣ) (sym (pres^ φ f n)) (Exponentiation.^-presUnit A _ n φf∈Aˣ)))
+
+
+-- "functorial action" of localizing away from an element
+module _ {A B : CommRing ℓ} (φ : CommRingHom A B) (f : fst A) where
+  open CommRingStr (snd B)
+  private
+    module A = InvertingElementsBase A
+    module B = InvertingElementsBase B
+    module AU = A.UniversalProp f
+    module BU = B.UniversalProp (φ $r f)
+
+    φ/1 = BU./1AsCommRingHom ∘cr φ
+
+  uniqInvElemHom : ∃![ χ ∈ CommRingHom A.R[1/ f ]AsCommRing B.R[1/ φ $r f ]AsCommRing ]
+                     (fst χ) ∘ (fst AU./1AsCommRingHom) ≡ (fst φ/1)
+  uniqInvElemHom = AU.invElemUniversalProp _ φ/1 (BU.S/1⊆S⁻¹Rˣ _ ∣ 1 , sym (·IdR _) ∣₁)
+
+
+
 module _ (R : CommRing ℓ) (f : fst R) where
  open CommRingTheory R
  open RingTheory (CommRing→Ring R)

Cubical/Algebra/CommRing/Localisation/Limit.agda

@@ -64,7 +64,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
  open CommRingTheory R'
  open RingTheory (CommRing→Ring R')
  open Sum (CommRing→Ring R')
- open CommIdeal R' hiding (subst-∈)
+ open CommIdeal R'
  open InvertingElementsBase R'
  open Exponentiation R'
  open CommRingStr ⦃...⦄

Cubical/Algebra/CommRing/Properties.agda

@@ -200,34 +200,6 @@ module CommRingEquivs where
  fst (idCommRingEquiv A) = idEquiv (fst A)
  snd (idCommRingEquiv A) = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)
 
-module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where
- open Units A' renaming (Rˣ to Aˣ ; _⁻¹ to _⁻¹ᵃ ; ·-rinv to ·A-rinv ; ·-linv to ·A-linv)
- private A = fst A'
- open CommRingStr (snd A') renaming (_·_ to _·A_ ; 1r to 1a)
- open Units B' renaming (Rˣ to Bˣ ; _⁻¹ to _⁻¹ᵇ ; ·-rinv to ·B-rinv)
- open CommRingStr (snd B') renaming  ( _·_ to _·B_ ; 1r to 1b
-                                     ; ·IdL to ·B-lid ; ·IdR to ·B-rid
-                                     ; ·Assoc to ·B-assoc)
-
- private
-   f = fst φ
- open IsRingHom (φ .snd)
-
- RingHomRespInv : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ → f r ∈ Bˣ
- RingHomRespInv r = f (r ⁻¹ᵃ) , (sym (pres· r (r ⁻¹ᵃ)) ∙∙ cong (f) (·A-rinv r) ∙∙ pres1)
-
- φ[x⁻¹]≡φ[x]⁻¹ : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ ⦃ φr∈Bˣ : f r ∈ Bˣ ⦄
-               → f (r ⁻¹ᵃ) ≡ (f r) ⁻¹ᵇ
- φ[x⁻¹]≡φ[x]⁻¹ r ⦃ r∈Aˣ ⦄ ⦃ φr∈Bˣ ⦄ =
-  f (r ⁻¹ᵃ)                         ≡⟨ sym (·B-rid _) ⟩
-  f (r ⁻¹ᵃ) ·B 1b                   ≡⟨ congR _·B_ (sym (·B-rinv _)) ⟩
-  f (r ⁻¹ᵃ) ·B ((f r) ·B (f r) ⁻¹ᵇ) ≡⟨ ·B-assoc _ _ _ ⟩
-  f (r ⁻¹ᵃ) ·B (f r) ·B (f r) ⁻¹ᵇ   ≡⟨ congL _·B_ (sym (pres· _ _)) ⟩
-  f (r ⁻¹ᵃ ·A r) ·B (f r) ⁻¹ᵇ       ≡⟨ cong (λ x → f x ·B (f r) ⁻¹ᵇ) (·A-linv _) ⟩
-  f 1a ·B (f r) ⁻¹ᵇ                 ≡⟨ congL _·B_ pres1 ⟩
-  1b ·B (f r) ⁻¹ᵇ                   ≡⟨ ·B-lid _ ⟩
-  (f r) ⁻¹ᵇ                         ∎
-
 
 module Exponentiation (R' : CommRing ℓ) where
  open CommRingStr (snd R')
@@ -276,6 +248,40 @@ module Exponentiation (R' : CommRing ℓ) where
  ^-presUnit f (suc n) f∈Rˣ = RˣMultClosed f (f ^ n) ⦃ f∈Rˣ ⦄ ⦃ ^-presUnit f n f∈Rˣ ⦄
 
 
+module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where
+ open Units A' renaming (Rˣ to Aˣ ; _⁻¹ to _⁻¹ᵃ ; ·-rinv to ·A-rinv ; ·-linv to ·A-linv)
+ open Units B' renaming (Rˣ to Bˣ ; _⁻¹ to _⁻¹ᵇ ; ·-rinv to ·B-rinv)
+ open Exponentiation A' renaming (_^_ to _^ᵃ_)
+ open Exponentiation B' renaming (_^_ to _^ᵇ_)
+ open CommRingStr ⦃...⦄
+ private
+   A = fst A'
+   f = fst φ
+   instance
+     _ = A' .snd
+     _ = B' .snd
+ open IsRingHom (φ .snd)
+
+ RingHomRespInv : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ → f r ∈ Bˣ
+ RingHomRespInv r = f (r ⁻¹ᵃ) , (sym (pres· r (r ⁻¹ᵃ)) ∙∙ cong (f) (·A-rinv r) ∙∙ pres1)
+
+ φ[x⁻¹]≡φ[x]⁻¹ : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ ⦃ φr∈Bˣ : f r ∈ Bˣ ⦄
+               → f (r ⁻¹ᵃ) ≡ (f r) ⁻¹ᵇ
+ φ[x⁻¹]≡φ[x]⁻¹ r ⦃ r∈Aˣ ⦄ ⦃ φr∈Bˣ ⦄ =
+  f (r ⁻¹ᵃ)                         ≡⟨ sym (·IdR _) ⟩
+  f (r ⁻¹ᵃ) · 1r                   ≡⟨ congR _·_ (sym (·B-rinv _)) ⟩
+  f (r ⁻¹ᵃ) · ((f r) · (f r) ⁻¹ᵇ) ≡⟨ ·Assoc _ _ _ ⟩
+  f (r ⁻¹ᵃ) · (f r) · (f r) ⁻¹ᵇ   ≡⟨ congL _·_ (sym (pres· _ _)) ⟩
+  f (r ⁻¹ᵃ · r) · (f r) ⁻¹ᵇ       ≡⟨ cong (λ x → f x · (f r) ⁻¹ᵇ) (·A-linv _) ⟩
+  f 1r · (f r) ⁻¹ᵇ                 ≡⟨ congL _·_ pres1 ⟩
+  1r · (f r) ⁻¹ᵇ                   ≡⟨ ·IdL _ ⟩
+  (f r) ⁻¹ᵇ                         ∎
+
+ pres^ : (x : A) (n : ℕ) → f (x ^ᵃ n) ≡ f x ^ᵇ n
+ pres^ x zero = pres1
+ pres^ x (suc n) = pres· _ _ ∙ cong (f x ·_) (pres^ x n)
+
+
 -- like in Ring.Properties we provide helpful lemmas here
 module CommRingTheory (R' : CommRing ℓ) where
  open CommRingStr (snd R')

Cubical/Algebra/DistLattice/BigOps.agda

@@ -34,7 +34,7 @@ open import Cubical.Relation.Binary.Order.Poset
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' : Level
 
 module KroneckerDelta (L' : DistLattice ℓ) where
  private
@@ -107,6 +107,20 @@ 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 IsLatticeHom (φ .snd)
+  open DistLatticeStr ⦃...⦄
+  open Join
+  open BigOpMap (LatticeHom→JoinSemilatticeHom φ)
+  private instance
+    _ = L .snd
+    _ = L' .snd
+
+  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 ⦃...⦄

Cubical/Algebra/Monoid/BigOp.agda

@@ -57,3 +57,18 @@ module MonoidBigOp (M' : Monoid ℓ) where
 
  bigOpSplit++ {n = zero} V W = sym (·IdL _)
  bigOpSplit++ {n = suc n} V W = cong (V zero ·_) (bigOpSplit++ (V ∘ suc) W) ∙ ·Assoc _ _ _
+
+
+
+module BigOpMap {M : Monoid ℓ} {M' : Monoid ℓ'} (φ : MonoidHom M M') where
+  private module M = MonoidBigOp M
+  private module M' = MonoidBigOp M'
+  open IsMonoidHom (φ .snd)
+  open MonoidStr ⦃...⦄
+  private instance
+    _ = M .snd
+    _ = M' .snd
+
+  presBigOp : {n : ℕ} (U : FinVec ⟨ M ⟩ n) → φ .fst (M.bigOp U) ≡ M'.bigOp (φ .fst ∘ U)
+  presBigOp {n = zero} U = presε
+  presBigOp {n = suc n} U = pres· _ _ ∙ cong (φ .fst (U zero) ·_) (presBigOp (U ∘ suc))