{-# OPTIONS --safe #-}
module Cubical.Papers.AffineSchemes 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.Algebra.DistLattice.Basis as DistLatticeBasis
import Cubical.HITs.SetQuotients as SQ
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.Data.FinData.Base as FiniteTypes
import Cubical.Algebra.Matrix as Matrices
import Cubical.Algebra.CommRing.FGIdeal as FinGenIdeals
import Cubical.AlgebraicGeometry.ZariskiLattice.Base as ZLB
module ZariskiLatDef = ZLB.ZarLat
import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty as ZLUP
module ZariskiLatUnivProp = ZLUP.ZarLatUniversalProp
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.Extension as E
module SheafExtension = E.PreSheafExtension
import Cubical.Categories.Instances.CommAlgebras as R-AlgConstructions
import Cubical.Algebra.CommRing.Localisation.Limit as LocalizationLimit
import Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf as StructureSheaf
open Prelude using (_≡_ ; PathP)
open Univalence using (ua)
import Cubical.Foundations.SIP
open R-Algs renaming (uaCommAlgebra to sip)
open Prelude using (isContr ; isProp ; isSet)
open HLevels using (hProp)
open PT renaming (∥_∥₁ to ∥_∥)
open Sigma using (∃-syntax)
open DistLatticeBasis using (IsBasis)
open SQ using (_/_)
open Localization using (_≈_ ; S⁻¹R ; S⁻¹RAsCommRing)
open SQ using (truncRelEquiv)
open LocalizationUnivProp.S⁻¹RUniversalProp using (_/1)
open LocalizationUnivProp.S⁻¹RUniversalProp using (S⁻¹RHasUniversalProp)
open R-Algs.CommAlgChar
open LocalizationR-Alg.AlgLoc using (S⁻¹RHasAlgUniversalProp)
open LocalizationUnivProp using (S⁻¹RChar)
open LocalizationR-Alg.AlgLoc using (S⁻¹RAlgCharEquiv)
open LocalizationInvEl.InvertingElementsBase using ([_ⁿ|n≥0] ; R[1/_] ; R[1/_]AsCommRing)
open LocalizationInvEl.DoubleLoc using (R[1/fg]≡R[1/f][1/g])
open LocalizationR-Alg.DoubleAlgLoc using (R[1/fg]≡R[1/f][1/g])
open LocalizationInvEl using (invertingUnitsPath)
open LocalizationR-Alg.AlgLocTwoSubsets using (isContrS₁⁻¹R≡S₂⁻¹R)
open ZariskiLatDef using (_∼_ ; ZL) renaming (_∼≡_ to _≋_)
open ZariskiLatDef using (≡→∼ ; ∼→≡)
open FiniteTypes renaming (_++Fin_ to _++_)
open FinGenIdeals using (FGIdealAddLemma)
open Matrices.ProdFin renaming (_··Fin_ to _··_)
open FinGenIdeals using (FGIdealMultLemma)
open ZariskiLatDef using (ZariskiLattice)
open ZariskiLatUnivProp using (D ; isSupportD)
open ZariskiLatUnivProp using (ZLHasUniversalProp)
open StructureSheaf using (contrHoms)
open StructureSheaf using (BasicOpens ; BO)
open ZariskiLatUnivProp using (ZLUniversalPropCorollary ; ⋁D≡)
open StructureSheaf using (basicOpensAreBasis)
open CatTheory using (ΣPropCat)
open SheafExtension using (DLRan ; DLRanNatIso)
open SheafDiagShapes using (DLShfDiagOb ; DLShfDiagHom ; DLShfDiag)
open SheafDiagShapes.DLShfDiagHomPath using (isSetDLShfDiagHom)
open SheafDiagShapes using (FinVec→Diag)
open Sheaves using (isDLSheaf)
open Sheaves.SheafOnBasis using (isDLBasisSheaf)
open Sheaves using (isDLSheafPullback)
open Sheaves.EquivalenceOfDefs using (L→P ; P→L)
open SheafExtension using (coverLemma)
open SheafExtension using (isDLSheafDLRan)
open R-Algs using (recPT→CommAlgebra)
open R-AlgConstructions.PreSheafFromUniversalProp renaming (universalPShf to 𝓟ᵤ)
open StructureSheaf using ( 𝓞ᴮ ; 𝓞 )
open StructureSheaf using (baseSections)
open StructureSheaf using (globalSection)
open LocalizationLimit using (isLimConeLocCone)
open StructureSheaf using (isSheaf𝓞ᴮ)
open StructureSheaf using (isSheaf𝓞)