{-# OPTIONS --safe #-}
module Cubical.Papers.FunctorialQcQsSchemes where
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.HITs.SetQuotients as SQ
import Cubical.Algebra.CommRing.Localisation.InvertingElements as LocalizationInvEl
module LocalizationInvElBase = LocalizationInvEl.InvertingElementsBase
module LocalizationInvElUniversalProp = LocalizationInvElBase.UniversalProp
import Cubical.AlgebraicGeometry.ZariskiLattice.Base as ZLB
module ZariskiLatDef = ZLB.ZarLat
import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty as ZLUP
module ZariskiLatUnivProp = ZLUP.ZarLatUniversalProp
module Localization&Radicals = LocalizationInvEl.RadicalLemma
import Cubical.AlgebraicGeometry.ZariskiLattice.Properties as ZLP
import Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base as ZFun
module RelativeAdjunction = ZFun.AdjBij
import Cubical.Categories.Site.Cover as Cover
import Cubical.Categories.Site.Coverage as Coverage
import Cubical.Categories.Site.Sheaf as Sheaf
import Cubical.Categories.Site.Instances.ZariskiCommRing as ZariskiCoverage
module ZarCovSubcanonical = ZariskiCoverage.SubcanonicalLemmas
import Cubical.Algebra.CommRing.Localisation.Limit as LocalizationLimit
import Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen as CO
import Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme as QcQsSchemes
import Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme as OSubscheme
module StandardOpen = OSubscheme.StandardOpens
open Prelude using (_≡_)
open Prelude using (isProp ; isSet)
open HLevels using (hProp)
open Univalence using (ua)
import Cubical.Foundations.SIP
open SQ using (_/_)
open PT renaming (∥_∥₁ to ∥_∥)
open Sigma using (∃-syntax)
open LocalizationInvElBase using (R[1/_] ; R[1/_]AsCommRing)
open LocalizationInvElUniversalProp using (_/1 ; invElemUniversalProp)
open ZariskiLatDef using (ZariskiLattice ; _∼≡_)
open ZLUP.IsSupport
open ZariskiLatUnivProp using (D ; isSupportD)
open ZariskiLatUnivProp using (ZLHasUniversalProp ; ⋁D≡)
open Localization&Radicals using (unitHelper; toUnit)
open ZLP using (unitLemmaZarLat)
open ZLP using (oneIdealLemmaZarLat)
open ZFun using (ℤFunctor ; Sp ; 𝔸¹ ; isAffine)
open ZFun using (𝓞)
open RelativeAdjunction
using (𝓞⊣SpIso ; 𝓞⊣SpNatℤFunctor ; 𝓞⊣SpNatCommRing ; 𝓞⊣SpCounitEquiv)
open Cover using (Cover)
open Coverage using (Coverage)
open Sheaf using (isCompatibleFamily ; CompatibleFamily)
open Sheaf renaming (elementToCompatibleFamily to σ)
open Sheaf using (isSheaf ; hasAmalgamationPropertyForCover)
open Sheaf using (isSubcanonical)
open ZariskiCoverage using (UniModVec ; pullbackUniModVec ; zariskiCoverage)
open ZFun using (isLocal)
open LocalizationLimit using (equalizerLemma)
open ZarCovSubcanonical using (applyEqualizerLemma)
open ZariskiCoverage using (isSubcanonicalZariskiCoverage)
open CO renaming (ZarLatFun to 𝓛)
open CO using (CompactOpen ; ⟦_⟧ᶜᵒ)
open CO using (CompOpenDistLattice)
open QcQsSchemes using (isQcQsScheme)
open QcQsSchemes using (singlAffineCover ; isQcQsSchemeAffine)
open QcQsSchemes using (AffineCover ; hasAffineCover)
open CO using (isSeparatedZarLatFun)
open CO using (presLocalCompactOpen)
open StandardOpen using (D)
open StandardOpen using (SpR[1/f]≅⟦Df⟧ ; isAffineD)
open OSubscheme using (isQcQsSchemeCompOpenOfAffine)