diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda index be3dd9d176..37a56b2037 100644 --- a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda +++ b/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) diff --git a/Cubical/Algebra/CommRing/Localisation/Limit.agda b/Cubical/Algebra/CommRing/Localisation/Limit.agda index 316c491e84..c8c755f512 100644 --- a/Cubical/Algebra/CommRing/Localisation/Limit.agda +++ b/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 ⦃...⦄ diff --git a/Cubical/Algebra/CommRing/Properties.agda b/Cubical/Algebra/CommRing/Properties.agda index b8d2033797..726774187f 100644 --- a/Cubical/Algebra/CommRing/Properties.agda +++ b/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') diff --git a/Cubical/Algebra/DistLattice/BigOps.agda b/Cubical/Algebra/DistLattice/BigOps.agda index a812d64641..1d5dfca316 100644 --- a/Cubical/Algebra/DistLattice/BigOps.agda +++ b/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' 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..4b28da2f88 100644 --- a/Cubical/Algebra/Lattice/Properties.agda +++ b/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 ⦃...⦄ diff --git a/Cubical/Algebra/Monoid/BigOp.agda b/Cubical/Algebra/Monoid/BigOp.agda index 803074aaf2..66ef69a12f 100644 --- a/Cubical/Algebra/Monoid/BigOp.agda +++ b/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)) diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda new file mode 100644 index 0000000000..6d5deef4d5 --- /dev/null +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda @@ -0,0 +1,239 @@ +{- + + A ℤ-functor is just a functor from rings to sets. + + NOTE: we consider the functor category [ Ring ℓ , Set ℓ ] for some universe level ℓ + and not [ Ring ℓ , Set (ℓ+1) ] as is done in + "Introduction to Algebraic Geometry and Algebraic Groups" + by Demazure & Gabriel! + + The category of ℤ-functors contains the category of (qcqs-) schemes + as a full subcategory and satisfies a "universal property" + similar to the one of schemes: + + There is an adjunction 𝓞 ⊣ᵢ Sp + (relative to the inclusion i : CommRing ℓ → CommRing (ℓ+1)) + between the "global sections functor" 𝓞 + and the fully-faithful embedding of affines Sp, + whose counit is a natural isomorphism + +-} + + +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.HLevels + +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat using (ℕ) + +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing + +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.Functors +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Yoneda +open import Cubical.Categories.Site.Sheaf +open import Cubical.Categories.Site.Instances.ZariskiCommRing + +open import Cubical.HITs.PropositionalTruncation as PT + + +open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) + + +module _ {ℓ : Level} where + + open Functor + open NatTrans + open CommRingStr ⦃...⦄ + open IsRingHom + + -- using the naming conventions of Demazure & Gabriel + ℤFunctor = Functor (CommRingsCategory {ℓ = ℓ}) (SET ℓ) + ℤFUNCTOR = FUNCTOR (CommRingsCategory {ℓ = ℓ}) (SET ℓ) + + -- uses that double op is original category definitionally + Sp : Functor (CommRingsCategory {ℓ = ℓ} ^op) ℤFUNCTOR + Sp = YO {C = (CommRingsCategory {ℓ = ℓ} ^op)} + + -- Affine schemes are merely representable functors + -- TODO: by univalence it should be fine to take untruncated Σ + isAffine : ℤFunctor → Type (ℓ-suc ℓ) + isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X + + -- a ℤ-functor that is a sheaf wrt the Zariski coverage is called local + isLocal : ℤFunctor → Type (ℓ-suc ℓ) + isLocal X = isSheaf zariskiCoverage X + + -- the forgetful functor + -- aka the affine line + -- (aka the representable of ℤ[x]) + 𝔸¹ : ℤFunctor + 𝔸¹ = ForgetfulCommRing→Set + + -- the "global sections" functor + 𝓞 : Functor ℤFUNCTOR (CommRingsCategory {ℓ = ℓ-suc ℓ} ^op) + fst (F-ob 𝓞 X) = X ⇒ 𝔸¹ + + -- ring struncture induced by internal ring object 𝔸¹ + N-ob (CommRingStr.0r (snd (F-ob 𝓞 X))) A _ = 0r + where instance _ = A .snd + N-hom (CommRingStr.0r (snd (F-ob 𝓞 X))) φ = funExt λ _ → sym (φ .snd .pres0) + + N-ob (CommRingStr.1r (snd (F-ob 𝓞 X))) A _ = 1r + where instance _ = A .snd + N-hom (CommRingStr.1r (snd (F-ob 𝓞 X))) φ = funExt λ _ → sym (φ .snd .pres1) + + N-ob ((snd (F-ob 𝓞 X) CommRingStr.+ α) β) A x = α .N-ob A x + β .N-ob A x + where instance _ = A .snd + N-hom ((snd (F-ob 𝓞 X) CommRingStr.+ α) β) {x = A} {y = B} φ = funExt path + where + instance + _ = A .snd + _ = B .snd + path : ∀ x → α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) + ≡ φ .fst (α .N-ob A x + β .N-ob A x) + path x = α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _+_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ + φ .fst (α .N-ob A x) + φ .fst (β .N-ob A x) + ≡⟨ sym (φ .snd .pres+ _ _) ⟩ + φ .fst (α .N-ob A x + β .N-ob A x) ∎ + + N-ob ((snd (F-ob 𝓞 X) CommRingStr.· α) β) A x = α .N-ob A x · β .N-ob A x + where instance _ = A .snd + N-hom ((snd (F-ob 𝓞 X) CommRingStr.· α) β) {x = A} {y = B} φ = funExt path + where + instance + _ = A .snd + _ = B .snd + path : ∀ x → α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) + ≡ φ .fst (α .N-ob A x · β .N-ob A x) + path x = α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _·_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ + φ .fst (α .N-ob A x) · φ .fst (β .N-ob A x) + ≡⟨ sym (φ .snd .pres· _ _) ⟩ + φ .fst (α .N-ob A x · β .N-ob A x) ∎ + + N-ob ((CommRingStr.- snd (F-ob 𝓞 X)) α) A x = - α .N-ob A x + where instance _ = A .snd + N-hom ((CommRingStr.- snd (F-ob 𝓞 X)) α) {x = A} {y = B} φ = funExt path + where + instance + _ = A .snd + _ = B .snd + path : ∀ x → - α .N-ob B (X .F-hom φ x) ≡ φ .fst (- α .N-ob A x) + path x = - α .N-ob B (X .F-hom φ x) ≡⟨ cong -_ (funExt⁻ (α .N-hom φ) x) ⟩ + - φ .fst (α .N-ob A x) ≡⟨ sym (φ .snd .pres- _) ⟩ + φ .fst (- α .N-ob A x) ∎ + + CommRingStr.isCommRing (snd (F-ob 𝓞 X)) = makeIsCommRing + isSetNatTrans + (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Assoc _ _ _)) + (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+IdR _)) + (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+InvR _)) + (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Comm _ _)) + (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Assoc _ _ _)) + (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·IdR _)) + (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·DistR+ _ _ _)) + (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Comm _ _)) + + -- action on natural transformations + fst (F-hom 𝓞 α) = α ●ᵛ_ + pres0 (snd (F-hom 𝓞 α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres1 (snd (F-hom 𝓞 α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres+ (snd (F-hom 𝓞 α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres· (snd (F-hom 𝓞 α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres- (snd (F-hom 𝓞 α)) _ = makeNatTransPath (funExt₂ λ _ _ → refl) + + -- functoriality of 𝓞 + F-id 𝓞 = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq 𝓞 _ _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + +-- we get a relative adjunction 𝓞 ⊣ᵢ Sp +-- with respect to the inclusion i : CommRing ℓ → CommRing (ℓ+1) +module AdjBij {ℓ : Level} where + + open Functor + open NatTrans + open Iso + open IsRingHom + + private module _ {A : CommRing ℓ} {X : ℤFunctor} where + _♭ : CommRingHom A (𝓞 .F-ob X) → X ⇒ Sp .F-ob A + fst (N-ob (φ ♭) B x) a = φ .fst a .N-ob B x + + pres0 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres0) + pres1 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres1) + pres+ (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres+ _ _) + pres· (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres· _ _) + pres- (snd (N-ob (φ ♭) B x)) _ = cong (λ y → y .N-ob B x) (φ .snd .pres- _) + + N-hom (φ ♭) ψ = funExt (λ x → RingHom≡ (funExt λ a → funExt⁻ (φ .fst a .N-hom ψ) x)) + + + -- the other direction is just precomposition modulo Yoneda + _♯ : X ⇒ Sp .F-ob A → CommRingHom A (𝓞 .F-ob X) + fst (α ♯) a = α ●ᵛ yonedaᴾ 𝔸¹ A .inv a + + pres0 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres0) + pres1 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres1) + pres+ (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres+ _ _) + pres· (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres· _ _) + pres- (snd (α ♯)) _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres- _) + + + -- the two maps are inverse to each other + ♭♯Id : ∀ (α : X ⇒ Sp .F-ob A) → ((α ♯) ♭) ≡ α + ♭♯Id _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) + + ♯♭Id : ∀ (φ : CommRingHom A (𝓞 .F-ob X)) → ((φ ♭) ♯) ≡ φ + ♯♭Id _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + 𝓞⊣SpIso : {A : CommRing ℓ} {X : ℤFunctor {ℓ}} + → Iso (CommRingHom A (𝓞 .F-ob X)) (X ⇒ Sp .F-ob A) + fun 𝓞⊣SpIso = _♭ + inv 𝓞⊣SpIso = _♯ + rightInv 𝓞⊣SpIso = ♭♯Id + leftInv 𝓞⊣SpIso = ♯♭Id + + 𝓞⊣SpNatℤFunctor : {A : CommRing ℓ} {X Y : ℤFunctor {ℓ}} (α : X ⇒ Sp .F-ob A) (β : Y ⇒ X) + → (β ●ᵛ α) ♯ ≡ (𝓞 .F-hom β) ∘cr (α ♯) + 𝓞⊣SpNatℤFunctor _ _ = RingHom≡ (funExt (λ _ → makeNatTransPath (funExt₂ (λ _ _ → refl)))) + + 𝓞⊣SpNatCommRing : {X : ℤFunctor {ℓ}} {A B : CommRing ℓ} + (φ : CommRingHom A (𝓞 .F-ob X)) (ψ : CommRingHom B A) + → (φ ∘cr ψ) ♭ ≡ (φ ♭) ●ᵛ Sp .F-hom ψ + 𝓞⊣SpNatCommRing _ _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) + + -- right relative adjunction induces a counit, + -- which is an equivalence + private + ε : (A : CommRing ℓ) → CommRingHom A ((𝓞 ∘F Sp) .F-ob A) + ε A = (idTrans (Sp .F-ob A)) ♯ + + 𝓞⊣SpCounitEquiv : (A : CommRing ℓ) → CommRingEquiv A ((𝓞 ∘F Sp) .F-ob A) + fst (𝓞⊣SpCounitEquiv A) = isoToEquiv theIso + where + theIso : Iso (A .fst) ((𝓞 ∘F Sp) .F-ob A .fst) + fun theIso = ε A .fst + inv theIso = yonedaᴾ 𝔸¹ A .fun + rightInv theIso α = ℤFUNCTOR .⋆IdL _ ∙ yonedaᴾ 𝔸¹ A .leftInv α + leftInv theIso a = path -- I get yellow otherwise + where + path : yonedaᴾ 𝔸¹ A .fun ((idTrans (Sp .F-ob A)) ●ᵛ yonedaᴾ 𝔸¹ A .inv a) ≡ a + path = cong (yonedaᴾ 𝔸¹ A .fun) (ℤFUNCTOR .⋆IdL _) ∙ yonedaᴾ 𝔸¹ A .rightInv a + snd (𝓞⊣SpCounitEquiv A) = ε A .snd diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda new file mode 100644 index 0000000000..a976787235 --- /dev/null +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda @@ -0,0 +1,382 @@ +{- + + The definition of compact open subfunctors of a ℤ-functor X: + + U ↪ Sp(A) is compact open if it is given by a f.g. ideal of A, + i.e. if ∃ f₁, ... ,fₙ : A s.t. for all rings B: + U(B) = { φ : Hom(A,B) | ⟨ φf₁ , ... , φfₙ ⟩ = B } + + U ↪ X is compact open, if pulling back along any A-valued point + Sp(A) → X gives a compact open of Sp(A). + + By observing that compact open subfunctors of affine schemes + are in 1-1 correspondence with radicals of f.g. ideals, + we get that compact open subfunctors are classified by the + ℤ-functor that sends a ring to its Zariski lattice. + +-} + + +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.HLevels + + +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat using (ℕ) + +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.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty +open import Cubical.AlgebraicGeometry.ZariskiLattice.Properties +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base + +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 +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Yoneda + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetQuotients as SQ + +open import Cubical.Relation.Binary.Order.Poset + + +open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) + +module _ {ℓ : Level} where + + open Iso + open Functor + open NatTrans + open NatIso + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open IsRingHom + open IsLatticeHom + open ZarLat + open ZarLatUniversalProp + + -- 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 + + -- the induced subfunctor + ⟦_⟧ᶜᵒ : {X : ℤFunctor} (U : CompactOpen X) → ℤFunctor + F-ob (⟦_⟧ᶜᵒ {X = X} U) A = (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D A 1r) + , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ + where instance _ = snd A + F-hom (⟦_⟧ᶜᵒ {X = X} U) {x = A} {y = B} φ (x , Ux≡D1) = (X .F-hom φ x) , path + where + instance + _ = A .snd + _ = B .snd + open IsLatticeHom + path : U .N-ob B (X .F-hom φ x) ≡ D B 1r + path = U .N-ob B (X .F-hom φ x) ≡⟨ funExt⁻ (U .N-hom φ) x ⟩ + ZarLatFun .F-hom φ (U .N-ob A x) ≡⟨ cong (ZarLatFun .F-hom φ) Ux≡D1 ⟩ + ZarLatFun .F-hom φ (D A 1r) ≡⟨ inducedZarLatHom φ .snd .pres1 ⟩ + D B 1r ∎ + F-id (⟦_⟧ᶜᵒ {X = X} U) = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) + (funExt⁻ (X .F-id) (x .fst))) + F-seq (⟦_⟧ᶜᵒ {X = X} U) φ ψ = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) + (funExt⁻ (X .F-seq φ ψ) (x .fst))) + + + isAffineCompactOpen : {X : ℤFunctor} (U : CompactOpen X) → Type (ℓ-suc ℓ) + isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ + + -- the (big) dist. lattice of compact opens + CompOpenDistLattice : Functor ℤFUNCTOR (DistLatticesCategory {ℓ = ℓ-suc ℓ} ^op) + fst (F-ob CompOpenDistLattice X) = CompactOpen X + + -- lattice structure induce by internal lattice object ZarLatFun + N-ob (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) A _ = 0l + where instance _ = ZariskiLattice A .snd + N-hom (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) _ = funExt λ _ → refl + + N-ob (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) A _ = 1l + where instance _ = ZariskiLattice A .snd + N-hom (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path + where + instance + _ = A .snd + _ = B .snd + _ = ZariskiLattice B .snd + path : D B 1r ≡ D B (φ .fst 1r) ∨l 0l + path = cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _) + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = U .N-ob A x ∨l V .N-ob A x + where instance _ = ZariskiLattice A .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = funExt path + where + instance + _ = ZariskiLattice A .snd + _ = ZariskiLattice B .snd + path : ∀ x → U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) + ≡ ZarLatFun .F-hom φ (U .N-ob A x ∨l V .N-ob A x) + path x = U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _∨l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ + ZarLatFun .F-hom φ (U .N-ob A x) ∨l ZarLatFun .F-hom φ (V .N-ob A x) + ≡⟨ sym (inducedZarLatHom φ .snd .pres∨l _ _) ⟩ + ZarLatFun .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) A x = U .N-ob A x ∧l V .N-ob A x + where instance _ = ZariskiLattice A .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = funExt path + where + instance + _ = ZariskiLattice A .snd + _ = ZariskiLattice B .snd + path : ∀ x → U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) + ≡ ZarLatFun .F-hom φ (U .N-ob A x ∧l V .N-ob A x) + path x = U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _∧l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ + ZarLatFun .F-hom φ (U .N-ob A x) ∧l ZarLatFun .F-hom φ (V .N-ob A x) + ≡⟨ sym (inducedZarLatHom φ .snd .pres∧l _ _) ⟩ + ZarLatFun .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ + + DistLatticeStr.isDistLattice (snd (F-ob CompOpenDistLattice X)) = makeIsDistLattice∧lOver∨l + isSetNatTrans + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lComm _ _))) + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lComm _ _))) + (λ _ _ → makeNatTransPath (funExt₂ -- don't know why ∧lAbsorb∨l doesn't work + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.absorb _ _ .snd))) + (λ _ _ _ → makeNatTransPath (funExt₂ -- same here + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) + + -- (contravariant) action on morphisms + fst (F-hom CompOpenDistLattice α) = α ●ᵛ_ + pres0 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres1 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∨l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∧l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + + -- functoriality + F-id CompOpenDistLattice = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq CompOpenDistLattice _ _ = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + + + -- useful constructions/lemmas + 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 + + -- better name? + X≅⟦1⟧ : NatIso X ⟦ 1l ⟧ᶜᵒ + N-ob (trans X≅⟦1⟧) _ φ = φ , refl + N-hom (trans X≅⟦1⟧) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + inv (nIso X≅⟦1⟧ B) = fst + sec (nIso X≅⟦1⟧ B) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + ret (nIso X≅⟦1⟧ B) = funExt λ _ → refl + + 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 + where + instance + _ = A .snd + _ = ZariskiLattice A .snd + _ = DistLattice→Lattice (ZariskiLattice A) + path : U .N-ob A x ≡ D A 1r + path = U .N-ob A x ≡⟨ funExt⁻ (funExt⁻ (cong N-ob (sym V≤U)) A) x ⟩ + V .N-ob A x ∨l U .N-ob A x ≡⟨ cong (_∨l U .N-ob A x) Vx≡D1 ⟩ + D A 1r ∨l U .N-ob A x ≡⟨ 1lLeftAnnihilates∨l _ ⟩ + 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)) + + compOpenInclSeq : ∀ {U V W : CompactOpen X} (U≤V : U ≤ V) (V≤W : V ≤ W) + → compOpenIncl (is-trans _ _ _ U≤V V≤W) + ≡ compOpenIncl U≤V ●ᵛ compOpenIncl V≤W + compOpenInclSeq _ _ = makeNatTransPath + (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) + + -- the structure sheaf + -- TODO: prove that this is a dist. lattice 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 _ _ + + -- important lemma + -- 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)) diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda new file mode 100644 index 0000000000..963eafdaaf --- /dev/null +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda @@ -0,0 +1,209 @@ +{- + + Compact open subfunctors of qcqs-schemes are qcqs-schemes (TODO!!!) + The proof proceeds by + 1. Defining standard/basic compact opens of affines and proving that they are affine + 2. Proving that arbitrary compact opens of affines are qcqs-schemes + +-} +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.HLevels + + +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat using (ℕ) + +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.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty +open import Cubical.AlgebraicGeometry.ZariskiLattice.Properties +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme + +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 +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Yoneda + + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetQuotients as SQ + +open import Cubical.Relation.Binary.Order.Poset + +open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) + + + +-- standard affine opens +module StandardOpens {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where + + 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/AlgebraicGeometry/Functorial/ZFunctors/QcQsScheme.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/QcQsScheme.agda new file mode 100644 index 0000000000..3736891d3e --- /dev/null +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/QcQsScheme.agda @@ -0,0 +1,97 @@ +{- + + A qcqs-scheme is a ℤ-functor that is local (a Zariski-sheaf) + and has an affine cover, where that notion of cover is given + by the lattice structure of compact open subfunctors + +-} + +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.HLevels + + +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat using (ℕ) + +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.AlgebraicGeometry.Functorial.ZFunctors.Base +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen + +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 +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Yoneda + + +open import Cubical.HITs.PropositionalTruncation as PT + +open import Cubical.Relation.Binary.Order.Poset + +open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) + +module _ {ℓ : Level} (X : ℤFunctor {ℓ = ℓ}) where + open Functor + open DistLatticeStr ⦃...⦄ + open Join (CompOpenDistLattice .F-ob X) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) + 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 ∥₁ + + isQcQsScheme : Type (ℓ-suc ℓ) + isQcQsScheme = isLocal X × hasAffineCover + + +-- affine schemes are qcqs-schemes +module _ {ℓ : Level} (A : CommRing ℓ) where + open Functor + open DistLatticeStr ⦃...⦄ + open AffineCover + private instance _ = (CompOpenDistLattice .F-ob (Sp .F-ob 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 , X≅⟦1⟧ (Sp .F-ob A) ∣₁ + + isQcQsSchemeAffine : isQcQsScheme (Sp .F-ob A) + fst isQcQsSchemeAffine = isSubcanonicalZariskiCoverage A + snd isQcQsSchemeAffine = ∣ singlAffineCover ∣₁ diff --git a/Cubical/Algebra/ZariskiLattice/Base.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda similarity index 99% rename from Cubical/Algebra/ZariskiLattice/Base.agda rename to Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda index 7bc8b026f9..8dd80cab40 100644 --- a/Cubical/Algebra/ZariskiLattice/Base.agda +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda @@ -1,5 +1,5 @@ {-# OPTIONS --safe --lossy-unification #-} -module Cubical.Algebra.ZariskiLattice.Base where +module Cubical.AlgebraicGeometry.ZariskiLattice.Base where open import Cubical.Foundations.Prelude diff --git a/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda new file mode 100644 index 0000000000..d27a3ab230 --- /dev/null +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda @@ -0,0 +1,255 @@ +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.AlgebraicGeometry.ZariskiLattice.Properties where + + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +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) + renaming (_∈_ to _∈ₚ_ ; ∈-isProp to ∈ₚ-isProp) + +import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Bool hiding (_≤_) +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ + ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc + ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm + ; ·-identityʳ to ·ℕ-rid) +open import Cubical.Data.Sigma.Base +open import Cubical.Data.Sigma.Properties +open import Cubical.Data.FinData +open import Cubical.Data.Unit +open import Cubical.Relation.Nullary +open import Cubical.Relation.Binary +open import Cubical.Relation.Binary.Order.Poset + +open import Cubical.Algebra.Ring +open import Cubical.Algebra.Ring.Properties +open import Cubical.Algebra.Ring.BigOps +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Localisation +open import Cubical.Algebra.CommRing.BinomialThm +open import Cubical.Algebra.CommRing.Ideal +open import Cubical.Algebra.CommRing.FGIdeal +open import Cubical.Algebra.CommRing.RadicalIdeal +open import Cubical.Tactics.CommRingSolver.Reflection +open import Cubical.Algebra.Semilattice +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice +open import Cubical.Algebra.DistLattice.Basis +open import Cubical.Algebra.DistLattice.BigOps +open import Cubical.Algebra.DistLattice.Downset +open import Cubical.Algebra.Matrix + +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty + +open import Cubical.HITs.SetQuotients as SQ +open import Cubical.HITs.PropositionalTruncation as PT + + +private variable ℓ : Level + +module _ (R : CommRing ℓ) where + open Iso + open CommRingStr ⦃...⦄ + open DistLatticeStr ⦃...⦄ + open PosetStr ⦃...⦄ + + open RingTheory (CommRing→Ring R) + open Sum (CommRing→Ring R) + open CommRingTheory R + open Exponentiation R + open BinomialThm R + open CommIdeal R + open RadicalIdeal R + open isCommIdeal + open ProdFin R + + open ZarLat R + open ZarLatUniversalProp R + open IsSupport isSupportD + + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice)) + using (IndPoset) + + private + instance + _ = R .snd + _ = ZariskiLattice .snd + _ = IndPoset .snd + + ⟨_⟩ : {n : ℕ} → FinVec (fst R) n → CommIdeal + ⟨ V ⟩ = ⟨ V ⟩[ R ] + + unitLemmaZarLat : ∀ f → D f ≡ D 1r → f ∈ₚ R ˣ + unitLemmaZarLat f Df≡D1 = PT.rec (∈ₚ-isProp (R ˣ) f) radicalHelper 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 + + radicalHelper : Σ[ n ∈ ℕ ] 1r ^ n ∈ ⟨ replicateFinVec 1 f ⟩ → f ∈ₚ R ˣ + radicalHelper (n , 1ⁿ∈⟨f⟩) = PT.rec (∈ₚ-isProp (R ˣ) f) fgHelper 1ⁿ∈⟨f⟩ + where + fgHelper : Σ[ α ∈ FinVec (fst R) 1 ] 1r ^ n ≡ linearCombination R α (replicateFinVec 1 f) + → f ∈ₚ R ˣ + fgHelper (α , 1ⁿ≡α₀f+0) = α zero , path + where + useSolver : ∀ f α₀ → f · α₀ ≡ α₀ · f + 0r + useSolver = solve R + + path : f · α zero ≡ 1r + path = f · α zero ≡⟨ useSolver _ _ ⟩ + α zero · f + 0r ≡⟨ sym 1ⁿ≡α₀f+0 ⟩ + 1r ^ n ≡⟨ 1ⁿ≡1 n ⟩ + 1r ∎ + + + +module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where + open Iso + open CommRingStr ⦃...⦄ + open DistLatticeStr ⦃...⦄ + open PosetStr ⦃...⦄ + + open Exponentiation R + 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 + _ = R[1/ f ]AsCommRing .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ⁿ ≡⟨ ∧lCommAssocr (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/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda similarity index 98% rename from Cubical/Algebra/ZariskiLattice/StructureSheaf.agda rename to Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda index 2b53e779a5..188fc9b72d 100644 --- a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda @@ -8,7 +8,7 @@ -} {-# OPTIONS --safe --lossy-unification #-} -module Cubical.Algebra.ZariskiLattice.StructureSheaf where +module Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf where open import Cubical.Foundations.Prelude @@ -56,8 +56,9 @@ open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Algebra.DistLattice.Basis open import Cubical.Algebra.DistLattice.BigOps -open import Cubical.Algebra.ZariskiLattice.Base -open import Cubical.Algebra.ZariskiLattice.UniversalProperty + +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty open import Cubical.Categories.Category.Base hiding (_[_,_]) open import Cubical.Categories.Functor @@ -91,7 +92,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 +112,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/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda similarity index 98% rename from Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda rename to Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda index 01a8dcd11f..7ee9203bed 100644 --- a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda @@ -9,7 +9,7 @@ -} {-# OPTIONS --safe --lossy-unification #-} -module Cubical.Algebra.ZariskiLattice.StructureSheafPullback where +module Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback where open import Cubical.Foundations.Prelude @@ -59,8 +59,9 @@ open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Algebra.DistLattice.Basis open import Cubical.Algebra.DistLattice.BigOps -open import Cubical.Algebra.ZariskiLattice.Base -open import Cubical.Algebra.ZariskiLattice.UniversalProperty + +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty open import Cubical.Categories.Category.Base hiding (_[_,_]) open import Cubical.Categories.Functor @@ -92,7 +93,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 +116,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 +190,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/AlgebraicGeometry/ZariskiLattice/UniversalProperty.agda similarity index 76% rename from Cubical/Algebra/ZariskiLattice/UniversalProperty.agda rename to Cubical/AlgebraicGeometry/ZariskiLattice/UniversalProperty.agda index 351562674d..0cfa62000b 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/UniversalProperty.agda @@ -1,5 +1,5 @@ {-# OPTIONS --safe --lossy-unification #-} -module Cubical.Algebra.ZariskiLattice.UniversalProperty where +module Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty where open import Cubical.Foundations.Prelude @@ -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 (_≤_) @@ -41,7 +41,7 @@ open import Cubical.Algebra.DistLattice.Basis open import Cubical.Algebra.DistLattice.BigOps open import Cubical.Algebra.Matrix -open import Cubical.Algebra.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base open import Cubical.HITs.SetQuotients as SQ open import Cubical.HITs.PropositionalTruncation as PT @@ -58,6 +58,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' @@ -70,7 +71,7 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where R = fst R' L = fst L' - record IsZarMap (d : R → L) : Type (ℓ-max ℓ ℓ') where + record IsSupport (d : R → L) : Type (ℓ-max ℓ ℓ') where constructor iszarmap field @@ -90,18 +91,25 @@ 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" open CommIdeal R' @@ -111,18 +119,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') @@ -136,7 +171,7 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where open ProdFin R' open ZarLat R' - open IsZarMap + open IsSupport private R = fst R' @@ -147,11 +182,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 @@ -170,18 +205,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') @@ -207,18 +242,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) @@ -254,7 +289,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 β)) @@ -304,10 +339,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 @@ -321,7 +356,7 @@ module _ {A B : CommRing ℓ} (φ : CommRingHom A B) where open ZarLat open ZarLatUniversalProp - open IsZarMap + open IsSupport open CommRingStr ⦃...⦄ open DistLatticeStr ⦃...⦄ open IsRingHom @@ -333,22 +368,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 @@ -360,7 +391,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 @@ -372,6 +403,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/CommRings.agda b/Cubical/Categories/Instances/CommRings.agda index 4b9353cabe..326022b5ce 100644 --- a/Cubical/Categories/Instances/CommRings.agda +++ b/Cubical/Categories/Instances/CommRings.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} +{-# OPTIONS --safe --lossy-unification #-} module Cubical.Categories.Instances.CommRings where open import Cubical.Foundations.Prelude @@ -105,6 +105,24 @@ module _ {ℓ : Level} where snd (fst (snd TerminalCommRing y)) = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl) snd (snd TerminalCommRing y) f = RingHom≡ (funExt (λ _ → refl)) + open RingTheory + trivialIsTerminalCommRing : ∀ (R : CommRing ℓ) + → R .snd .0r ≡ R .snd .1r + → isTerminal CommRingsCategory R + fst (fst (trivialIsTerminalCommRing R 0≡1 A)) _ = R .snd .0r + pres0 (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) = refl + pres1 (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) = 0≡1 + pres+ (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) _ _ = sym (R .snd .+IdR _) + pres· (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) _ _ = + sym (0RightAnnihilates (CommRing→Ring R) _) + pres- (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) _ = + sym (0Selfinverse (CommRing→Ring R)) + snd (trivialIsTerminalCommRing R 0≡1 A) f = + RingHom≡ (funExt λ x → sym (0RightAnnihilates (CommRing→Ring R) _) + ∙∙ cong (R .snd ._·_ (f .fst x)) 0≡1 + ∙∙ R .snd .·IdR _) + + open Pullback {- diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda deleted file mode 100644 index 701f7c4020..0000000000 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ /dev/null @@ -1,450 +0,0 @@ -{- - - The impredicative way to define functorial qcqs-schemes (over Spec(ℤ)) - --} -{-# OPTIONS --safe --lossy-unification #-} -module Cubical.Categories.Instances.ZFunctors where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Function -open import Cubical.Foundations.Powerset -open import Cubical.Foundations.HLevels - - -open import Cubical.Functions.FunExtEquiv - -open import Cubical.Data.Sigma -open import Cubical.Data.Nat using (ℕ) - -open import Cubical.Data.FinData - -open import Cubical.Algebra.Ring -open import Cubical.Algebra.CommRing -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.Categories.Category -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.NaturalTransformation -open import Cubical.Categories.Yoneda - -open import Cubical.HITs.PropositionalTruncation as PT -open import Cubical.HITs.SetQuotients as SQ - -open import Cubical.Relation.Binary.Order.Poset - -open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) - -private - variable - ℓ ℓ' ℓ'' : Level - - -module _ {ℓ : Level} where - - open Functor - open NatTrans - open CommRingStr ⦃...⦄ - open IsRingHom - - -- using the naming conventions of Nieper-Wisskirchen - ℤFunctor = Functor (CommRingsCategory {ℓ = ℓ}) (SET ℓ) - ℤFUNCTOR = FUNCTOR (CommRingsCategory {ℓ = ℓ}) (SET ℓ) - - -- Yoneda in the notation of Demazure-Gabriel, - -- uses that double op is original category definitionally - Sp : Functor (CommRingsCategory {ℓ = ℓ} ^op) ℤFUNCTOR - Sp = YO {C = (CommRingsCategory {ℓ = ℓ} ^op)} - - -- the forgetful functor - -- aka the affine line - -- (aka the representable of ℤ[x]) - 𝔸¹ : ℤFunctor - 𝔸¹ = ForgetfulCommRing→Set - - -- the global sections functor - Γ : Functor ℤFUNCTOR (CommRingsCategory {ℓ = ℓ-suc ℓ} ^op) - fst (F-ob Γ X) = X ⇒ 𝔸¹ - - -- ring struncture induced by internal ring object 𝔸¹ - N-ob (CommRingStr.0r (snd (F-ob Γ X))) A _ = 0r - where instance _ = A .snd - N-hom (CommRingStr.0r (snd (F-ob Γ X))) φ = funExt λ _ → sym (φ .snd .pres0) - - N-ob (CommRingStr.1r (snd (F-ob Γ X))) A _ = 1r - where instance _ = A .snd - N-hom (CommRingStr.1r (snd (F-ob Γ X))) φ = funExt λ _ → sym (φ .snd .pres1) - - N-ob ((snd (F-ob Γ X) CommRingStr.+ α) β) A x = α .N-ob A x + β .N-ob A x - where instance _ = A .snd - N-hom ((snd (F-ob Γ X) CommRingStr.+ α) β) {x = A} {y = B} φ = funExt path - where - instance - _ = A .snd - _ = B .snd - path : ∀ x → α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) - ≡ φ .fst (α .N-ob A x + β .N-ob A x) - path x = α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) - ≡⟨ cong₂ _+_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ - φ .fst (α .N-ob A x) + φ .fst (β .N-ob A x) - ≡⟨ sym (φ .snd .pres+ _ _) ⟩ - φ .fst (α .N-ob A x + β .N-ob A x) ∎ - - N-ob ((snd (F-ob Γ X) CommRingStr.· α) β) A x = α .N-ob A x · β .N-ob A x - where instance _ = A .snd - N-hom ((snd (F-ob Γ X) CommRingStr.· α) β) {x = A} {y = B} φ = funExt path - where - instance - _ = A .snd - _ = B .snd - path : ∀ x → α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) - ≡ φ .fst (α .N-ob A x · β .N-ob A x) - path x = α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) - ≡⟨ cong₂ _·_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ - φ .fst (α .N-ob A x) · φ .fst (β .N-ob A x) - ≡⟨ sym (φ .snd .pres· _ _) ⟩ - φ .fst (α .N-ob A x · β .N-ob A x) ∎ - - N-ob ((CommRingStr.- snd (F-ob Γ X)) α) A x = - α .N-ob A x - where instance _ = A .snd - N-hom ((CommRingStr.- snd (F-ob Γ X)) α) {x = A} {y = B} φ = funExt path - where - instance - _ = A .snd - _ = B .snd - path : ∀ x → - α .N-ob B (X .F-hom φ x) ≡ φ .fst (- α .N-ob A x) - path x = - α .N-ob B (X .F-hom φ x) ≡⟨ cong -_ (funExt⁻ (α .N-hom φ) x) ⟩ - - φ .fst (α .N-ob A x) ≡⟨ sym (φ .snd .pres- _) ⟩ - φ .fst (- α .N-ob A x) ∎ - - CommRingStr.isCommRing (snd (F-ob Γ X)) = makeIsCommRing - isSetNatTrans - (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Assoc _ _ _)) - (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+IdR _)) - (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+InvR _)) - (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Comm _ _)) - (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Assoc _ _ _)) - (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·IdR _)) - (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·DistR+ _ _ _)) - (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Comm _ _)) - - -- action on natural transformations - fst (F-hom Γ α) = α ●ᵛ_ - pres0 (snd (F-hom Γ α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres1 (snd (F-hom Γ α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres+ (snd (F-hom Γ α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - pres· (snd (F-hom Γ α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - pres- (snd (F-hom Γ α)) _ = makeNatTransPath (funExt₂ λ _ _ → refl) - - -- functoriality of Γ - F-id Γ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - F-seq Γ _ _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - - --- we get an adjunction Γ ⊣ Sp modulo size issues -module AdjBij where - - open Functor - open NatTrans - open Iso - open IsRingHom - - private module _ {A : CommRing ℓ} {X : ℤFunctor {ℓ}} where - _♭ : CommRingHom A (Γ .F-ob X) → X ⇒ Sp .F-ob A - fst (N-ob (φ ♭) B x) a = φ .fst a .N-ob B x - - pres0 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres0) - pres1 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres1) - pres+ (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres+ _ _) - pres· (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres· _ _) - pres- (snd (N-ob (φ ♭) B x)) _ = cong (λ y → y .N-ob B x) (φ .snd .pres- _) - - N-hom (φ ♭) ψ = funExt (λ x → RingHom≡ (funExt λ a → funExt⁻ (φ .fst a .N-hom ψ) x)) - - - -- the other direction is just precomposition modulo Yoneda - _♯ : X ⇒ Sp .F-ob A → CommRingHom A (Γ .F-ob X) - fst (α ♯) a = α ●ᵛ yonedaᴾ 𝔸¹ A .inv a - - pres0 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres0) - pres1 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres1) - pres+ (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres+ _ _) - pres· (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres· _ _) - pres- (snd (α ♯)) _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres- _) - - - -- the two maps are inverse to each other - ♭♯Id : ∀ (α : X ⇒ Sp .F-ob A) → ((α ♯) ♭) ≡ α - ♭♯Id _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) - - ♯♭Id : ∀ (φ : CommRingHom A (Γ .F-ob X)) → ((φ ♭) ♯) ≡ φ - ♯♭Id _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - - Γ⊣SpIso : {A : CommRing ℓ} {X : ℤFunctor {ℓ}} - → Iso (CommRingHom A (Γ .F-ob X)) (X ⇒ Sp .F-ob A) - fun Γ⊣SpIso = _♭ - inv Γ⊣SpIso = _♯ - rightInv Γ⊣SpIso = ♭♯Id - leftInv Γ⊣SpIso = ♯♭Id - - Γ⊣SpNatℤFunctor : {A : CommRing ℓ} {X Y : ℤFunctor {ℓ}} (α : X ⇒ Sp .F-ob A) (β : Y ⇒ X) - → (β ●ᵛ α) ♯ ≡ (Γ .F-hom β) ∘cr (α ♯) - Γ⊣SpNatℤFunctor _ _ = RingHom≡ (funExt (λ _ → makeNatTransPath (funExt₂ (λ _ _ → refl)))) - - Γ⊣SpNatCommRing : {X : ℤFunctor {ℓ}} {A B : CommRing ℓ} - (φ : CommRingHom A (Γ .F-ob X)) (ψ : CommRingHom B A) - → (φ ∘cr ψ) ♭ ≡ (φ ♭) ●ᵛ Sp .F-hom ψ - Γ⊣SpNatCommRing _ _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) - - -- the counit is an equivalence - private - ε : (A : CommRing ℓ) → CommRingHom A ((Γ ∘F Sp) .F-ob A) - ε A = (idTrans (Sp .F-ob A)) ♯ - - Γ⊣SpCounitEquiv : (A : CommRing ℓ) → CommRingEquiv A ((Γ ∘F Sp) .F-ob A) - fst (Γ⊣SpCounitEquiv A) = isoToEquiv theIso - where - theIso : Iso (A .fst) ((Γ ∘F Sp) .F-ob A .fst) - fun theIso = ε A .fst - inv theIso = yonedaᴾ 𝔸¹ A .fun - rightInv theIso α = ℤFUNCTOR .⋆IdL _ ∙ yonedaᴾ 𝔸¹ A .leftInv α - leftInv theIso a = path -- I get yellow otherwise - where - path : yonedaᴾ 𝔸¹ A .fun ((idTrans (Sp .F-ob A)) ●ᵛ yonedaᴾ 𝔸¹ A .inv a) ≡ a - path = cong (yonedaᴾ 𝔸¹ A .fun) (ℤFUNCTOR .⋆IdL _) ∙ yonedaᴾ 𝔸¹ A .rightInv a - snd (Γ⊣SpCounitEquiv A) = ε A .snd - - --- Affine schemes -module _ {ℓ : Level} where - open Functor - - 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 - - --- The unit is an equivalence iff the ℤ-functor is affine. --- Unfortunately, we can't give a natural transformation --- X ⇒ Sp (Γ X), because the latter ℤ-functor lives in a higher universe. --- We can however give terms that look just like the unit, --- giving us an alternative def. of affine ℤ-functors -private module AffineDefs {ℓ : Level} where - open Functor - open NatTrans - open Iso - open IsRingHom - η : (X : ℤFunctor) (A : CommRing ℓ) → X .F-ob A .fst → CommRingHom (Γ .F-ob X) A - fst (η X A x) α = α .N-ob A x - pres0 (snd (η X A x)) = refl - pres1 (snd (η X A x)) = refl - pres+ (snd (η X A x)) _ _ = refl - pres· (snd (η X A x)) _ _ = refl - pres- (snd (η X A x)) _ = refl - - -- this is basically a natural transformation - ηObHom : (X : ℤFunctor) {A B : CommRing ℓ} (φ : CommRingHom A B) - → η X B ∘ (X .F-hom φ) ≡ (φ ∘cr_) ∘ η X A - ηObHom X φ = funExt (λ x → RingHom≡ (funExt λ α → funExt⁻ (α .N-hom φ) x)) - - -- can only state equality on object part, but that would be enough - ηHom : {X Y : ℤFunctor} (α : X ⇒ Y) (A : CommRing ℓ) (x : X .F-ob A .fst) - → η Y A (α .N-ob A x) ≡ η X A x ∘cr Γ .F-hom α - ηHom _ _ _ = RingHom≡ refl - - isAffine' : (X : ℤFunctor) → Type (ℓ-suc ℓ) - isAffine' X = ∀ (A : CommRing ℓ) → isEquiv (η X A) - -- TODO: isAffine → isAffine' - - --- compact opens and affine covers -module _ {ℓ : Level} where - - open Iso - open Functor - open NatTrans - open DistLatticeStr ⦃...⦄ - open CommRingStr ⦃...⦄ - open IsRingHom - open IsLatticeHom - open ZarLat - open ZarLatUniversalProp - - -- the Zariski lattice classifying compact open subobjects - 𝓛 : ℤFunctor {ℓ = ℓ} - F-ob 𝓛 A = ZL A , SQ.squash/ - F-hom 𝓛 φ = inducedZarLatHom φ .fst - F-id 𝓛 {A} = cong fst (inducedZarLatHomId A) - F-seq 𝓛 φ ψ = cong fst (inducedZarLatHomSeq φ ψ) - - CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) - CompactOpen X = X ⇒ 𝓛 - - -- the induced subfunctor - ⟦_⟧ᶜᵒ : {X : ℤFunctor} (U : CompactOpen X) → ℤFunctor - F-ob (⟦_⟧ᶜᵒ {X = X} U) A = (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D A 1r) - , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ - where instance _ = snd A - F-hom (⟦_⟧ᶜᵒ {X = X} U) {x = A} {y = B} φ (x , Ux≡D1) = (X .F-hom φ x) , path - where - instance - _ = A .snd - _ = B .snd - open IsLatticeHom - path : U .N-ob B (X .F-hom φ x) ≡ D B 1r - path = U .N-ob B (X .F-hom φ x) ≡⟨ funExt⁻ (U .N-hom φ) x ⟩ - 𝓛 .F-hom φ (U .N-ob A x) ≡⟨ cong (𝓛 .F-hom φ) Ux≡D1 ⟩ - 𝓛 .F-hom φ (D A 1r) ≡⟨ inducedZarLatHom φ .snd .pres1 ⟩ - D B 1r ∎ - F-id (⟦_⟧ᶜᵒ {X = X} U) = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) - (funExt⁻ (X .F-id) (x .fst))) - F-seq (⟦_⟧ᶜᵒ {X = X} U) φ ψ = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) - (funExt⁻ (X .F-seq φ ψ) (x .fst))) - - - isAffineCompactOpen : {X : ℤFunctor} (U : CompactOpen X) → Type (ℓ-suc ℓ) - isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ - - -- TODO: define basic opens D(f) ↪ Sp A and prove ⟦ D(f) ⟧ᶜᵒ ≅ Sp A[1/f] - - -- the (big) dist. lattice of compact opens - CompOpenDistLattice : Functor ℤFUNCTOR (DistLatticesCategory {ℓ = ℓ-suc ℓ} ^op) - fst (F-ob CompOpenDistLattice X) = CompactOpen X - - -- lattice structure induce by internal lattice object 𝓛 - N-ob (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) A _ = 0l - where instance _ = ZariskiLattice A .snd - N-hom (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) _ = funExt λ _ → refl - - N-ob (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) A _ = 1l - where instance _ = ZariskiLattice A .snd - N-hom (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path - where - instance - _ = A .snd - _ = B .snd - _ = ZariskiLattice B .snd - path : D B 1r ≡ D B (φ .fst 1r) ∨l 0l - path = cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _) - - N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = U .N-ob A x ∨l V .N-ob A x - where instance _ = ZariskiLattice A .snd - N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = funExt path - where - instance - _ = ZariskiLattice A .snd - _ = ZariskiLattice B .snd - path : ∀ x → U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) - ≡ 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) - path x = U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) - ≡⟨ cong₂ _∨l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ - 𝓛 .F-hom φ (U .N-ob A x) ∨l 𝓛 .F-hom φ (V .N-ob A x) - ≡⟨ sym (inducedZarLatHom φ .snd .pres∨l _ _) ⟩ - 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ - - N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) A x = U .N-ob A x ∧l V .N-ob A x - where instance _ = ZariskiLattice A .snd - N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = funExt path - where - instance - _ = ZariskiLattice A .snd - _ = ZariskiLattice B .snd - path : ∀ x → U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) - ≡ 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) - path x = U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) - ≡⟨ cong₂ _∧l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ - 𝓛 .F-hom φ (U .N-ob A x) ∧l 𝓛 .F-hom φ (V .N-ob A x) - ≡⟨ sym (inducedZarLatHom φ .snd .pres∧l _ _) ⟩ - 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ - - DistLatticeStr.isDistLattice (snd (F-ob CompOpenDistLattice X)) = makeIsDistLattice∧lOver∨l - isSetNatTrans - (λ _ _ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lAssoc _ _ _))) - (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lRid _))) - (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lComm _ _))) - (λ _ _ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lAssoc _ _ _))) - (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lRid _))) - (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lComm _ _))) - (λ _ _ → makeNatTransPath (funExt₂ -- don't know why ∧lAbsorb∨l doesn't work - (λ A _ → ZariskiLattice A .snd .DistLatticeStr.absorb _ _ .snd))) - (λ _ _ _ → makeNatTransPath (funExt₂ -- same here - (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) - - -- (contravariant) action on morphisms - fst (F-hom CompOpenDistLattice α) = α ●ᵛ_ - pres0 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres1 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres∨l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - pres∧l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - - -- functoriality - F-id CompOpenDistLattice = LatticeHom≡f _ _ - (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - F-seq CompOpenDistLattice _ _ = LatticeHom≡f _ _ - (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - - - module _ (X : ℤFunctor) where - 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))) - 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 ∥₁ - -- TODO: A ℤ-functor is a qcqs-scheme if it is a Zariski sheaf and has an affine cover - - -- the structure sheaf - private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op - - compOpenIncl : {U V : CompactOpen X} → V ≤ U → ⟦ V ⟧ᶜᵒ ⇒ ⟦ U ⟧ᶜᵒ - N-ob (compOpenIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) = x , path - where - instance - _ = A .snd - _ = ZariskiLattice A .snd - _ = DistLattice→Lattice (ZariskiLattice A) - path : U .N-ob A x ≡ D A 1r - path = U .N-ob A x ≡⟨ funExt⁻ (funExt⁻ (cong N-ob (sym V≤U)) A) x ⟩ - V .N-ob A x ∨l U .N-ob A x ≡⟨ cong (_∨l U .N-ob A x) Vx≡D1 ⟩ - D A 1r ∨l U .N-ob A x ≡⟨ 1lLeftAnnihilates∨l _ ⟩ - D A 1r ∎ - N-hom (compOpenIncl V≤U) φ = funExt λ x → Σ≡Prop (λ _ → squash/ _ _) refl - - compOpenInclId : ∀ {U : CompactOpen X} → compOpenIncl (is-refl U) ≡ idTrans ⟦ U ⟧ᶜᵒ - compOpenInclId = makeNatTransPath (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) - - compOpenInclSeq : ∀ {U V W : CompactOpen X} (U≤V : U ≤ V) (V≤W : V ≤ W) - → compOpenIncl (is-trans _ _ _ U≤V V≤W) - ≡ compOpenIncl U≤V ●ᵛ compOpenIncl V≤W - compOpenInclSeq _ _ = makeNatTransPath - (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) - - 𝓞 : Functor COᵒᵖ (CommRingsCategory {ℓ = ℓ-suc ℓ}) - F-ob 𝓞 U = Γ .F-ob ⟦ U ⟧ᶜᵒ - F-hom 𝓞 U≥V = Γ .F-hom (compOpenIncl U≥V) - F-id 𝓞 = cong (Γ .F-hom) compOpenInclId ∙ Γ .F-id - F-seq 𝓞 _ _ = cong (Γ .F-hom) (compOpenInclSeq _ _) ∙ Γ .F-seq _ _ diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda new file mode 100644 index 0000000000..602d26e9d8 --- /dev/null +++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda @@ -0,0 +1,229 @@ +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Categories.Site.Instances.ZariskiCommRing where + + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Structure + +open import Cubical.Data.Nat using (ℕ ; zero ; suc) +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.Data.FinData.Order renaming (_<'Fin_ to _<_) + +open import Cubical.Algebra.Ring +open import Cubical.Algebra.Ring.BigOps +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.Categories.Category +open import Cubical.Categories.Limits.Terminal +open import Cubical.Categories.Instances.CommRings +open import Cubical.Categories.Site.Coverage +open import Cubical.Categories.Site.Sheaf +open import Cubical.Categories.Constructions.Slice +open import Cubical.Categories.Yoneda + +open import Cubical.HITs.PropositionalTruncation as PT + +private + variable + ℓ ℓ' ℓ'' : Level + +open Coverage +open SliceOb + +-- the type of unimodular vectors, i.e. generators of the 1-ideal +record UniModVec (R : CommRing ℓ) : Type ℓ where + constructor + unimodvec + + open CommRingStr (str R) + open CommIdeal R using (_∈_) + + field + n : ℕ + f : FinVec ⟨ R ⟩ n + isUniMod : 1r ∈ ⟨ f ⟩[ R ] + +module _ {A : CommRing ℓ} {B : CommRing ℓ'} (φ : CommRingHom A B) where + open UniModVec + open IsRingHom ⦃...⦄ + open CommRingStr ⦃...⦄ + open Sum (CommRing→Ring B) + open SumMap _ _ φ + private + module A = CommIdeal A + module B = CommIdeal B + + instance + _ = A .snd + _ = B .snd + _ = φ .snd + + pullbackUniModVec : UniModVec A → UniModVec B + n (pullbackUniModVec um) = um .n + f (pullbackUniModVec um) i = φ $r um .f i + isUniMod (pullbackUniModVec um) = B.subst-∈ -- 1 ∈ ⟨ f₁ ,..., fₙ ⟩ → 1 ∈ ⟨ φ(f₁) ,..., φ(fₙ) ⟩ + ⟨ φ .fst ∘ um .f ⟩[ B ] + pres1 (PT.map mapHelper (um .isUniMod)) + where + mapHelper : Σ[ α ∈ FinVec ⟨ A ⟩ _ ] 1r ≡ linearCombination A α (um .f) + → Σ[ β ∈ FinVec ⟨ B ⟩ _ ] φ $r 1r ≡ linearCombination B β (φ .fst ∘ um .f) + fst (mapHelper (α , 1≡∑αf)) = φ .fst ∘ α + snd (mapHelper (α , 1≡∑αf)) = + subst (λ x → φ $r x ≡ linearCombination B (φ .fst ∘ α) (φ .fst ∘ um .f)) + (sym 1≡∑αf) + (∑Map _ ∙ ∑Ext (λ _ → pres· _ _)) + + +{- + + For 1 ∈ ⟨ f₁ ,..., fₙ ⟩ we get a cover by arrows _/1 : R → R[1/fᵢ] for i=1,...,n + Pullback along φ : A → B is given by the induced arrows A[1/fᵢ] → B[1/φ(fᵢ)] + +-} +zariskiCoverage : Coverage (CommRingsCategory {ℓ = ℓ} ^op) ℓ ℓ-zero +fst (covers zariskiCoverage R) = UniModVec R +fst (snd (covers zariskiCoverage R) um) = Fin n --patches + where + open UniModVec um +S-ob (snd (snd (covers zariskiCoverage R) um) i) = R[1/ f i ]AsCommRing + where + open UniModVec um + open InvertingElementsBase R +S-arr (snd (snd (covers zariskiCoverage R) um) i) = /1AsCommRingHom + where + open UniModVec um + open InvertingElementsBase.UniversalProp R (f i) +pullbackStability zariskiCoverage {c = A} um {d = B} φ = + ∣ pullbackUniModVec φ um , (λ i → ∣ i , ψ i , RingHom≡ (sym (ψComm i)) ∣₁) ∣₁ + where + open UniModVec + module A = InvertingElementsBase A + module B = InvertingElementsBase B + module AU = A.UniversalProp + module BU = B.UniversalProp + + ψ : (i : Fin (um .n)) → CommRingHom A.R[1/ um .f i ]AsCommRing B.R[1/ φ $r um .f i ]AsCommRing + ψ i = uniqInvElemHom φ (um .f i) .fst .fst + + ψComm : ∀ i → (ψ i .fst) ∘ (AU._/1 (um .f i)) ≡ (BU._/1 (φ $r um .f i)) ∘ φ .fst + ψComm i = uniqInvElemHom φ (um .f i) .fst .snd + + +-- this defines a subcanonical coverage +-- the proof is analoguous to the case of lattice sheaves, +-- see "isLimConeLocCone" in Cubical.Algebra.CommRing.Localisation.Limit +-- first, a lemma +module SubcanonicalLemmas (A R : CommRing ℓ) where + open CommRingStr ⦃...⦄ + open CommIdeal R using (_∈_) + + private instance + _ = A .snd + _ = R .snd + + module _ + {n : ℕ} + (f : FinVec ⟨ R ⟩ (suc n)) -- have to treat case of empty vec separately + (isUniModF : 1r ∈ ⟨ f ⟩[ R ]) + (fam@(φ , isCompatibleφ) : CompatibleFamily (yo A) + (str (covers zariskiCoverage R) + (unimodvec (suc n) f isUniModF))) + where + open InvertingElementsBase R + open RingHoms + module U i = UniversalProp (f i) + module UP i j = UniversalProp (f i · f j) + + private + _/1ⁱ : ⟨ R ⟩ → {i : Fin (suc n)} → R[1/ (f i) ] + (r /1ⁱ) {i = i} = U._/1 i r + + + applyEqualizerLemma : ∀ a → ∃![ r ∈ ⟨ R ⟩ ] ∀ i → r /1ⁱ ≡ φ i .fst a + applyEqualizerLemma a = equalizerLemma R f isUniModF (λ i → φ i .fst a) path + where + pathHelper : ∀ i j → χˡ R f i j ∘r (U./1AsCommRingHom i) + ≡ χʳ R f i j ∘r (U./1AsCommRingHom j) + pathHelper i j = RingHom≡ + (χˡUnique R f i j .fst .snd ∙ sym (χʳUnique R f i j .fst .snd)) + + path : ∀ i j → χˡ R f i j .fst (φ i $r a) ≡ χʳ R f i j .fst (φ j $r a) + path i j = funExt⁻ (cong fst (isCompatibleφ i j _ _ _ (pathHelper i j))) a + + inducedHom : CommRingHom A R + fst inducedHom a = applyEqualizerLemma a .fst .fst + snd inducedHom = makeIsRingHom + (cong fst (applyEqualizerLemma 1r .snd (1r , 1Coh))) + (λ x y → cong fst (applyEqualizerLemma (x + y) .snd (_ , +Coh x y))) + (λ x y → cong fst (applyEqualizerLemma (x · y) .snd (_ , ·Coh x y))) + where + open IsRingHom + 1Coh : ∀ i → (1r /1ⁱ ≡ φ i .fst 1r) + 1Coh i = sym (φ i .snd .pres1) + + +Coh : ∀ x y i → ((fst inducedHom x + fst inducedHom y) /1ⁱ ≡ φ i .fst (x + y)) + +Coh x y i = let instance _ = snd R[1/ f i ]AsCommRing in + U./1AsCommRingHom i .snd .pres+ _ _ + ∙∙ cong₂ _+_ (applyEqualizerLemma x .fst .snd i) (applyEqualizerLemma y .fst .snd i) + ∙∙ sym (φ i .snd .pres+ x y) + + ·Coh : ∀ x y i → ((fst inducedHom x · fst inducedHom y) /1ⁱ ≡ φ i .fst (x · y)) + ·Coh x y i = let instance _ = snd R[1/ f i ]AsCommRing in + U./1AsCommRingHom i .snd .pres· _ _ + ∙∙ cong₂ _·_ (applyEqualizerLemma x .fst .snd i) (applyEqualizerLemma y .fst .snd i) + ∙∙ sym (φ i .snd .pres· x y) + + inducedHomUnique : ∀ (ψ : CommRingHom A R) + → (∀ a i → (ψ $r a) /1ⁱ ≡ φ i $r a) + → inducedHom ≡ ψ + inducedHomUnique ψ ψ/1≡φ = + RingHom≡ + (funExt + (λ a → cong fst (applyEqualizerLemma a .snd (ψ $r a , ψ/1≡φ a)))) + + +isSubcanonicalZariskiCoverage : isSubcanonical + (CommRingsCategory {ℓ = ℓ} ^op) + zariskiCoverage +isSubcanonicalZariskiCoverage A R (unimodvec zero f isUniModF) = + isoToIsEquiv (isContr→Iso' + (trivialIsTerminalCommRing R 0≡1 A) + isContrCompatibleFamily _) + -- better way than pattern matching inside unimodvec??? + where + um = (unimodvec zero f isUniModF) + open CommRingStr (R .snd) + + 0≡1 : 0r ≡ 1r + 0≡1 = PT.rec (is-set _ _) Σhelper isUniModF + where + Σhelper : Σ[ α ∈ FinVec ⟨ R ⟩ zero ] 1r ≡ linearCombination R α f + → 0r ≡ 1r + Σhelper (_ , 1≡αf) = sym 1≡αf + + isContrCompatibleFamily : isContr (CompatibleFamily (yo A) + (str (covers zariskiCoverage R) um)) + fst (fst isContrCompatibleFamily) () + snd (fst isContrCompatibleFamily) () + snd isContrCompatibleFamily _ = CompatibleFamily≡ _ _ _ _ λ () + +isSubcanonicalZariskiCoverage A R (unimodvec (suc n) f isUniModF) = isoToIsEquiv theIso + where + open Iso + open SubcanonicalLemmas A R + um = (unimodvec (suc n) f isUniModF) + + theIso : Iso (CommRingHom A R) + (CompatibleFamily (yo A) (str (covers zariskiCoverage R) um)) + fun theIso = elementToCompatibleFamily _ _ + inv theIso fam = inducedHom f isUniModF fam + rightInv theIso fam = CompatibleFamily≡ _ _ _ _ + λ i → RingHom≡ (funExt + λ a → applyEqualizerLemma f isUniModF fam a .fst .snd i) + leftInv theIso φ = inducedHomUnique _ _ _ _ λ _ _ → refl diff --git a/Cubical/Categories/Site/Sheaf.agda b/Cubical/Categories/Site/Sheaf.agda index c1fa5b53ac..12f0ea25af 100644 --- a/Cubical/Categories/Site/Sheaf.agda +++ b/Cubical/Categories/Site/Sheaf.agda @@ -20,6 +20,7 @@ open import Cubical.Categories.Site.Coverage open import Cubical.Categories.Presheaf open import Cubical.Categories.Functor open import Cubical.Categories.Constructions.FullSubcategory +open import Cubical.Categories.Yoneda module _ {ℓ ℓ' : Level} @@ -62,6 +63,11 @@ module _ (isSetΠ (λ i → str (P ⟅ patchObj cov i ⟆))) isPropIsCompatibleFamily + CompatibleFamily≡ : (fam fam' : CompatibleFamily) + → (∀ i → fam .fst i ≡ fam' .fst i) + → fam ≡ fam' + CompatibleFamily≡ fam fam' p = Σ≡Prop isPropIsCompatibleFamily (funExt p) + elementToCompatibleFamily : ⟨ P ⟅ c ⟆ ⟩ → CompatibleFamily elementToCompatibleFamily x = (λ i → (P ⟪ patchArr cov i ⟫) x) , @@ -136,3 +142,16 @@ module _ (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) (ℓ-suc ℓF)) (ℓ-max (ℓ-max ℓ ℓ') ℓF) SheafCategory = FullSubcategory (PresheafCategory C ℓF) (isSheaf J) + + +module _ + {ℓ ℓ' ℓcov ℓpat : Level} + (C : Category ℓ ℓ') + (J : Coverage C ℓcov ℓpat) + where + + isSubcanonical : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) + isSubcanonical = ∀ c → isSheaf J (yo c) + + isPropIsSubcanonical : isProp isSubcanonical + isPropIsSubcanonical = isPropΠ λ c → isPropIsSheaf J (yo c) diff --git a/Cubical/Papers/AffineSchemes.agda b/Cubical/Papers/AffineSchemes.agda index beb6a5859d..612b7d8476 100644 --- a/Cubical/Papers/AffineSchemes.agda +++ b/Cubical/Papers/AffineSchemes.agda @@ -22,55 +22,55 @@ module Cubical.Papers.AffineSchemes where -- 2: Background -- 2.2: Cubical Agda -import Cubical.Foundations.Prelude as Prelude -import Cubical.Foundations.HLevels as HLevels -import Cubical.Foundations.Univalence as Univalence -import Cubical.Data.Sigma as Sigma -import Cubical.HITs.PropositionalTruncation as PT -import Cubical.Algebra.DistLattice.Basis as DistLatticeBasis -import Cubical.HITs.SetQuotients as SQ +import Cubical.Foundations.Prelude as Prelude +import Cubical.Foundations.HLevels as HLevels +import Cubical.Foundations.Univalence as Univalence +import Cubical.Data.Sigma as Sigma +import Cubical.HITs.PropositionalTruncation as PT +import Cubical.Algebra.DistLattice.Basis as DistLatticeBasis +import Cubical.HITs.SetQuotients as SQ -- 3: Commutative Algebra -- 3.1: Localization -import Cubical.Algebra.CommRing.Localisation.Base as L +import Cubical.Algebra.CommRing.Localisation.Base as L module Localization = L.Loc -import Cubical.Algebra.CommRing.Localisation.UniversalProperty as LocalizationUnivProp -import Cubical.Algebra.CommRing.Localisation.InvertingElements as LocalizationInvEl -import Cubical.Algebra.CommAlgebra as R-Algs -import Cubical.Algebra.CommAlgebra.Localisation as LocalizationR-Alg +import Cubical.Algebra.CommRing.Localisation.UniversalProperty as LocalizationUnivProp +import Cubical.Algebra.CommRing.Localisation.InvertingElements as LocalizationInvEl +import Cubical.Algebra.CommAlgebra as R-Algs +import Cubical.Algebra.CommAlgebra.Localisation as LocalizationR-Alg -- 3.2: The Zariski Lattice -import Cubical.Data.FinData.Base as FiniteTypes -import Cubical.Algebra.Matrix as Matrices -import Cubical.Algebra.CommRing.FGIdeal as FinGenIdeals +import Cubical.Data.FinData.Base as FiniteTypes +import Cubical.Algebra.Matrix as Matrices +import Cubical.Algebra.CommRing.FGIdeal as FinGenIdeals -import Cubical.Algebra.ZariskiLattice.Base as ZLB +import Cubical.AlgebraicGeometry.ZariskiLattice.Base as ZLB module ZariskiLatDef = ZLB.ZarLat -import Cubical.Algebra.ZariskiLattice.UniversalProperty as ZLUP +import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty as ZLUP module ZariskiLatUnivProp = ZLUP.ZarLatUniversalProp -- 4: Category Theory -- background theory not explicitly mentioned -import Cubical.Categories.Category.Base as CatTheory -import Cubical.Categories.Limits as GeneralLimits -import Cubical.Categories.Limits.RightKan as GeneralKanExtension +import Cubical.Categories.Category.Base as CatTheory +import Cubical.Categories.Limits as GeneralLimits +import Cubical.Categories.Limits.RightKan as GeneralKanExtension -import Cubical.Categories.DistLatticeSheaf.Diagram as SheafDiagShapes -import Cubical.Categories.DistLatticeSheaf.Base as Sheaves +import Cubical.Categories.DistLatticeSheaf.Diagram as SheafDiagShapes +import Cubical.Categories.DistLatticeSheaf.Base as Sheaves -import Cubical.Categories.DistLatticeSheaf.Extension as E +import Cubical.Categories.DistLatticeSheaf.Extension as E module SheafExtension = E.PreSheafExtension -- 5: The Structure Sheaf -import Cubical.Categories.Instances.CommAlgebras as R-AlgConstructions -import Cubical.Algebra.CommRing.Localisation.Limit as LocalizationLimit -import Cubical.Algebra.ZariskiLattice.StructureSheaf as StructureSheaf +import Cubical.Categories.Instances.CommAlgebras as R-AlgConstructions +import Cubical.Algebra.CommRing.Localisation.Limit as LocalizationLimit +import Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf as StructureSheaf @@ -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/README.agda b/Cubical/README.agda index c1f7d002fa..094eccbc73 100644 --- a/Cubical/README.agda +++ b/Cubical/README.agda @@ -65,6 +65,9 @@ import Cubical.ZCohomology.Everything -- Algebra library (in development) import Cubical.Algebra.Everything +-- Algebraic geometry +import Cubical.AlgebraicGeometry.Everything + -- Various talks import Cubical.Talks.Everything diff --git a/Cubical/Relation/Binary/Order/Poset/Properties.agda b/Cubical/Relation/Binary/Order/Poset/Properties.agda index 4e56fc7d47..50d6f9b6ab 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,23 @@ 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 + IsPoset.is-set (PosetStr.isPoset (snd (↓ᴾ u))) = + isSetΣSndProp is-set λ _ → is-prop-valued _ _ + IsPoset.is-prop-valued (PosetStr.isPoset (snd (↓ᴾ u))) _ _ = is-prop-valued _ _ + IsPoset.is-refl (PosetStr.isPoset (snd (↓ᴾ u))) _ = is-refl _ + IsPoset.is-trans (PosetStr.isPoset (snd (↓ᴾ u))) _ _ _ = is-trans _ _ _ + IsPoset.is-antisym (PosetStr.isPoset (snd (↓ᴾ u))) _ _ v≤w w≤v = + Σ≡Prop (λ _ → is-prop-valued _ _) (is-antisym _ _ v≤w w≤v)