Skip to content

Commit 1397b03

Browse files
anshwad10anshwad10
authored
Use posetal reflections for Zariski Lattice
1 parent 1c9c647 commit 1397b03

File tree

1 file changed

+174
-164
lines changed
  • Cubical/AlgebraicGeometry/ZariskiLattice

1 file changed

+174
-164
lines changed

‎Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda‎

Lines changed: 174 additions & 164 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
{-# OPTIONS --safe --lossy-unification #-}
1+
{-# OPTIONS --cubical --safe --lossy-unification #-}
22
module Cubical.AlgebraicGeometry.ZariskiLattice.Base where
33

44

@@ -23,6 +23,9 @@ open import Cubical.Data.Unit
2323
open import Cubical.Relation.Nullary
2424
open import Cubical.Relation.Binary
2525
open import Cubical.Relation.Binary.Order.Poset
26+
open import Cubical.Relation.Binary.Order.Proset
27+
open import Cubical.Relation.Binary.Order.Poset.Instances.PosetalReflection as PR
28+
open import Cubical.Functions.Embedding
2629

2730
open import Cubical.Algebra.Ring
2831
open import Cubical.Algebra.Ring.Properties
@@ -39,181 +42,188 @@ open import Cubical.Algebra.DistLattice
3942
open import Cubical.Algebra.Matrix
4043

4144
open import Cubical.HITs.SetQuotients as SQ
45+
open import Cubical.HITs.PropositionalTruncation as PT
46+
47+
open import Cubical.Tactics.CommRingSolver
4248

4349
open Iso
4450
open BinaryRelation
4551
open isEquivRel
4652

47-
private
48-
variable
49-
ℓ ℓ' : Level
53+
private variable
54+
ℓ ℓ' : Level
5055

5156

5257
module ZarLat (R' : CommRing ℓ) where
53-
open CommRingStr (snd R')
54-
open RingTheory (CommRing→Ring R')
55-
open Sum (CommRing→Ring R')
56-
open CommRingTheory R'
57-
open Exponentiation R'
58-
open BinomialThm R'
59-
open CommIdeal R'
60-
open RadicalIdeal R'
61-
open isCommIdeal
62-
open ProdFin R'
63-
open IdealSum R'
64-
65-
private
66-
R = fst R'
67-
A = Σ[ n ∈ ℕ ] (FinVec R n)
68-
⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
69-
⟨ V ⟩ = ⟨ V ⟩[ R' ]
70-
71-
-- This is small!
72-
_≼_ : A → A → Type ℓ
73-
(_ , α) ≼ (_ , β) = ∀ i → α i ∈ √ ⟨ β ⟩
74-
75-
private
58+
open CommRingStr (snd R')
59+
open RingTheory (CommRing→Ring R')
60+
open Sum (CommRing→Ring R')
61+
open CommRingTheory R'
62+
open Exponentiation R'
63+
open BinomialThm R'
64+
open CommIdeal R'
65+
open RadicalIdeal R'
66+
open isCommIdeal
67+
open ProdFin R'
68+
open IdealSum R'
69+
70+
private
71+
R = fst R'
72+
A = Σ[ n ∈ ℕ ] (FinVec R n)
73+
⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
74+
⟨ V ⟩ = ⟨ V ⟩[ R' ]
75+
76+
-- This is small!
77+
_≼_ : A → A → Type ℓ
78+
(_ , α) ≼ (_ , β) = ∀ i → α i ∈ √ ⟨ β ⟩
79+
7680
isRefl≼ : ∀ {a} → a ≼ a
7781
isRefl≼ i = ∈→∈√ _ _ (indInIdeal _ _ i)
7882

7983
isTrans≼ : ∀ {a b c : A} → a ≼ b → b ≼ c → a ≼ c
8084
isTrans≼ a≼b b≼c i = (√FGIdealCharRImpl _ _ b≼c) _ (a≼b i)
8185

82-
_∼_ : A → A → Type ℓ -- \sim
83-
α ∼ β = (α ≼ β) × (β ≼ α)
84-
85-
∼PropValued : isPropValued (_∼_)
86-
∼PropValued (_ , α) (_ , β) = isProp× (isPropΠ (λ i → √ ⟨ β ⟩ .fst (α i) .snd))
87-
(isPropΠ (λ i → √ ⟨ α ⟩ .fst (β i) .snd))
88-
89-
∼EquivRel : isEquivRel (_∼_)
90-
reflexive ∼EquivRel _ = isRefl≼ , isRefl≼
91-
symmetric ∼EquivRel _ _ = Σ-swap-Iso .fun
92-
transitive ∼EquivRel _ _ _ a∼b b∼c = isTrans≼ (fst a∼b) (fst b∼c) , isTrans≼ (snd b∼c) (snd a∼b)
93-
94-
-- lives in the same universe as R
95-
ZL : Type ℓ
96-
ZL = A / (_∼_)
97-
98-
-- need something big in our proofs though:
99-
_∼≡_ : A → A → Type (ℓ-suc ℓ)
100-
(_ , α) ∼≡ (_ , β) = √ ⟨ α ⟩ ≡ √ ⟨ β ⟩
101-
102-
≡→∼ : ∀ {a b : A} → a ∼≡ b → a ∼ b
103-
≡→∼ r = √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) r h)
104-
, √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) (sym r) h)
105-
106-
∼→≡ : ∀ {a b : A} → a ∼ b → a ∼≡ b
107-
∼→≡ r = CommIdeal≡Char (√FGIdealCharRImpl _ ⟨ _ ⟩ (fst r))
108-
(√FGIdealCharRImpl _ ⟨ _ ⟩ (snd r))
109-
110-
∼≃≡ : ∀ {a b : A} → (a ∼ b) ≃ (a ∼≡ b)
111-
∼≃≡ = propBiimpl→Equiv (∼PropValued _ _) (isSetCommIdeal _ _) ∼→≡ ≡→∼
112-
113-
0z : ZL
114-
0z = [ 0 , (λ ()) ]
115-
116-
1z : ZL
117-
1z = [ 1 , (replicateFinVec 1 1r) ]
118-
119-
_∨z_ : ZL → ZL → ZL
120-
_∨z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
121-
(λ (_ , α) (_ , β) → (_ , α ++Fin β))
122-
(λ (_ , α) (_ , β) → ≡→∼ (cong √
123-
(FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α))))
124-
λ (_ , α) (_ , β) (_ , γ) α∼β → ≡→∼ (--need to show α∨γ ∼ β∨γ
125-
√ ⟨ α ++Fin γ ⟩ ≡⟨ cong √ (FGIdealAddLemma _ α γ) ⟩
126-
√ (⟨ α ⟩ +i ⟨ γ ⟩) ≡⟨ sym (√+LContr _ _) ⟩
127-
√ (√ ⟨ α ⟩ +i ⟨ γ ⟩) ≡⟨ cong (λ I → √ (I +i ⟨ γ ⟩)) (∼→≡ α∼β) ⟩
128-
√ (√ ⟨ β ⟩ +i ⟨ γ ⟩) ≡⟨ √+LContr _ _ ⟩
129-
√ (⟨ β ⟩ +i ⟨ γ ⟩) ≡⟨ cong √ (sym (FGIdealAddLemma _ β γ)) ⟩
130-
√ ⟨ β ++Fin γ ⟩ ∎)
131-
132-
_∧z_ : ZL → ZL → ZL
133-
_∧z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
134-
(λ (_ , α) (_ , β) → (_ , α ··Fin β))
135-
(λ (_ , α) (_ , β) → ≡→∼ (cong √
136-
(FGIdealMultLemma _ α β ∙∙ ·iComm _ _ ∙∙ sym (FGIdealMultLemma _ β α))))
137-
λ (_ , α) (_ , β) (_ , γ) α∼β → ≡→∼ (--need to show α∧γ ∼ β∧γ
138-
√ ⟨ α ··Fin γ ⟩ ≡⟨ cong √ (FGIdealMultLemma _ α γ) ⟩
139-
√ (⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ sym (√·LContr _ _) ⟩
140-
√ (√ ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong (λ I → √ (I ·i ⟨ γ ⟩)) (∼→≡ α∼β) ⟩
141-
√ (√ ⟨ β ⟩ ·i ⟨ γ ⟩) ≡⟨ √·LContr _ _ ⟩
142-
√ (⟨ β ⟩ ·i ⟨ γ ⟩) ≡⟨ cong √ (sym (FGIdealMultLemma _ β γ)) ⟩
143-
√ ⟨ β ··Fin γ ⟩ ∎)
144-
145-
-- join axioms
146-
∨zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∨z (𝔟 ∨z 𝔠) ≡ (𝔞 ∨z 𝔟) ∨z 𝔠
147-
∨zAssoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
148-
λ (_ , α) (_ , β) (_ , γ) → eq/ _ _ (≡→∼ (cong √ (IdealAddAssoc _ _ _ _)))
149-
150-
∨zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∨z 𝔟 ≡ 𝔟 ∨z 𝔞
151-
∨zComm = SQ.elimProp2 (λ _ _ → squash/ _ _)
152-
λ (_ , α) (_ , β) → eq/ _ _
153-
(≡→∼ (cong √ (FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α))))
154-
155-
∨zLid : ∀ (𝔞 : ZL) → 0z ∨z 𝔞 ≡ 𝔞
156-
∨zLid = SQ.elimProp (λ _ → squash/ _ _) λ _ → eq/ _ _ (reflexive ∼EquivRel _)
157-
158-
∨zRid : ∀ (𝔞 : ZL) → 𝔞 ∨z 0z ≡ 𝔞
159-
∨zRid _ = ∨zComm _ _ ∙ ∨zLid _
160-
161-
162-
-- -- meet axioms
163-
∧zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∧z 𝔠) ≡ (𝔞 ∧z 𝔟) ∧z 𝔠
164-
∧zAssoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
86+
≼PropValued : isPropValued _≼_
87+
≼PropValued (_ , α) (_ , β) = isPropΠ λ i → √ ⟨ β ⟩ .fst (α i) .snd
88+
89+
isProset≼ : IsProset _≼_
90+
isProset≼ = isproset (isSetΣ isSetℕ λ x → isSet→ is-set) ≼PropValued (λ _ → isRefl≼) (λ _ _ _ → isTrans≼)
91+
92+
_∼_ : A → A → Type ℓ -- \sim
93+
_∼_ = SymKernel _≼_
94+
95+
∼PropValued : isPropValued (_∼_)
96+
∼PropValued (_ , α) (_ , β) = isProp× (isPropΠ (λ i → √ ⟨ β ⟩ .fst (α i) .snd))
97+
(isPropΠ (λ i → √ ⟨ α ⟩ .fst (β i) .snd))
98+
99+
∼EquivRel : isEquivRel (_∼_)
100+
∼EquivRel = isProset→isEquivRelSymKernel isProset≼
101+
102+
private
103+
AProset : Proset ℓ ℓ
104+
AProset = _ , prosetstr _≼_ isProset≼
105+
106+
-- lives in the same universe as R
107+
ZLPoset : Poset ℓ ℓ
108+
ZLPoset = ReflectionPoset AProset
109+
110+
ZL : Type ℓ
111+
ZL = ZLPoset .fst
112+
113+
_≤ZL_ = ZLPoset .snd .PosetStr._≤_
114+
isPosetZL = ZLPoset .snd .PosetStr.isPoset
115+
isProsetZL = isPoset→isProset isPosetZL
116+
117+
0a : A
118+
0a = 0 , λ ()
119+
120+
1a : A
121+
1a = 1 , λ _ → 1r
122+
123+
-- need something big in our proofs though:
124+
_∼≡_ : A → A → Type (ℓ-suc ℓ)
125+
(_ , α) ∼≡ (_ , β) = √ ⟨ α ⟩ ≡ √ ⟨ β ⟩
126+
127+
≡→∼ : ∀ {a b : A} → a ∼≡ b → a ∼ b
128+
≡→∼ r = √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) r h)
129+
, √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) (sym r) h)
130+
131+
∼→≡ : ∀ {a b : A} → a ∼ b → a ∼≡ b
132+
∼→≡ r = CommIdeal≡Char (√FGIdealCharRImpl _ ⟨ _ ⟩ (fst r))
133+
(√FGIdealCharRImpl _ ⟨ _ ⟩ (snd r))
134+
135+
∼≃≡ : ∀ {a b : A} → (a ∼ b) ≃ (a ∼≡ b)
136+
∼≃≡ = propBiimpl→Equiv (∼PropValued _ _) (isSetCommIdeal _ _) ∼→≡ ≡→∼
137+
138+
0z : ZL
139+
0z = [ 0a ]
140+
141+
0z-least : isLeast isProsetZL (_ , id↪ _) 0z
142+
0z-least = []presLeast AProset 0a λ x ()
143+
144+
1z : ZL
145+
1z = [ 1a ]
146+
147+
1z-greatest : isGreatest isProsetZL (_ , id↪ _) 1z
148+
1z-greatest = []presGreatest AProset 1a λ x i → ∣ 0 , ∣ const 1r , solve! R' ∣₁ ∣₁
149+
150+
_∨a_ : A → A → A
151+
(_ , α) ∨a (_ , β) = _ , α ++Fin β
152+
153+
∨a-join : ∀ x y → isJoin isProset≼ x y (x ∨a y)
154+
∨a-join x y z = {! !}
155+
156+
ZL-joins : isJoinSemipseudolattice ZLPoset
157+
ZL-joins = hasBinJoins AProset λ x y → _ , ∨a-join x y
158+
159+
_∨z_ : ZL → ZL → ZL
160+
x ∨z y = ZL-joins x y .fst
161+
162+
_∧a_ : A → A → A
163+
(_ , α) ∧a (_ , β) = _ , α ··Fin β
164+
165+
∧a-meet : ∀ x y → isMeet isProset≼ x y (x ∧a y)
166+
∧a-meet x y z = {! !}
167+
168+
ZL-meets : isMeetSemipseudolattice ZLPoset
169+
ZL-meets = hasBinMeets AProset λ x y → _ , ∧a-meet x y
170+
171+
_∧z_ : ZL → ZL → ZL
172+
x ∧z y = ZL-meets x y .fst
173+
174+
-- join axioms
175+
∨zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∨z (𝔟 ∨z 𝔠) ≡ (𝔞 ∨z 𝔟) ∨z 𝔠
176+
∨zAssoc = joinAssoc isPosetZL ZL-joins
177+
178+
∨zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∨z 𝔟 ≡ 𝔟 ∨z 𝔞
179+
∨zComm = joinComm isPosetZL ZL-joins
180+
181+
∨zLid : ∀ (𝔞 : ZL) → 0z ∨z 𝔞 ≡ 𝔞
182+
∨zLid = SQ.elimProp (λ _ → squash/ _ _) λ _ → refl
183+
184+
∨zRid : ∀ (𝔞 : ZL) → 𝔞 ∨z 0z ≡ 𝔞
185+
∨zRid _ = ∨zComm _ _ ∙ ∨zLid _
186+
187+
-- -- meet axioms
188+
∧zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∧z 𝔠) ≡ (𝔞 ∧z 𝔟) ∧z 𝔠
189+
∧zAssoc = meetAssoc isPosetZL ZL-meets
190+
191+
∧zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z 𝔟 ≡ 𝔟 ∧z 𝔞
192+
∧zComm = meetComm isPosetZL ZL-meets
193+
194+
∧zRid : ∀ (𝔞 : ZL) → 𝔞 ∧z 1z ≡ 𝔞
195+
∧zRid = SQ.elimProp (λ _ → squash/ _ _) λ (_ , α) → eq/ _ _ $ ≡→∼ $ cong √ $
196+
⟨ α ··Fin (replicateFinVec 1 1r) ⟩ ≡⟨ FGIdealMultLemma _ _ _ ⟩
197+
⟨ α ⟩ ·i ⟨ (replicateFinVec 1 1r) ⟩ ≡⟨ cong (⟨ α ⟩ ·i_) (contains1Is1 _ (indInIdeal _ _ zero)) ⟩
198+
⟨ α ⟩ ·i 1Ideal ≡⟨ ·iRid _ ⟩
199+
⟨ α ⟩ ∎
200+
201+
202+
-- absorption and distributivity
203+
∧zAbsorb∨z : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z (𝔞 ∨z 𝔟) ≡ 𝔞
204+
∧zAbsorb∨z = MeetAbsorbLJoin ZLPoset (ZL-meets , ZL-joins)
205+
206+
∧zLDist∨z : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∨z 𝔠) ≡ (𝔞 ∧z 𝔟) ∨z (𝔞 ∧z 𝔠)
207+
∧zLDist∨z = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
165208
λ (_ , α) (_ , β) (_ , γ) → eq/ _ _ (≡→∼
166-
(√ ⟨ α ··Fin (β ··Fin γ) ⟩ ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
167-
√ (⟨ α ⟩ ·i ⟨ β ··Fin γ ⟩) ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealMultLemma _ _ _) ⟩
168-
√ (⟨ α ⟩ ·i (⟨ β ⟩ ·i ⟨ γ ⟩)) ≡⟨ cong √ (·iAssoc _ _ _) ⟩
169-
√ ((⟨ α ⟩ ·i ⟨ β ⟩) ·i ⟨ γ ⟩) ≡⟨ cong (λ x → √ (x ·i ⟨ γ ⟩)) (sym (FGIdealMultLemma _ _ _)) ⟩
170-
√ (⟨ α ··Fin β ⟩ ·i ⟨ γ ⟩) ≡⟨ cong √ (sym (FGIdealMultLemma _ _ _)) ⟩
171-
√ ⟨ (α ··Fin β) ··Fin γ ⟩ ∎))
172-
173-
∧zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z 𝔟 ≡ 𝔟 ∧z 𝔞
174-
∧zComm = SQ.elimProp2 (λ _ _ → squash/ _ _)
175-
λ (_ , α) (_ , β) → eq/ _ _ (≡→∼
176-
(cong √ (FGIdealMultLemma _ α β ∙∙ ·iComm _ _ ∙∙ sym (FGIdealMultLemma _ β α))))
177-
178-
∧zRid : ∀ (𝔞 : ZL) → 𝔞 ∧z 1z ≡ 𝔞
179-
∧zRid = SQ.elimProp (λ _ → squash/ _ _)
180-
λ (_ , α) → eq/ _ _ (≡→∼ (cong √
181-
(⟨ α ··Fin (replicateFinVec 1 1r) ⟩ ≡⟨ FGIdealMultLemma _ _ _ ⟩
182-
⟨ α ⟩ ·i ⟨ (replicateFinVec 1 1r) ⟩ ≡⟨ cong (⟨ α ⟩ ·i_) (contains1Is1 _ (indInIdeal _ _ zero)) ⟩
183-
⟨ α ⟩ ·i 1Ideal ≡⟨ ·iRid _ ⟩
184-
⟨ α ⟩ ∎)))
185-
186-
187-
-- absorption and distributivity
188-
∧zAbsorb∨z : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z (𝔞 ∨z 𝔟) ≡ 𝔞
189-
∧zAbsorb∨z = SQ.elimProp2 (λ _ _ → squash/ _ _)
190-
λ (_ , α) (_ , β) → eq/ _ _ (≡→∼
191-
(√ ⟨ α ··Fin (α ++Fin β) ⟩ ≡⟨ cong √ (FGIdealMultLemma _ α (α ++Fin β)) ⟩
192-
√ (⟨ α ⟩ ·i ⟨ α ++Fin β ⟩) ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ α β) ⟩
193-
√ (⟨ α ⟩ ·i (⟨ α ⟩ +i ⟨ β ⟩)) ≡⟨ √·Absorb+ _ _ ⟩
194-
√ ⟨ α ⟩ ∎))
195-
196-
∧zLDist∨z : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∨z 𝔠) ≡ (𝔞 ∧z 𝔟) ∨z (𝔞 ∧z 𝔠)
197-
∧zLDist∨z = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
198-
λ (_ , α) (_ , β) (_ , γ) → eq/ _ _ (≡→∼
199-
(√ ⟨ α ··Fin (β ++Fin γ) ⟩ ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
200-
√ (⟨ α ⟩ ·i ⟨ β ++Fin γ ⟩) ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ _ _) ⟩
201-
√ (⟨ α ⟩ ·i (⟨ β ⟩ +i ⟨ γ ⟩)) ≡⟨ cong √ (·iRdist+i _ _ _) ⟩
202-
-- L/R-dist are swapped
203-
-- in Lattices vs Rings
204-
√ (⟨ α ⟩ ·i ⟨ β ⟩ +i ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong₂ (λ x y → √ (x +i y))
205-
(sym (FGIdealMultLemma _ _ _))
206-
(sym (FGIdealMultLemma _ _ _)) ⟩
207-
√ (⟨ α ··Fin β ⟩ +i ⟨ α ··Fin γ ⟩) ≡⟨ cong √ (sym (FGIdealAddLemma _ _ _)) ⟩
208-
√ ⟨ (α ··Fin β) ++Fin (α ··Fin γ) ⟩ ∎))
209-
210-
211-
ZariskiLattice : DistLattice ℓ
212-
fst ZariskiLattice = ZL
213-
DistLatticeStr.0l (snd ZariskiLattice) = 0z
214-
DistLatticeStr.1l (snd ZariskiLattice) = 1z
215-
DistLatticeStr._∨l_ (snd ZariskiLattice) = _∨z_
216-
DistLatticeStr._∧l_ (snd ZariskiLattice) = _∧z_
217-
DistLatticeStr.isDistLattice (snd ZariskiLattice) =
218-
makeIsDistLattice∧lOver∨l squash/ ∨zAssoc ∨zRid ∨zComm
219-
∧zAssoc ∧zRid ∧zComm ∧zAbsorb∨z ∧zLDist∨z
209+
(√ ⟨ α ··Fin (β ++Fin γ) ⟩ ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
210+
√ (⟨ α ⟩ ·i ⟨ β ++Fin γ ⟩) ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ _ _) ⟩
211+
√ (⟨ α ⟩ ·i (⟨ β ⟩ +i ⟨ γ ⟩)) ≡⟨ cong √ (·iRdist+i _ _ _) ⟩
212+
-- L/R-dist are swapped
213+
-- in Lattices vs Rings
214+
√ (⟨ α ⟩ ·i ⟨ β ⟩ +i ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong₂ (λ x y → √ (x +i y))
215+
(sym (FGIdealMultLemma _ _ _))
216+
(sym (FGIdealMultLemma _ _ _)) ⟩
217+
√ (⟨ α ··Fin β ⟩ +i ⟨ α ··Fin γ ⟩) ≡⟨ cong √ (sym (FGIdealAddLemma _ _ _)) ⟩
218+
√ ⟨ (α ··Fin β) ++Fin (α ··Fin γ) ⟩ ∎))
219+
220+
221+
ZariskiLattice : DistLattice ℓ
222+
fst ZariskiLattice = ZL
223+
DistLatticeStr.0l (snd ZariskiLattice) = 0z
224+
DistLatticeStr.1l (snd ZariskiLattice) = 1z
225+
DistLatticeStr._∨l_ (snd ZariskiLattice) = _∨z_
226+
DistLatticeStr._∧l_ (snd ZariskiLattice) = _∧z_
227+
DistLatticeStr.isDistLattice (snd ZariskiLattice) =
228+
makeIsDistLattice∧lOver∨l squash/ ∨zAssoc ∨zRid ∨zComm
229+
∧zAssoc ∧zRid ∧zComm ∧zAbsorb∨z ∧zLDist∨z

0 commit comments

Comments
 (0)