diff --git a/Cubical/Algebra/CommRing/FGIdeal.agda b/Cubical/Algebra/CommRing/FGIdeal.agda index 446c9bd131..9334f69c1b 100644 --- a/Cubical/Algebra/CommRing/FGIdeal.agda +++ b/Cubical/Algebra/CommRing/FGIdeal.agda @@ -11,6 +11,8 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function open import Cubical.Foundations.Transport open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Powerset using () renaming ( _∈_ to _∈ₚ_ + ; ∈-isProp to ∈ₚ-isProp) open import Cubical.Data.Empty as ⊥ open import Cubical.Data.Sigma @@ -431,3 +433,14 @@ module GeneratingPowers (R' : CommRing ℓ) (n : ℕ) where path = linearCombination R' α U ^ ((ℕsuc m) ·ℕ n) ≡⟨ cong (_^ ((ℕsuc m) ·ℕ n)) (sym p) ⟩ 1r ^ ((ℕsuc m) ·ℕ n) ≡⟨ 1ⁿ≡1 ((ℕsuc m) ·ℕ n) ⟩ 1r ∎ + + +-- principal ideals containing 1 are generated by units +module _ {R : CommRing ℓ} {f : fst R} where + private ⟨f⟩ = ⟨ replicateFinVec 1 f ⟩[ R ] + open CommRingStr (snd R) + open CommIdeal R + + containsOne→Unit : 1r ∈ ⟨f⟩ → f ∈ₚ R ˣ + containsOne→Unit = PT.rec (∈ₚ-isProp (R ˣ) f) + λ (α , 1≡α₀f+0) → α zero , solve! R ∙ sym 1≡α₀f+0 diff --git a/Cubical/Algebra/CommRing/RadicalIdeal.agda b/Cubical/Algebra/CommRing/RadicalIdeal.agda index 0fdabfb3e7..16faf4c575 100644 --- a/Cubical/Algebra/CommRing/RadicalIdeal.agda +++ b/Cubical/Algebra/CommRing/RadicalIdeal.agda @@ -4,7 +4,7 @@ module Cubical.Algebra.CommRing.RadicalIdeal where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv open import Cubical.Foundations.Function -open import Cubical.Foundations.Powerset using (⊆-isProp) +open import Cubical.Foundations.Powerset using (⊆-isProp ; ∈-isProp) open import Cubical.Foundations.HLevels open import Cubical.Data.Sigma @@ -95,7 +95,9 @@ module RadicalIdeal (R' : CommRing ℓ) where ∈→∈√ : ∀ (I : CommIdeal) (x : R) → x ∈ I → x ∈ √ I ∈→∈√ I _ x∈I = ∣ 1 , subst-∈ I (sym (·IdR _)) x∈I ∣₁ - + -- inverse direction holds for 1 + 1∈√→1∈ : ∀ (I : CommIdeal) → 1r ∈ √ I → 1r ∈ I + 1∈√→1∈ I = PT.rec (∈-isProp (fst I) _) λ (n , 1ⁿ∈I) → subst-∈ I (1ⁿ≡1 n) 1ⁿ∈I -- important lemma for characterization of the Zariski lattice open KroneckerDelta (CommRing→Ring R') diff --git a/Cubical/Algebra/DistLattice/BigOps.agda b/Cubical/Algebra/DistLattice/BigOps.agda index a812d64641..9f8f844741 100644 --- a/Cubical/Algebra/DistLattice/BigOps.agda +++ b/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' @@ -145,3 +154,12 @@ module Meet (L' : DistLattice ℓ) where ⋀Join1r : ∀ {n} → (V : FinVec L n) → ⋀ (λ i → 1l ∨l V i) ≡ 1l ⋀Join1r V = sym (⋀Joinrdist 1l V) ∙ 1lLeftAnnihilates∨l _ + + +module MeetMap {L : DistLattice ℓ} {L' : DistLattice ℓ'} (φ : DistLatticeHom L L') where + private module L = Meet L + private module L' = Meet L' + open BigOpMap (LatticeHom→MeetSemilatticeHom φ) + + pres⋀ : {n : ℕ} (U : FinVec ⟨ L ⟩ n) → φ .fst (L.⋀ U) ≡ L'.⋀ (φ .fst ∘ U) + pres⋀ = presBigOp diff --git a/Cubical/Algebra/DistLattice/Downset.agda b/Cubical/Algebra/DistLattice/Downset.agda new file mode 100644 index 0000000000..907c419732 --- /dev/null +++ b/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) diff --git a/Cubical/Algebra/Lattice/Base.agda b/Cubical/Algebra/Lattice/Base.agda index 7f411bb793..b96cf6c62e 100644 --- a/Cubical/Algebra/Lattice/Base.agda +++ b/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 diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda index c1622d2fc7..7051f72a54 100644 --- a/Cubical/Algebra/Lattice/Properties.agda +++ b/Cubical/Algebra/Lattice/Properties.agda @@ -29,25 +29,30 @@ 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 ∎ + 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 _ + 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 ∎ + 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 ∎ - 1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l - 1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _ + 1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l + 1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _ + -- Provide an interface to CommMonoid lemmas about _∧l_. + module ∧l = CommMonoidTheory (Semilattice→CommMonoid (Lattice→MeetSemilattice L')) + + ∧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 _)) ∙ ∧l.commAssocSwap x x y z module Order (L' : Lattice ℓ) where @@ -74,13 +79,16 @@ module Order (L' : Lattice ℓ) where IndPosetPath : JoinPoset ≡ MeetPoset IndPosetPath = PosetPath _ _ .fst ((idEquiv _) , isposetequiv ≤Equiv ) - -- transport inequalities from ≤m to ≤j + -- transport some inequalities from ≤m to ≤j ∧lIsMinJoin : ∀ x y z → z ≤j x → z ≤j y → z ≤j x ∧l y ∧lIsMinJoin _ _ _ z≤jx z≤jy = ≤m→≤j _ _ (∧lIsMin _ _ _ (≤j→≤m _ _ z≤jx) (≤j→≤m _ _ z≤jy)) ∧≤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 ⦃...⦄ diff --git a/Cubical/Algebra/ZariskiLattice/Properties.agda b/Cubical/Algebra/ZariskiLattice/Properties.agda new file mode 100644 index 0000000000..ba9813b866 --- /dev/null +++ b/Cubical/Algebra/ZariskiLattice/Properties.agda @@ -0,0 +1,207 @@ +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Algebra.ZariskiLattice.Properties where + + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Powerset using (ℙ) + renaming (_∈_ to _∈ₚ_ ; ∈-isProp to ∈ₚ-isProp) + +open import Cubical.Data.Nat using (ℕ) +open import Cubical.Data.Sigma.Properties +open import Cubical.Data.FinData +open import Cubical.Relation.Binary.Order.Poset + +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Localisation +open import Cubical.Algebra.CommRing.Ideal +open import Cubical.Algebra.CommRing.FGIdeal +open import Cubical.Algebra.CommRing.RadicalIdeal +open import Cubical.Tactics.CommRingSolver +open import Cubical.Algebra.Semilattice +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice +open import Cubical.Algebra.DistLattice.Downset + +open import Cubical.Algebra.ZariskiLattice.Base +open import Cubical.Algebra.ZariskiLattice.UniversalProperty + +open import Cubical.HITs.SetQuotients as SQ +import Cubical.HITs.PropositionalTruncation as PT + + +private variable ℓ : Level + +module _ (R : CommRing ℓ) where + open Iso + open CommRingStr ⦃...⦄ + open PosetStr ⦃...⦄ + + open Exponentiation R + open CommIdeal R + open RadicalIdeal R + + open ZarLat R + open ZarLatUniversalProp R + + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice)) + using (IndPoset) + + private + instance + _ = R .snd + _ = IndPoset .snd + + ⟨_⟩ : {n : ℕ} → FinVec (fst R) n → CommIdeal + ⟨ V ⟩ = ⟨ V ⟩[ R ] + + unitLemmaZarLat : ∀ f → D f ≡ D 1r → f ∈ₚ R ˣ + unitLemmaZarLat f Df≡D1 = containsOne→Unit (1∈√→1∈ _ 1∈√⟨f⟩) + where + D1≤Df : D 1r ≤ D f + D1≤Df = subst (_≤ D f) Df≡D1 (is-refl _) + + 1∈√⟨f⟩ : 1r ∈ √ ⟨ replicateFinVec 1 f ⟩ + 1∈√⟨f⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun D1≤Df .fst zero + + +module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where + open CommRingStr ⦃...⦄ + open DistLatticeStr ⦃...⦄ + open PosetStr ⦃...⦄ + + open InvertingElementsBase R + open UniversalProp f + + open ZarLat + open ZarLatUniversalProp + open IsSupport + + open DistLatticeDownset (ZariskiLattice R) + open Order (DistLattice→Lattice (ZariskiLattice R)) + open LatticeTheory (DistLattice→Lattice (ZariskiLattice R)) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (ZariskiLattice R))) + using () renaming (IndPoset to ZLRPoset) + + open MeetSemilattice (Lattice→MeetSemilattice (DistLattice→Lattice (ZariskiLattice R))) + using (≤-∧LPres ; ∧≤RCancel) + + private + instance + _ = R .snd + _ = ZariskiLattice R .snd + _ = ZLRPoset .snd + + powerLemma : ∀ fⁿ → fⁿ ∈ₚ [ f ⁿ|n≥0] → D R f ∧l D R fⁿ ≡ D R f + powerLemma fⁿ = PT.rec (squash/ _ _) + λ (n , fⁿ≡f^n) → cong (λ x → D R f ∧l D R x) fⁿ≡f^n + ∙ ≤j→≤m _ _ (supportExpIneq (isSupportD R) n f) + + locEqPowerLemma : ∀ r fⁿ → fⁿ ∈ₚ [ f ⁿ|n≥0] + → D R f ∧l D R (r · fⁿ) ≡ D R f ∧l D R r + locEqPowerLemma r fⁿ fⁿIsPow = + D R f ∧l D R (r · fⁿ) ≡⟨ cong (D R f ∧l_) (isSupportD R .·≡∧ _ _) ⟩ + D R f ∧l (D R r ∧l D R fⁿ) ≡⟨ ∧lAssoc (D R f) (D R r) (D R fⁿ) ⟩ + (D R f ∧l D R r) ∧l D R fⁿ ≡⟨ ∧l.commAssocr (D R f) (D R r) (D R fⁿ) ⟩ + (D R f ∧l D R fⁿ) ∧l D R r ≡⟨ cong (_∧l D R r) (powerLemma _ fⁿIsPow) ⟩ + D R f ∧l D R r ∎ + + locEqPowerLemma2 : ∀ r fᵐ fⁿ → fᵐ ∈ₚ [ f ⁿ|n≥0] → fⁿ ∈ₚ [ f ⁿ|n≥0] + → D R f ∧l D R (fᵐ · r · fⁿ) ≡ D R f ∧l D R r + locEqPowerLemma2 r fᵐ fⁿ fᵐIsPow fⁿIsPow = + D R f ∧l D R (fᵐ · r · fⁿ) ≡⟨ locEqPowerLemma (fᵐ · r) fⁿ fⁿIsPow ⟩ + D R f ∧l D R (fᵐ · r) ≡⟨ cong (D R f ∧l_) (isSupportD R .·≡∧ _ _) ⟩ + D R f ∧l (D R fᵐ ∧l D R r) ≡⟨ ∧lAssoc (D R f) (D R fᵐ) (D R r) ⟩ + (D R f ∧l D R fᵐ) ∧l D R r ≡⟨ cong (_∧l D R r) (powerLemma _ fᵐIsPow) ⟩ + D R f ∧l D R r ∎ + + + locDownSupp : R[1/ f ] → ↓ (D R f) + locDownSupp = + SQ.rec + (isSetΣSndProp squash/ λ x → is-prop-valued x _) + -- the actual map: r/fⁿ ↦ Dr∧Df + (λ (r , _) → (D R f ∧l D R r) , ≤m→≤j _ _ (∧≤RCancel (D R f) (D R r))) + -- coherence + λ (r , fⁿ , fⁿIsPow) (r' , fᵐ , fᵐIsPow) ((fᵏ , fᵏIsPow) , fᵏrfᵐ≡fᵏr'fⁿ) + → Σ≡Prop (λ x → is-prop-valued x _) + (sym (locEqPowerLemma2 r fᵏ fᵐ fᵏIsPow fᵐIsPow) + ∙∙ cong (λ x → D R f ∧l D R x) fᵏrfᵐ≡fᵏr'fⁿ + ∙∙ locEqPowerLemma2 r' fᵏ fⁿ fᵏIsPow fⁿIsPow) + + isSupportLocDownSupp : IsSupport R[1/ f ]AsCommRing (↓ᴰᴸ (D R f)) locDownSupp + pres0 isSupportLocDownSupp = + Σ≡Prop (λ x → is-prop-valued x _) + (cong (D R f ∧l_) (isSupportD R .pres0) ∙ 0lRightAnnihilates∧l (D R f)) + pres1 isSupportLocDownSupp = Σ≡Prop (λ x → is-prop-valued x _) (∧lRid (D R f)) + ·≡∧ isSupportLocDownSupp = + SQ.elimProp2 + (λ _ _ → DistLatticeStr.is-set (↓ᴰᴸ (D R f) .snd) _ _) + λ (r , _) (r' , _) → Σ≡Prop (λ x → is-prop-valued x _) + (cong (D R f ∧l_) (isSupportD R .·≡∧ r r') + ∙ ∧lLdist∧l (D R f) (D R r) (D R r')) + +≤∨ isSupportLocDownSupp = + SQ.elimProp2 + (λ _ _ → DistLatticeStr.is-set (↓ᴰᴸ (D R f) .snd) _ _) + λ (r , fⁿ , fⁿIsPow) (r' , fᵐ , fᵐIsPow) + → Σ≡Prop (λ x → is-prop-valued x _) + (subst ((D R f ∧l D R ((r · fᵐ) + (r' · fⁿ))) ≤_) + (path r r' fⁿ fᵐ fⁿIsPow fᵐIsPow) + (ineq r r' fⁿ fᵐ)) + where + ineq : ∀ r r' fⁿ fᵐ + → (D R f ∧l D R (r · fᵐ + r' · fⁿ)) ≤ (D R f ∧l (D R (r · fᵐ) ∨l D R (r' · fⁿ))) + ineq r r' fⁿ fᵐ = ≤m→≤j _ _ (≤-∧LPres (D R (r · fᵐ + r' · fⁿ)) + (D R (r · fᵐ) ∨l D R (r' · fⁿ)) + (D R f) + (≤j→≤m _ _ (isSupportD R .+≤∨ (r · fᵐ) (r' · fⁿ)))) + + path : ∀ r r' fⁿ fᵐ → fⁿ ∈ₚ [ f ⁿ|n≥0] → fᵐ ∈ₚ [ f ⁿ|n≥0] + → D R f ∧l (D R (r · fᵐ) ∨l D R (r' · fⁿ)) + ≡ (D R f ∧l D R r) ∨l (D R f ∧l D R r') + path r r' fⁿ fᵐ fⁿIsPow fᵐIsPow = + ∧lLdist∨l (D R f) (D R (r · fᵐ)) (D R (r' · fⁿ)) + ∙ cong₂ (_∨l_) (locEqPowerLemma r fᵐ fᵐIsPow) (locEqPowerLemma r' fⁿ fⁿIsPow) + + + -- one direction of the equivalence + locToDownHom : DistLatticeHom (ZariskiLattice R[1/ f ]AsCommRing) (↓ᴰᴸ (D R f)) + locToDownHom = ZLHasUniversalProp _ _ _ isSupportLocDownSupp .fst .fst + + toDownSupp : R .fst → ↓ (D R f) + toDownSupp = locDownSupp ∘ _/1 + + isSupportToDownSupp : IsSupport R (↓ᴰᴸ (D R f)) toDownSupp + isSupportToDownSupp = presSupportPrecomp /1AsCommRingHom _ _ isSupportLocDownSupp + + -- the map ZL R → ZL R[1/f] → ↓Df is just Df∧_ + -- does not type check without lossy unification!!! + toLocToDown≡ToDown : locToDownHom ∘dl inducedZarLatHom /1AsCommRingHom + ≡ toDownHom (D R f) + toLocToDown≡ToDown = + cong fst (isContr→isProp + (ZLHasUniversalProp R (↓ᴰᴸ (D R f)) toDownSupp isSupportToDownSupp) + (locToDownHom ∘dl (inducedZarLatHom /1AsCommRingHom) , toLocToDownComm) + (toDownHom (D R f) , toDownComm)) + where + toDownComm : toDownHom (D R f) .fst ∘ (D R) ≡ toDownSupp + toDownComm = funExt λ r → Σ≡Prop (λ x → is-prop-valued x _) refl + + toLocToDownComm : locToDownHom .fst ∘ inducedZarLatHom /1AsCommRingHom .fst ∘ D R + ≡ toDownSupp + toLocToDownComm = + locToDownHom .fst ∘ (inducedZarLatHom /1AsCommRingHom) .fst ∘ D R + + ≡⟨ cong (locToDownHom .fst ∘_) (inducedZarLatHomComm /1AsCommRingHom) ⟩ + + locToDownHom .fst ∘ D R[1/ f ]AsCommRing ∘ _/1 + + ≡⟨ ∘-assoc (locToDownHom .fst) (D R[1/ f ]AsCommRing) _/1 ⟩ + + (locToDownHom .fst ∘ D R[1/ f ]AsCommRing) ∘ _/1 + + ≡⟨ cong (_∘ _/1) (ZLHasUniversalProp _ _ _ isSupportLocDownSupp .fst .snd) ⟩ + + locDownSupp ∘ _/1 ∎ diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda index ac8798946b..b70970886c 100644 --- a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda +++ b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda @@ -91,7 +91,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where open ZarLat R' open ZarLatUniversalProp R' - open IsZarMap + open IsSupport open Join ZariskiLattice open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice)) @@ -111,9 +111,9 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where BO = Σ[ 𝔞 ∈ ZL ] (𝔞 ∈ₚ BasicOpens) basicOpensAreBasis : IsBasis ZariskiLattice BasicOpens - contains1 basicOpensAreBasis = ∣ 1r , isZarMapD .pres1 ∣₁ + contains1 basicOpensAreBasis = ∣ 1r , isSupportD .pres1 ∣₁ ∧lClosed basicOpensAreBasis 𝔞 𝔟 = map2 - λ (f , Df≡𝔞) (g , Dg≡𝔟) → (f · g) , isZarMapD .·≡∧ f g ∙ cong₂ (_∧z_) Df≡𝔞 Dg≡𝔟 + λ (f , Df≡𝔞) (g , Dg≡𝔟) → (f · g) , isSupportD .·≡∧ f g ∙ cong₂ (_∧z_) Df≡𝔞 Dg≡𝔟 ⋁Basis basicOpensAreBasis = elimProp (λ _ → isPropPropTrunc) Σhelper where Σhelper : (a : Σ[ n ∈ ℕ ] FinVec R n) diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda b/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda index a01e5d6971..61bc82976c 100644 --- a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda +++ b/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda @@ -92,7 +92,7 @@ module _ (R' : CommRing ℓ) where open ZarLat R' open ZarLatUniversalProp R' - open IsZarMap + open IsSupport open Join ZariskiLattice open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice)) @@ -115,9 +115,9 @@ module _ (R' : CommRing ℓ) where BO = Σ[ 𝔞 ∈ ZL ] (𝔞 ∈ₚ BasicOpens) basicOpensAreBasis : IsBasis ZariskiLattice BasicOpens - contains1 basicOpensAreBasis = ∣ 1r , isZarMapD .pres1 ∣₁ + contains1 basicOpensAreBasis = ∣ 1r , isSupportD .pres1 ∣₁ ∧lClosed basicOpensAreBasis 𝔞 𝔟 = map2 - λ (f , Df≡𝔞) (g , Dg≡𝔟) → (f · g) , isZarMapD .·≡∧ f g ∙ cong₂ (_∧z_) Df≡𝔞 Dg≡𝔟 + λ (f , Df≡𝔞) (g , Dg≡𝔟) → (f · g) , isSupportD .·≡∧ f g ∙ cong₂ (_∧z_) Df≡𝔞 Dg≡𝔟 ⋁Basis basicOpensAreBasis = elimProp (λ _ → isPropPropTrunc) Σhelper where Σhelper : (a : Σ[ n ∈ ℕ ] FinVec R n) @@ -189,7 +189,7 @@ module _ (R' : CommRing ℓ) where _ = BasisStructurePShf canonical0∈BO : 0z ∈ₚ BasicOpens - canonical0∈BO = ∣ 0r , isZarMapD .pres0 ∣₁ + canonical0∈BO = ∣ 0r , isSupportD .pres0 ∣₁ canonical0∈BO≡0∈BO : canonical0∈BO ≡ 0∈BO canonical0∈BO≡0∈BO = BasicOpens 0z .snd _ _ diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda index 3983ab834e..4355fe899c 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda @@ -9,7 +9,7 @@ open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Univalence open import Cubical.Foundations.HLevels open import Cubical.Foundations.Transport -open import Cubical.Foundations.Powerset using (ℙ ; ⊆-refl-consequence) +open import Cubical.Foundations.Powerset using (ℙ ; ⊆-refl-consequence) renaming (_∈_ to _∈ₚ_) import Cubical.Data.Empty as ⊥ open import Cubical.Data.Bool hiding (_≤_) @@ -57,6 +57,7 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where open Sum (CommRing→Ring R') open CommRingTheory R' open Exponentiation R' + open Units R' open DistLatticeStr (L' .snd) renaming (is-set to isSetL) open Join L' @@ -69,8 +70,8 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where R = fst R' L = fst L' - record IsZarMap (d : R → L) : Type (ℓ-max ℓ ℓ') where - constructor iszarmap + record IsSupport (d : R → L) : Type (ℓ-max ℓ ℓ') where + constructor issupport field pres0 : d 0r ≡ 0l @@ -89,20 +90,27 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where d·LCancel : ∀ x y → d (x · y) ≤ d y d·LCancel x y = subst (λ a → a ≤ d y) (sym (·≡∧ x y)) (∧≤LCancelJoin _ _) + d·RCancel : ∀ x y → d (x · y) ≤ d x + d·RCancel x y = subst (λ a → a ≤ d x) (sym (·≡∧ x y)) (∧≤RCancelJoin _ _) + linearCombination≤LCancel : {n : ℕ} (α β : FinVec R n) → d (linearCombination R' α β) ≤ ⋁ (d ∘ β) linearCombination≤LCancel α β = is-trans _ _ _ (∑≤⋁ (λ i → α i · β i)) (≤-⋁Ext _ _ λ i → d·LCancel (α i) (β i)) - ZarMapIdem : ∀ (n : ℕ) (x : R) → d (x ^ (suc n)) ≡ d x - ZarMapIdem zero x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) pres1 ∙∙ ∧lRid _ - ZarMapIdem (suc n) x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) (ZarMapIdem n x) ∙∙ ∧lIdem _ + supportUnit : ∀ x → x ∈ₚ Rˣ → d x ≡ 1l + supportUnit x (x⁻¹ , xx⁻¹≡1) = is-antisym _ _ (1lRightAnnihilates∨l _) + (subst (_≤ d x) (cong d xx⁻¹≡1 ∙ pres1) (d·RCancel _ _)) + + supportIdem : ∀ (n : ℕ) (x : R) → d (x ^ (suc n)) ≡ d x + supportIdem zero x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) pres1 ∙∙ ∧lRid _ + supportIdem (suc n) x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) (supportIdem n x) ∙∙ ∧lIdem _ - ZarMapExpIneq : ∀ (n : ℕ) (x : R) → d x ≤ d (x ^ n) - ZarMapExpIneq zero x = cong (d x ∨l_) pres1 ∙∙ 1lRightAnnihilates∨l _ ∙∙ sym pres1 - ZarMapExpIneq (suc n) x = subst (λ y → d x ≤ y) (sym (ZarMapIdem _ x)) (∨lIdem _) + supportExpIneq : ∀ (n : ℕ) (x : R) → d x ≤ d (x ^ n) + supportExpIneq zero x = cong (d x ∨l_) pres1 ∙∙ 1lRightAnnihilates∨l _ ∙∙ sym pres1 + supportExpIneq (suc n) x = subst (λ y → d x ≤ y) (sym (supportIdem _ x)) (∨lIdem _) - -- the crucial lemma about "Zariski maps" + -- the crucial lemma about support maps open CommIdeal R' open RadicalIdeal R' open isCommIdeal @@ -110,18 +118,45 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal ⟨ V ⟩ = ⟨ V ⟩[ R' ] - ZarMapRadicalIneq : ∀ {n : ℕ} (α : FinVec R n) (x : R) + supportRadicalIneq : ∀ {n : ℕ} (α : FinVec R n) (x : R) → x ∈ √ ⟨ α ⟩ → d x ≤ ⋁ (d ∘ α) - ZarMapRadicalIneq α x = PT.elim (λ _ → isSetL _ _) + supportRadicalIneq α x = PT.elim (λ _ → isSetL _ _) (uncurry (λ n → (PT.elim (λ _ → isSetL _ _) (uncurry (curriedHelper n))))) where curriedHelper : (n : ℕ) (β : FinVec R _) → x ^ n ≡ linearCombination R' β α → d x ≤ ⋁ (d ∘ α) - curriedHelper n β xⁿ≡∑βα = d x ≤⟨ ZarMapExpIneq n x ⟩ + curriedHelper n β xⁿ≡∑βα = d x ≤⟨ supportExpIneq n x ⟩ d (x ^ n) ≤⟨ subst (λ y → y ≤ ⋁ (d ∘ α)) (sym (cong d xⁿ≡∑βα)) (linearCombination≤LCancel β α) ⟩ ⋁ (d ∘ α) ◾ +-- precomposition with a ring hom +module _ {A B : CommRing ℓ} (φ : CommRingHom A B) + (L : DistLattice ℓ) (d : B .fst → L .fst) where + open IsSupport + open CommRingStr ⦃...⦄ + open DistLatticeStr ⦃...⦄ + open IsRingHom + private + instance + _ = L .snd + _ = A .snd + _ = B .snd + + presSupportPrecomp : IsSupport B L d → IsSupport A L (d ∘ fst φ) + pres0 (presSupportPrecomp dIsSupport) = cong d (φ .snd .pres0) ∙ dIsSupport .pres0 + pres1 (presSupportPrecomp dIsSupport) = cong d (φ .snd .pres1) ∙ dIsSupport .pres1 + ·≡∧ (presSupportPrecomp dIsSupport) x y = cong d (φ .snd .pres· x y) + ∙ dIsSupport .·≡∧ (φ .fst x) (φ .fst y) + +≤∨ (presSupportPrecomp dIsSupport) x y = + let open JoinSemilattice + (Lattice→JoinSemilattice (DistLattice→Lattice L)) + in subst (λ z → z ≤ (d (φ .fst x)) ∨l (d (φ .fst y))) + (sym (cong d (φ .snd .pres+ x y))) + (dIsSupport .+≤∨ (φ .fst x) (φ .fst y)) + + + module ZarLatUniversalProp (R' : CommRing ℓ) where open CommRingStr (snd R') open RingTheory (CommRing→Ring R') @@ -135,7 +170,7 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where open ProdFin R' open ZarLat R' - open IsZarMap + open IsSupport private R = fst R' @@ -146,11 +181,11 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where D : R → ZL D x = [ 1 , replicateFinVec 1 x ] -- λ x → √⟨x⟩ - isZarMapD : IsZarMap R' ZariskiLattice D - pres0 isZarMapD = eq/ _ _ (≡→∼ (cong √ (0FGIdeal _ ∙ sym (emptyFGIdeal _ _)))) - pres1 isZarMapD = refl - ·≡∧ isZarMapD x y = cong {B = λ _ → ZL} (λ U → [ 1 , U ]) (Length1··Fin x y) - +≤∨ isZarMapD x y = eq/ _ _ (≡→∼ (cong √ (CommIdeal≡Char + isSupportD : IsSupport R' ZariskiLattice D + pres0 isSupportD = eq/ _ _ (≡→∼ (cong √ (0FGIdeal _ ∙ sym (emptyFGIdeal _ _)))) + pres1 isSupportD = refl + ·≡∧ isSupportD x y = cong {B = λ _ → ZL} (λ U → [ 1 , U ]) (Length1··Fin x y) + +≤∨ isSupportD x y = eq/ _ _ (≡→∼ (cong √ (CommIdeal≡Char (inclOfFGIdeal _ 3Vec ⟨ 2Vec ⟩ 3Vec⊆2Vec) (inclOfFGIdeal _ 2Vec ⟨ 3Vec ⟩ 2Vec⊆3Vec)))) where @@ -169,18 +204,18 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where -- defintion of the universal property hasZarLatUniversalProp : (L : DistLattice ℓ') (D : R → fst L) - → IsZarMap R' L D + → IsSupport R' L D → Type _ hasZarLatUniversalProp {ℓ' = ℓ'} L D _ = ∀ (L' : DistLattice ℓ') (d : R → fst L') - → IsZarMap R' L' d + → IsSupport R' L' d → ∃![ χ ∈ DistLatticeHom L L' ] (fst χ) ∘ D ≡ d - isPropZarLatUniversalProp : (L : DistLattice ℓ') (D : R → fst L) (isZarMapD : IsZarMap R' L D) - → isProp (hasZarLatUniversalProp L D isZarMapD) - isPropZarLatUniversalProp L D isZarMapD = isPropΠ3 (λ _ _ _ → isPropIsContr) + isPropZarLatUniversalProp : (L : DistLattice ℓ') (D : R → fst L) (isSupportD : IsSupport R' L D) + → isProp (hasZarLatUniversalProp L D isSupportD) + isPropZarLatUniversalProp L D isSupportD = isPropΠ3 (λ _ _ _ → isPropIsContr) - ZLHasUniversalProp : hasZarLatUniversalProp ZariskiLattice D isZarMapD - ZLHasUniversalProp L' d isZarMapd = (χ , funExt χcomp) , χunique + ZLHasUniversalProp : hasZarLatUniversalProp ZariskiLattice D isSupportD + ZLHasUniversalProp L' d isSupportd = (χ , funExt χcomp) , χunique where open DistLatticeStr (snd L') renaming (is-set to isSetL) open LatticeTheory (DistLattice→Lattice L') @@ -206,18 +241,18 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where ineq1 : ⋁ (d ∘ α) ≤ ⋁ (d ∘ β) ineq1 = ⋁IsMax (d ∘ α) (⋁ (d ∘ β)) - λ i → ZarMapRadicalIneq isZarMapd β (α i) (√FGIdealCharLImpl α ⟨ β ⟩ incl1 i) + λ i → supportRadicalIneq isSupportd β (α i) (√FGIdealCharLImpl α ⟨ β ⟩ incl1 i) incl2 : √ ⟨ β ⟩ ⊆ √ ⟨ α ⟩ incl2 = ⊆-refl-consequence _ _ (cong fst (∼→≡ α∼β)) .snd ineq2 : ⋁ (d ∘ β) ≤ ⋁ (d ∘ α) ineq2 = ⋁IsMax (d ∘ β) (⋁ (d ∘ α)) - λ i → ZarMapRadicalIneq isZarMapd α (β i) (√FGIdealCharLImpl β ⟨ α ⟩ incl2 i) + λ i → supportRadicalIneq isSupportd α (β i) (√FGIdealCharLImpl β ⟨ α ⟩ incl2 i) pres0 (snd χ) = refl - pres1 (snd χ) = ∨lRid _ ∙ isZarMapd .pres1 + pres1 (snd χ) = ∨lRid _ ∙ isSupportd .pres1 pres∨l (snd χ) = elimProp2 (λ _ _ → isSetL _ _) (uncurry (λ n α → uncurry (curriedHelper n α))) where curriedHelper : (n : ℕ) (α : FinVec R n) (m : ℕ) (β : FinVec R m) @@ -253,7 +288,7 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where ⋁ (d ∘ (λ j → α zero · β j)) ∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β)) - ≡⟨ cong (_∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))) (⋁Ext (λ j → isZarMapd .·≡∧ (α zero) (β j))) ⟩ + ≡⟨ cong (_∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))) (⋁Ext (λ j → isSupportd .·≡∧ (α zero) (β j))) ⟩ ⋁ (λ j → d (α zero) ∧l d (β j)) ∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β)) @@ -303,10 +338,10 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where -- the map induced by applying the universal property to the Zariski lattice -- itself is the identity hom - ZLUniversalPropCorollary : ZLHasUniversalProp ZariskiLattice D isZarMapD .fst .fst + ZLUniversalPropCorollary : ZLHasUniversalProp ZariskiLattice D isSupportD .fst .fst ≡ idDistLatticeHom ZariskiLattice ZLUniversalPropCorollary = cong fst - (ZLHasUniversalProp ZariskiLattice D isZarMapD .snd + (ZLHasUniversalProp ZariskiLattice D isSupportD .snd (idDistLatticeHom ZariskiLattice , refl)) -- and another corollary @@ -320,7 +355,7 @@ module _ {A B : CommRing ℓ} (φ : CommRingHom A B) where open ZarLat open ZarLatUniversalProp - open IsZarMap + open IsSupport open CommRingStr ⦃...⦄ open DistLatticeStr ⦃...⦄ open IsRingHom @@ -332,22 +367,18 @@ module _ {A B : CommRing ℓ} (φ : CommRingHom A B) where _ = (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)) + Dcomp = D B ∘ fst φ + + isSupportDcomp : IsSupport A (ZariskiLattice B) Dcomp + isSupportDcomp = presSupportPrecomp φ (ZariskiLattice B) (D B) (isSupportD B) inducedZarLatHom : DistLatticeHom (ZariskiLattice A) (ZariskiLattice B) - inducedZarLatHom = ZLHasUniversalProp A (ZariskiLattice B) Dcomp isZarMapDcomp .fst .fst + inducedZarLatHom = + ZLHasUniversalProp A (ZariskiLattice B) Dcomp isSupportDcomp .fst .fst + + inducedZarLatHomComm : inducedZarLatHom .fst ∘ D A ≡ Dcomp + inducedZarLatHomComm = + ZLHasUniversalProp A (ZariskiLattice B) Dcomp isSupportDcomp .fst .snd -- functoriality module _ (A : CommRing ℓ) where @@ -359,7 +390,7 @@ module _ (A : CommRing ℓ) where inducedZarLatHomId = cong fst (ZLHasUniversalProp A (ZariskiLattice A) (Dcomp (idCommRingHom A)) - (isZarMapDcomp (idCommRingHom A)) .snd + (isSupportDcomp (idCommRingHom A)) .snd (idDistLatticeHom (ZariskiLattice A) , refl)) module _ {A B C : CommRing ℓ} (φ : CommRingHom A B) (ψ : CommRingHom B C) where @@ -371,6 +402,6 @@ module _ {A B C : CommRing ℓ} (φ : CommRingHom A B) (ψ : CommRingHom B C) wh inducedZarLatHomSeq = cong fst (ZLHasUniversalProp A (ZariskiLattice C) (Dcomp (ψ ∘cr φ)) - (isZarMapDcomp (ψ ∘cr φ)) .snd + (isSupportDcomp (ψ ∘cr φ)) .snd (inducedZarLatHom ψ ∘dl inducedZarLatHom φ , funExt (λ _ → ∨lRid _))) where open DistLatticeStr (ZariskiLattice C .snd) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index a1a669082e..faec14ebef 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -23,20 +23,24 @@ open import Cubical.Data.FinData open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Localisation +open import Cubical.Algebra.CommRing.RadicalIdeal open import Cubical.Algebra.Semilattice open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Algebra.DistLattice.BigOps open import Cubical.Algebra.ZariskiLattice.Base open import Cubical.Algebra.ZariskiLattice.UniversalProperty +open import Cubical.Algebra.ZariskiLattice.Properties -open import Cubical.Categories.Category +open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Functor open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.CommRings open import Cubical.Categories.Instances.DistLattice open import Cubical.Categories.Instances.DistLattices open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.Site.Cover open import Cubical.Categories.Site.Coverage open import Cubical.Categories.Site.Sheaf open import Cubical.Categories.Site.Instances.ZariskiCommRing @@ -246,7 +250,7 @@ module _ {ℓ : Level} where isAffine : (X : ℤFunctor) → Type (ℓ-suc ℓ) isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X - -- TODO: 𝔸¹ ≅ Sp ℤ[x] and 𝔾ₘ ≅ Sp ℤ[x,x⁻¹] as first examples of affine schemes + -- TODO: 𝔸¹ ≅ Sp ℤ[x] and 𝔾ₘ ≅ Sp ℤ[x,x⁻¹] ≅ D(x) ↪ 𝔸¹ as first examples of affine schemes -- The unit is an equivalence iff the ℤ-functor is affine. @@ -296,13 +300,55 @@ module _ {ℓ : Level} where open ZarLat open ZarLatUniversalProp - -- the Zariski lattice classifying compact open subobjects + -- the Zariski lattice functor classifying compact open subobjects ZarLatFun : ℤFunctor {ℓ = ℓ} F-ob ZarLatFun A = ZL A , SQ.squash/ F-hom ZarLatFun φ = inducedZarLatHom φ .fst F-id ZarLatFun {A} = cong fst (inducedZarLatHomId A) F-seq ZarLatFun φ ψ = cong fst (inducedZarLatHomSeq φ ψ) + -- this is a separated presheaf + -- (TODO: prove this a sheaf) + isSeparatedZarLatFun : isSeparated zariskiCoverage ZarLatFun + isSeparatedZarLatFun A (unimodvec n f 1∈⟨f₁,⋯,fₙ⟩) u w uRest≡wRest = + u ≡⟨ sym (∧lLid _) ⟩ + 1l ∧l u ≡⟨ congL _∧l_ D1≡⋁Dfᵢ ⟩ + (⋁ (D A ∘ f)) ∧l u ≡⟨ ⋁Meetldist _ _ ⟩ + ⋁ (λ i → D A (f i) ∧l u) ≡⟨ ⋁Ext Dfᵢ∧u≡Dfᵢ∧w ⟩ + ⋁ (λ i → D A (f i) ∧l w) ≡⟨ sym (⋁Meetldist _ _) ⟩ + (⋁ (D A ∘ f)) ∧l w ≡⟨ congL _∧l_ (sym D1≡⋁Dfᵢ) ⟩ + 1l ∧l w ≡⟨ ∧lLid _ ⟩ + w ∎ + where + open Join (ZariskiLattice A) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (ZariskiLattice A))) + using (IndPoset) + open LatticeTheory (DistLattice→Lattice (ZariskiLattice A)) + open PosetStr (IndPoset .snd) + open IsSupport (isSupportD A) + open RadicalIdeal A + instance + _ = A .snd + _ = ZariskiLattice A .snd + + D1≡⋁Dfᵢ : 1l ≡ ⋁ (D A ∘ f) + D1≡⋁Dfᵢ = is-antisym _ _ + (supportRadicalIneq f 1r (∈→∈√ _ _ 1∈⟨f₁,⋯,fₙ⟩)) + (1lRightAnnihilates∨l _) + + Dfᵢ∧u≡Dfᵢ∧w : ∀ i → D A (f i) ∧l u ≡ D A (f i) ∧l w + Dfᵢ∧u≡Dfᵢ∧w i = + D A (f i) ∧l u + ≡⟨ sym (cong fst (funExt⁻ (cong fst toLocToDown≡ToDown) u)) ⟩ + locToDownHom .fst (inducedZarLatHom /1AsCommRingHom .fst u) .fst + ≡⟨ cong (λ x → locToDownHom .fst x .fst) (uRest≡wRest i) ⟩ + locToDownHom .fst (inducedZarLatHom /1AsCommRingHom .fst w) .fst + ≡⟨ cong fst (funExt⁻ (cong fst toLocToDown≡ToDown) w) ⟩ + D A (f i) ∧l w ∎ + where + open InvertingElementsBase.UniversalProp A (f i) + open LocDownSetIso A (f i) + CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) CompactOpen X = X ⇒ ZarLatFun @@ -413,7 +459,7 @@ module _ {ℓ : Level} where module _ (X : ℤFunctor) where - open isIso + open isIsoC private instance _ = (CompOpenDistLattice .F-ob X) .snd compOpenTopNatIso : NatIso X ⟦ 1l ⟧ᶜᵒ @@ -425,24 +471,16 @@ module _ {ℓ : Level} where module _ (X : ℤFunctor) where + open isIsoC open Join (CompOpenDistLattice .F-ob X) open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) open PosetStr (IndPoset .snd) hiding (_≤_) - open LatticeTheory ⦃...⦄ -- ((DistLattice→Lattice (CompOpenDistLattice .F-ob X))) + open LatticeTheory ⦃...⦄ private instance _ = (CompOpenDistLattice .F-ob X) .snd - record AffineCover : Type (ℓ-suc ℓ) where - field - n : ℕ - U : FinVec (CompactOpen X) n - covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ - isAffineU : ∀ i → isAffineCompactOpen (U i) - - hasAffineCover : Type (ℓ-suc ℓ) - hasAffineCover = ∥ AffineCover ∥₁ - - -- the structure sheaf - private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op + compOpenGlobalIncl : (U : CompactOpen X) → ⟦ U ⟧ᶜᵒ ⇒ X + N-ob (compOpenGlobalIncl U) A = fst + N-hom (compOpenGlobalIncl U) φ = refl compOpenIncl : {U V : CompactOpen X} → V ≤ U → ⟦ V ⟧ᶜᵒ ⇒ ⟦ U ⟧ᶜᵒ N-ob (compOpenIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) = x , path @@ -458,6 +496,30 @@ module _ {ℓ : Level} where D A 1r ∎ N-hom (compOpenIncl V≤U) φ = funExt λ x → Σ≡Prop (λ _ → squash/ _ _) refl + -- this is essentially U∧_ + compOpenDownHom : (U : CompactOpen X) + → DistLatticeHom (CompOpenDistLattice .F-ob X) + (CompOpenDistLattice .F-ob ⟦ U ⟧ᶜᵒ) + compOpenDownHom U = CompOpenDistLattice .F-hom (compOpenGlobalIncl U) + + module _ {U V : CompactOpen X} (V≤U : V ≤ U) where + -- We need this separate definition to avoid termination checker issues, + -- but we don't understand why. + private + compOpenDownHomFun : (A : CommRing ℓ) + → ⟦ V ⟧ᶜᵒ .F-ob A .fst + → ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ .F-ob A .fst + compOpenDownHomFun A v = (compOpenIncl V≤U ⟦ A ⟧) v , snd v + + compOpenDownHomNatIso : NatIso ⟦ V ⟧ᶜᵒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ + N-ob (trans compOpenDownHomNatIso) = compOpenDownHomFun + N-hom (trans compOpenDownHomNatIso) _ = + funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl) + inv (nIso compOpenDownHomNatIso A) ((x , Ux≡D1) , Vx≡D1) = x , Vx≡D1 + sec (nIso compOpenDownHomNatIso A) = + funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl) + ret (nIso compOpenDownHomNatIso A) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + compOpenInclId : ∀ {U : CompactOpen X} → compOpenIncl (is-refl U) ≡ idTrans ⟦ U ⟧ᶜᵒ compOpenInclId = makeNatTransPath (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) @@ -467,32 +529,267 @@ module _ {ℓ : Level} where compOpenInclSeq _ _ = makeNatTransPath (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) + + -- the structure sheaf + private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op + strDLSh : Functor COᵒᵖ (CommRingsCategory {ℓ = ℓ-suc ℓ}) F-ob strDLSh U = 𝓞 .F-ob ⟦ U ⟧ᶜᵒ F-hom strDLSh U≥V = 𝓞 .F-hom (compOpenIncl U≥V) F-id strDLSh = cong (𝓞 .F-hom) compOpenInclId ∙ 𝓞 .F-id F-seq strDLSh _ _ = cong (𝓞 .F-hom) (compOpenInclSeq _ _) ∙ 𝓞 .F-seq _ _ - -- the canonical one element affine cover of a representable + + -- def. affine cover and locality for definition of qcqs-scheme + module _ (X : ℤFunctor) where + open isIsoC + open Join (CompOpenDistLattice .F-ob X) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) + open PosetStr (IndPoset .snd) hiding (_≤_) + open LatticeTheory ⦃...⦄ + private instance _ = (CompOpenDistLattice .F-ob X) .snd + + record AffineCover : Type (ℓ-suc ℓ) where + field + n : ℕ + U : FinVec (CompactOpen X) n + covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ + isAffineU : ∀ i → isAffineCompactOpen (U i) + + hasAffineCover : Type (ℓ-suc ℓ) + hasAffineCover = ∥ AffineCover ∥₁ + + -- qcqs-schemes as Zariski sheaves (local ℤ-functors) with an affine cover in the sense above + isLocal : ℤFunctor → Type (ℓ-suc ℓ) + isLocal X = isSheaf zariskiCoverage X + + -- Compact opens of Zariski sheaves are sheaves + presLocalCompactOpen : (X : ℤFunctor) (U : CompactOpen X) → isLocal X → isLocal ⟦ U ⟧ᶜᵒ + presLocalCompactOpen X U isLocalX R um@(unimodvec _ f _) = isoToIsEquiv isoU + where + open Coverage zariskiCoverage + open InvertingElementsBase R + instance _ = R .snd + + fᵢCoverR = covers R .snd um + + isoX : Iso (X .F-ob R .fst) (CompatibleFamily X fᵢCoverR) + isoX = equivToIso (elementToCompatibleFamily _ _ , isLocalX R um) + + compatibleFamIncl : (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) → (CompatibleFamily X fᵢCoverR) + compatibleFamIncl fam = (fst ∘ fst fam) + , λ i j B φ ψ φψComm → cong fst (fam .snd i j B φ ψ φψComm) + + compatibleFamIncl≡ : ∀ (y : Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r) + → compatibleFamIncl (elementToCompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR y) + ≡ elementToCompatibleFamily X fᵢCoverR (y .fst) + compatibleFamIncl≡ y = CompatibleFamily≡ _ _ _ _ λ _ → refl + + isoU : Iso (Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r) + (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) + fun isoU = elementToCompatibleFamily _ _ + fst (inv isoU fam) = isoX .inv (compatibleFamIncl fam) + snd (inv isoU fam) = -- U (x) ≡ D(1) + -- knowing that U(x/1)¸≡ D(1) in R[1/fᵢ] + let x = isoX .inv (compatibleFamIncl fam) in + isSeparatedZarLatFun R um (U .N-ob R x) (D R 1r) + λ i → let open UniversalProp (f i) + instance _ = R[1/ (f i) ]AsCommRing .snd in + + inducedZarLatHom /1AsCommRingHom .fst (U .N-ob R x) + + ≡⟨ funExt⁻ (sym (U .N-hom /1AsCommRingHom)) x ⟩ + + U .N-ob R[1/ (f i) ]AsCommRing (X .F-hom /1AsCommRingHom x) + + ≡⟨ cong (U .N-ob R[1/ f i ]AsCommRing) + (funExt⁻ (cong fst (isoX .rightInv (compatibleFamIncl fam))) i) ⟩ + + U .N-ob R[1/ (f i) ]AsCommRing (fam .fst i .fst) + + ≡⟨ fam .fst i .snd ⟩ + + D R[1/ (f i) ]AsCommRing 1r + + ≡⟨ sym (inducedZarLatHom /1AsCommRingHom .snd .pres1) ⟩ + + inducedZarLatHom /1AsCommRingHom .fst (D R 1r) ∎ + + rightInv isoU fam = + Σ≡Prop (λ _ → isPropIsCompatibleFamily _ _ _) + (funExt λ i → Σ≡Prop (λ _ → squash/ _ _) + (funExt⁻ (cong fst + (isoX .rightInv (compatibleFamIncl fam))) i)) + leftInv isoU y = Σ≡Prop (λ _ → squash/ _ _) + (cong (isoX .inv) (compatibleFamIncl≡ y) + ∙ isoX .leftInv (y .fst)) + + + -- definition of quasi-compact, quasi-separated schemes + isQcQsScheme : ℤFunctor → Type (ℓ-suc ℓ) + isQcQsScheme X = isLocal X × hasAffineCover X + + + -- affine schemes are qcqs-schemes module _ (A : CommRing ℓ) where open AffineCover private instance _ = (CompOpenDistLattice ⟅ Sp ⟅ A ⟆ ⟆) .snd + -- the canonical one element affine cover of a representable singlAffineCover : AffineCover (Sp .F-ob A) n singlAffineCover = 1 U singlAffineCover zero = 1l covers singlAffineCover = ∨lRid _ isAffineU singlAffineCover zero = ∣ A , compOpenTopNatIso (Sp ⟅ A ⟆) ∣₁ + isQcQsSchemeAffine : isQcQsScheme (Sp .F-ob A) + fst isQcQsSchemeAffine = isSubcanonicalZariskiCoverage A + snd isQcQsSchemeAffine = ∣ singlAffineCover ∣₁ - -- qcqs-schemes as Zariski sheaves (local ℤ-functors) with an affine cover in the sense above - isLocal : ℤFunctor → Type (ℓ-suc ℓ) - isLocal X = isSheaf zariskiCoverage X - isQcQsScheme : ℤFunctor → Type (ℓ-suc ℓ) - isQcQsScheme X = isLocal X × hasAffineCover X +-- standard affine opens +-- TODO: separate file? +module StandardOpens {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where - -- affine schemes are qcqs-schemes - isQcQsSchemeAffine : ∀ (A : CommRing ℓ) → isQcQsScheme (Sp .F-ob A) - fst (isQcQsSchemeAffine A) = isSubcanonicalZariskiCoverage A - snd (isQcQsSchemeAffine A) = ∣ singlAffineCover A ∣₁ + open Iso + open Functor + open NatTrans + open NatIso + open isIsoC + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open IsRingHom + open RingHoms + open IsLatticeHom + open ZarLat + + open InvertingElementsBase R + open UniversalProp f + + private module ZL = ZarLatUniversalProp + + private + instance + _ = R .snd + + D : CompactOpen (Sp ⟅ R ⟆) + D = yonedaᴾ ZarLatFun R .inv (ZL.D R f) + + SpR[1/f]≅⟦Df⟧ : NatIso (Sp .F-ob R[1/ f ]AsCommRing) ⟦ D ⟧ᶜᵒ + N-ob (trans SpR[1/f]≅⟦Df⟧) B φ = (φ ∘r /1AsCommRingHom) , ∨lRid _ ∙ path + where + open CommRingHomTheory φ + open IsSupport (ZL.isSupportD B) + instance + _ = B .snd + _ = ZariskiLattice B .snd + + isUnitφ[f/1] : φ .fst (f /1) ∈ B ˣ + isUnitφ[f/1] = RingHomRespInv (f /1) ⦃ S/1⊆S⁻¹Rˣ f ∣ 1 , sym (·IdR f) ∣₁ ⦄ + + path : ZL.D B (φ .fst (f /1)) ≡ 1l + path = supportUnit _ isUnitφ[f/1] + + N-hom (trans SpR[1/f]≅⟦Df⟧) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ refl) + + inv (nIso SpR[1/f]≅⟦Df⟧ B) (φ , Dφf≡D1) = invElemUniversalProp B φ isUnitφf .fst .fst + where + instance _ = ZariskiLattice B .snd + isUnitφf : φ .fst f ∈ B ˣ + isUnitφf = unitLemmaZarLat B (φ $r f) (sym (∨lRid _) ∙ Dφf≡D1) + + sec (nIso SpR[1/f]≅⟦Df⟧ B) = + funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ (invElemUniversalProp _ _ _ .fst .snd)) + ret (nIso SpR[1/f]≅⟦Df⟧ B) = + funExt λ φ → cong fst (invElemUniversalProp B (φ ∘r /1AsCommRingHom) _ .snd (φ , refl)) + + isAffineD : isAffineCompactOpen D + isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁ + + +-- compact opens of affine schemes are qcqs-schemes +module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where + + open StandardOpens + + open Iso + open Functor + open NatTrans + open NatIso + open isIsoC + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open PosetStr ⦃...⦄ + open IsRingHom + open RingHoms + open IsLatticeHom + open ZarLat + + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset; ind≤bigOp) + open InvertingElementsBase R + open Join + open JoinMap + open AffineCover + private module ZL = ZarLatUniversalProp + + private + instance + _ = R .snd + _ = ZariskiLattice R .snd + _ = CompOpenDistLattice .F-ob (Sp .F-ob R) .snd + _ = CompOpenDistLattice .F-ob ⟦ W ⟧ᶜᵒ .snd + _ = IndPoset .snd + + w : ZL R + w = yonedaᴾ ZarLatFun R .fun W + + -- yoneda is a lattice homomorphsim + isHomYoneda : IsLatticeHom (DistLattice→Lattice (ZariskiLattice R) .snd) + (yonedaᴾ ZarLatFun R .inv) + (DistLattice→Lattice (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) .snd) + pres0 isHomYoneda = makeNatTransPath (funExt₂ (λ _ _ → refl)) + pres1 isHomYoneda = + makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres1)) + pres∨l isHomYoneda u v = + makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres∨l u v)) + pres∧l isHomYoneda u v = + makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres∧l u v)) + + module _ {n : ℕ} + (f : FinVec (fst R) n) + (⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W) where + + Df≤W : ∀ i → D R (f i) ≤ W + Df≤W i = subst (D R (f i) ≤_) ⋁Df≡W (ind≤bigOp (D R ∘ f) i) + + toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ + AffineCover.n toAffineCover = n + U toAffineCover i = compOpenDownHom (Sp ⟅ R ⟆) W .fst (D R (f i)) + covers toAffineCover = sym (pres⋁ (compOpenDownHom (Sp ⟅ R ⟆) W) (D R ∘ f)) + ∙ cong (compOpenDownHom (Sp ⟅ R ⟆) W .fst) ⋁Df≡W + ∙ makeNatTransPath (funExt₂ (λ _ → snd)) + isAffineU toAffineCover i = + ∣ _ , seqNatIso (SpR[1/f]≅⟦Df⟧ R (f i)) (compOpenDownHomNatIso _ (Df≤W i)) ∣₁ + + module _ {n : ℕ} + (f : FinVec (fst R) n) + (⋁Df≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ f) ≡ w) where + + private + ⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W + ⋁Df≡W = sym (pres⋁ (_ , isHomYoneda) (ZL.D R ∘ f)) + ∙ cong (yonedaᴾ ZarLatFun R .inv) ⋁Df≡w + ∙ yonedaᴾ ZarLatFun R .leftInv W + + makeAffineCoverCompOpenOfAffine : AffineCover ⟦ W ⟧ᶜᵒ + makeAffineCoverCompOpenOfAffine = toAffineCover f ⋁Df≡W + + hasAffineCoverCompOpenOfAffine : hasAffineCover ⟦ W ⟧ᶜᵒ + hasAffineCoverCompOpenOfAffine = PT.map truncHelper ([]surjective w) + where + truncHelper : Σ[ n,f ∈ Σ ℕ (FinVec (fst R)) ] [ n,f ] ≡ w → AffineCover ⟦ W ⟧ᶜᵒ + truncHelper ((n , f) , [n,f]≡w) = makeAffineCoverCompOpenOfAffine f (ZL.⋁D≡ R f ∙ [n,f]≡w) + + isQcQsSchemeCompOpenOfAffine : isQcQsScheme ⟦ W ⟧ᶜᵒ + fst isQcQsSchemeCompOpenOfAffine = presLocalCompactOpen _ _ (isSubcanonicalZariskiCoverage R) + snd isQcQsSchemeCompOpenOfAffine = hasAffineCoverCompOpenOfAffine diff --git a/Cubical/Papers/AffineSchemes.agda b/Cubical/Papers/AffineSchemes.agda index beb6a5859d..fc3d95bf73 100644 --- a/Cubical/Papers/AffineSchemes.agda +++ b/Cubical/Papers/AffineSchemes.agda @@ -164,7 +164,7 @@ open FinGenIdeals using (FGIdealMultLemma) open ZariskiLatDef using (ZariskiLattice) -- support map D and universal property -open ZariskiLatUnivProp using (D ; isZarMapD) +open ZariskiLatUnivProp using (D ; isSupportD) open ZariskiLatUnivProp using (ZLHasUniversalProp) -- D(g) ≤ D(f) ⇔ isContr (R-Hom R[1/f] R[1/g]) diff --git a/Cubical/Relation/Binary/Order/Poset/Properties.agda b/Cubical/Relation/Binary/Order/Poset/Properties.agda index 4e56fc7d47..a3122fb1ca 100644 --- a/Cubical/Relation/Binary/Order/Poset/Properties.agda +++ b/Cubical/Relation/Binary/Order/Poset/Properties.agda @@ -8,6 +8,8 @@ open import Cubical.Functions.Embedding open import Cubical.HITs.PropositionalTruncation as ∥₁ +open import Cubical.Data.Sigma + open import Cubical.Relation.Binary.Base open import Cubical.Relation.Binary.Order.Poset.Base open import Cubical.Relation.Binary.Order.Preorder.Base @@ -69,3 +71,20 @@ Poset→StrictPoset : Poset ℓ ℓ' → StrictPoset ℓ (ℓ-max ℓ ℓ') Poset→StrictPoset (_ , pos) = _ , strictposetstr (BinaryRelation.IrreflKernel (PosetStr._≤_ pos)) (isPoset→isStrictPosetIrreflKernel (PosetStr.isPoset pos)) + + +module PosetDownset (P' : Poset ℓ ℓ') where + private P = fst P' + open PosetStr (snd P') + + ↓ : P → Type (ℓ-max ℓ ℓ') + ↓ u = Σ[ v ∈ P ] v ≤ u + + ↓ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ' + fst (↓ᴾ u) = ↓ u + PosetStr._≤_ (snd (↓ᴾ u)) v w = v .fst ≤ w .fst + PosetStr.isPoset (snd (↓ᴾ u)) = + isPosetInduced + (PosetStr.isPoset (snd P')) + _ + (EmbeddingΣProp (λ a → is-prop-valued _ _))