Documentation

Mathlib.AlgebraicGeometry.Limits

(Co)Limits of Schemes #

We construct various limits and colimits in the category of schemes.

The existence of fibred products was shown in Mathlib/AlgebraicGeometry/Pullbacks.lean.
Spec ℤ is the terminal object.
The preceding two results imply that Scheme has all finite limits.
The empty scheme is the (strict) initial object.
The disjoint union is the coproduct of a family of schemes, and the forgetful functor to LocallyRingedSpace and TopCat preserves them.

TODO #

Spec preserves finite coproducts.

noncomputable def AlgebraicGeometry.specZIsTerminal :

CategoryTheory.Limits.IsTerminal (Spec (CommRingCat.of ℤ))

Spec ℤ is the terminal object in the category of schemes.

Instances For

noncomputable def AlgebraicGeometry.specULiftZIsTerminal :

CategoryTheory.Limits.IsTerminal (Spec (CommRingCat.of (ULift.{u, 0} ℤ)))

Spec ℤ is the terminal object in the category of schemes.

Instances For

instance AlgebraicGeometry.instHasTerminalScheme :

CategoryTheory.Limits.HasTerminal Scheme

instance AlgebraicGeometry.instIsAffineTerminalScheme :

IsAffine (⊤_ Scheme)

instance AlgebraicGeometry.instHasFiniteLimitsScheme :

CategoryTheory.Limits.HasFiniteLimits Scheme

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instOverTerminalScheme (X : Scheme) :

X.Over (⊤_ Scheme)

instance AlgebraicGeometry.instIsOverTerminalScheme {X Y : Scheme} [X.Over (⊤_ Scheme)] [Y.Over (⊤_ Scheme)] (f : X ⟶ Y) :

Scheme.Hom.IsOver f (⊤_ Scheme)

instance AlgebraicGeometry.instSubsingletonOverTerminalScheme {X : Scheme} :

Subsingleton (X.Over (⊤_ Scheme))

noncomputable def AlgebraicGeometry.Scheme.emptyTo (X : Scheme) :

∅ ⟶ X

The map from the empty scheme.

Instances For

@[simp]

theorem AlgebraicGeometry.Scheme.emptyTo_c_app (X : Scheme) (x✝ : (TopologicalSpace.Opens ↥X)ᵒᵖ) :

X.emptyTo.c.app x✝ = CommRingCat.punitIsTerminal.from (X.presheaf.obj x✝)

@[simp]

theorem AlgebraicGeometry.Scheme.emptyTo_base (X : Scheme) :

X.emptyTo.base = TopCat.ofHom { toFun := fun (x : PEmpty.{u + 1}) => x.elim, continuous_toFun := ⋯ }

theorem AlgebraicGeometry.Scheme.empty_ext {X : Scheme} (f g : ∅ ⟶ X) :

f = g

theorem AlgebraicGeometry.Scheme.empty_ext_iff {X : Scheme} {f g : ∅ ⟶ X} :

f = g ↔ True

theorem AlgebraicGeometry.Scheme.eq_emptyTo {X : Scheme} (f : ∅ ⟶ X) :

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.hom_unique_of_empty_source (X : Scheme) :

Unique (∅ ⟶ X)

noncomputable def AlgebraicGeometry.emptyIsInitial :

CategoryTheory.Limits.IsInitial ∅

The empty scheme is the initial object in the category of schemes.

Instances For

@[simp]

theorem AlgebraicGeometry.emptyIsInitial_to :

emptyIsInitial.to = Scheme.emptyTo

instance AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme :

IsEmpty ↥∅

instance AlgebraicGeometry.spec_punit_isEmpty :

IsEmpty ↥(Spec (CommRingCat.of PUnit.{u + 1}))

@[instance 100]

instance AlgebraicGeometry.isOpenImmersion_of_isEmpty {X Y : Scheme} (f : X ⟶ Y) [IsEmpty ↥X] :

IsOpenImmersion f

@[instance 100]

instance AlgebraicGeometry.isIso_of_isEmpty {X Y : Scheme} (f : X ⟶ Y) [IsEmpty ↥Y] :

CategoryTheory.IsIso f

noncomputable def AlgebraicGeometry.isInitialOfIsEmpty {X : Scheme} [IsEmpty ↥X] :

CategoryTheory.Limits.IsInitial X

A scheme is initial if its underlying space is empty .

Instances For

noncomputable def AlgebraicGeometry.specPUnitIsInitial :

CategoryTheory.Limits.IsInitial (Spec (CommRingCat.of PUnit.{u + 1}))

Spec 0 is the initial object in the category of schemes.

Instances For

@[deprecated AlgebraicGeometry.specPUnitIsInitial (since := "2026-02-08")]

def AlgebraicGeometry.specPunitIsInitial :

CategoryTheory.Limits.IsInitial (Spec (CommRingCat.of PUnit.{u + 1}))

Alias of AlgebraicGeometry.specPUnitIsInitial.

Spec 0 is the initial object in the category of schemes.

Instances For

theorem AlgebraicGeometry.isInitial_iff_isEmpty {X : Scheme} :

Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty ↥X

@[instance 100]

instance AlgebraicGeometry.isAffine_of_isEmpty {X : Scheme} [IsEmpty ↥X] :

instance AlgebraicGeometry.instHasInitialScheme :

CategoryTheory.Limits.HasInitial Scheme

instance AlgebraicGeometry.initial_isEmpty :

IsEmpty ↥(⊥_ Scheme)

theorem AlgebraicGeometry.isAffineOpen_bot (X : Scheme) :

IsAffineOpen ⊥

instance AlgebraicGeometry.instHasStrictInitialObjectsScheme :

CategoryTheory.Limits.HasStrictInitialObjects Scheme

instance AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty {X : Scheme} [IsEmpty ↥X] (U : X.Opens) :

Subsingleton ↑(X.presheaf.obj (Opposite.op U))

@[instance 100]

instance AlgebraicGeometry.instIsAffineOfSubsingletonCarrierCarrierCommRingCat {X : Scheme} [Subsingleton ↥X] :

This is true in general for finite discrete schemes. See below.

theorem AlgebraicGeometry.IsAffineOpen.of_subsingleton {X : Scheme} {U : X.Opens} (hU : (↑U).Subsingleton) :

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instCreatesColimitsOfShapeSchemeLocallyRingedSpaceDiscreteForgetToLocallyRingedSpaceOfSmall {σ : Type v} [Small.{u, v} σ] :

CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete σ) Scheme.forgetToLocallyRingedSpace

instance AlgebraicGeometry.instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall {σ : Type v} [Small.{u, v} σ] :

CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete σ) Scheme.forgetToTop

instance AlgebraicGeometry.instHasColimitsOfShapeDiscreteSchemeOfSmall {σ : Type v} [Small.{u, v} σ] :

CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete σ) Scheme

theorem AlgebraicGeometry.sigmaι_eq_iff {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] (i j : σ) (x : ↥(g i)) (y : ↥(g j)) :

(CategoryTheory.Limits.Sigma.ι g i) x = (CategoryTheory.Limits.Sigma.ι g j) y ↔ ⟨i, x⟩ = ⟨j, y⟩

theorem AlgebraicGeometry.disjoint_opensRange_sigmaι {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] (i j : σ) (h : i ≠ j) :

Disjoint (Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι g i)) (Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι g j))

The images of each component in the coproduct is disjoint.

theorem AlgebraicGeometry.isEmpty_of_commSq_sigmaι_of_ne {σ : Type v} {g : σ → Scheme} [Small.{u, v} σ] {i j : σ} {Z : Scheme} {a : Z ⟶ g i} {b : Z ⟶ g j} (h : CategoryTheory.CommSq a b (CategoryTheory.Limits.Sigma.ι g i) (CategoryTheory.Limits.Sigma.ι g j)) (hij : i ≠ j) :

theorem AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] {i j : σ} (hij : i ≠ j) :

IsEmpty ↥(CategoryTheory.Limits.pullback (CategoryTheory.Limits.Sigma.ι g i) (CategoryTheory.Limits.Sigma.ι g j))

instance AlgebraicGeometry.instCoproductsOfShapeDisjointSchemeOfSmall {σ : Type v} [Small.{u, v} σ] :

CategoryTheory.Limits.CoproductsOfShapeDisjoint Scheme σ

instance AlgebraicGeometry.instHasFiniteCoproductsScheme :

CategoryTheory.Limits.HasFiniteCoproducts Scheme

instance AlgebraicGeometry.instMonoCoprodScheme :

CategoryTheory.Limits.MonoCoprod Scheme

noncomputable def AlgebraicGeometry.sigmaOpenCover {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] :

(∐ g).OpenCover

The cover of ∐ X by the Xᵢ.

Instances For

@[simp]

theorem AlgebraicGeometry.sigmaOpenCover_I₀ {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] :

(sigmaOpenCover g).I₀ = σ

@[simp]

theorem AlgebraicGeometry.sigmaOpenCover_X {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] (a✝ : σ) :

(sigmaOpenCover g).X a✝ = g a✝

@[simp]

theorem AlgebraicGeometry.sigmaOpenCover_f {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] (b : σ) :

(sigmaOpenCover g).f b = CategoryTheory.Limits.Sigma.ι g b

noncomputable def AlgebraicGeometry.sigmaMk {ι : Type u} (f : ι → Scheme) :

(i : ι) × ↥(f i) ≃ₜ ↥(∐ f)

The underlying topological space of the coproduct is homeomorphic to the disjoint union.

Instances For

@[simp]

theorem AlgebraicGeometry.sigmaMk_mk {ι : Type u} (f : ι → Scheme) (i : ι) (x : ↥(f i)) :

(sigmaMk f) ⟨i, x⟩ = (CategoryTheory.Limits.Sigma.ι f i) x

theorem AlgebraicGeometry.isOpenImmersion_sigmaDesc {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] {X : Scheme} (α : (i : σ) → g i ⟶ X) [∀ (i : σ), IsOpenImmersion (α i)] (hα : Pairwise (Function.onFun Disjoint fun (x : σ) => Set.range ⇑(α x))) :

IsOpenImmersion (CategoryTheory.Limits.Sigma.desc α)

theorem AlgebraicGeometry.nonempty_isColimit_cofanMk_of {σ : Type v} [Small.{u, v} σ] {X : σ → Scheme} {S : Scheme} (f : (i : σ) → X i ⟶ S) [∀ (i : σ), IsOpenImmersion (f i)] (hcov : ⨆ (i : σ), Scheme.Hom.opensRange (f i) = ⊤) (hdisj : Pairwise (Function.onFun Disjoint fun (x : σ) => Scheme.Hom.opensRange (f x))) :

Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk S f))

S is the disjoint union of Xᵢ if the Xᵢ are covering, pairwise disjoint open subschemes of S.

noncomputable def AlgebraicGeometry.coprodIsoSigma (X Y : Scheme) :

X ⨿ Y ≅ ∐ fun (i : ULift.{u, 0} CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.casesOn i.down X Y

(Implementation Detail) The coproduct of the two schemes is given by indexed coproducts over WalkingPair.

Instances For

theorem AlgebraicGeometry.ι_left_coprodIsoSigma_inv (X Y : Scheme) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (i : ULift.{u, 0} CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.casesOn i.down X Y) { down := CategoryTheory.Limits.WalkingPair.left }) (coprodIsoSigma X Y).inv = CategoryTheory.Limits.coprod.inl

theorem AlgebraicGeometry.ι_right_coprodIsoSigma_inv (X Y : Scheme) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (i : ULift.{u, 0} CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.casesOn i.down X Y) { down := CategoryTheory.Limits.WalkingPair.right }) (coprodIsoSigma X Y).inv = CategoryTheory.Limits.coprod.inr

instance AlgebraicGeometry.instIsOpenImmersionInlScheme (X Y : Scheme) :

IsOpenImmersion CategoryTheory.Limits.coprod.inl

instance AlgebraicGeometry.instIsOpenImmersionInrScheme (X Y : Scheme) :

IsOpenImmersion CategoryTheory.Limits.coprod.inr

theorem AlgebraicGeometry.isCompl_range_inl_inr (X Y : Scheme) :

IsCompl (Set.range ⇑CategoryTheory.Limits.coprod.inl) (Set.range ⇑CategoryTheory.Limits.coprod.inr)

theorem AlgebraicGeometry.isCompl_opensRange_inl_inr (X Y : Scheme) :

IsCompl (Scheme.Hom.opensRange CategoryTheory.Limits.coprod.inl) (Scheme.Hom.opensRange CategoryTheory.Limits.coprod.inr)

@[simp]

theorem AlgebraicGeometry.inl_ne_inr (X Y : Scheme) (x : ↥X) (y : ↥Y) :

CategoryTheory.Limits.coprod.inl x ≠ CategoryTheory.Limits.coprod.inr y

@[simp]

theorem AlgebraicGeometry.inr_ne_inl (X Y : Scheme) (x : ↥X) (y : ↥Y) :

CategoryTheory.Limits.coprod.inr y ≠ CategoryTheory.Limits.coprod.inl x

noncomputable def AlgebraicGeometry.coprodMk (X Y : Scheme) :

↥X ⊕ ↥Y ≃ₜ ↥(X ⨿ Y)

The underlying topological space of the coproduct is homeomorphic to the disjoint union

Instances For

@[simp]

theorem AlgebraicGeometry.coprodMk_inl (X Y : Scheme) (x : ↥X) :

(coprodMk X Y) (Sum.inl x) = CategoryTheory.Limits.coprod.inl x

@[simp]

theorem AlgebraicGeometry.coprodMk_inr (X Y : Scheme) (x : ↥Y) :

(coprodMk X Y) (Sum.inr x) = CategoryTheory.Limits.coprod.inr x

noncomputable def AlgebraicGeometry.coprodOpenCover (X Y : Scheme) :

(X ⨿ Y).OpenCover

The open cover of the coproduct of two schemes.

Instances For

theorem AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsOpenImmersion f] [IsOpenImmersion g] (hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)) :

Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g))

If X and Y are open disjoint and covering open subschemes of S, S is the disjoint union of X and Y.

theorem AlgebraicGeometry.isPullback_inl_inl_coprodMap {X Y X' Y' : Scheme} (f : X ⟶ X') (g : Y ⟶ Y') :

CategoryTheory.IsPullback f CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.map f g)

theorem AlgebraicGeometry.isPullback_inr_inr_coprodMap {X Y X' Y' : Scheme} (f : X ⟶ X') (g : Y ⟶ Y') :

CategoryTheory.IsPullback g CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.map f g)

instance AlgebraicGeometry.instFinitaryExtensiveScheme :

CategoryTheory.FinitaryExtensive Scheme

noncomputable def AlgebraicGeometry.Scheme.coprodPresheafObjIso {X Y : Scheme} (U : (X ⨿ Y).Opens) :

The sections on coproducts of schemes are the (categorical) product of the sections on the components

Instances For

@[simp]

theorem AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst {X Y : Scheme} (U : (X ⨿ Y).Opens) :

CategoryTheory.CategoryStruct.comp (coprodPresheafObjIso U).hom CategoryTheory.Limits.prod.fst = Hom.app CategoryTheory.Limits.coprod.inl U

@[simp]

@[simp]

theorem AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd {X Y : Scheme} (U : (X ⨿ Y).Opens) :

CategoryTheory.CategoryStruct.comp (coprodPresheafObjIso U).hom CategoryTheory.Limits.prod.snd = Hom.app CategoryTheory.Limits.coprod.inr U

@[simp]

noncomputable def AlgebraicGeometry.coprodSpec (R S : Type u) [CommRing R] [CommRing S] :

Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S) ⟶ Spec (CommRingCat.of (R × S))

The map Spec R ⨿ Spec S ⟶ Spec (R × S). This is an isomorphism as witnessed by an IsIso instance provided below.

Instances For

@[simp]

theorem AlgebraicGeometry.coprodSpec_inl (R S : Type u) [CommRing R] [CommRing S] :

CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (coprodSpec R S) = Spec.map (CommRingCat.ofHom (RingHom.fst R S))

theorem AlgebraicGeometry.coprodSpec_inl_assoc (R S : Type u) [CommRing R] [CommRing S] {Z : Scheme} (h : Spec (CommRingCat.of (R × S)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (coprodSpec R S) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) h

@[simp]

theorem AlgebraicGeometry.coprodSpec_inr (R S : Type u) [CommRing R] [CommRing S] :

CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (coprodSpec R S) = Spec.map (CommRingCat.ofHom (RingHom.snd R S))

theorem AlgebraicGeometry.coprodSpec_inr_assoc (R S : Type u) [CommRing R] [CommRing S] {Z : Scheme} (h : Spec (CommRingCat.of (R × S)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (coprodSpec R S) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) h

theorem AlgebraicGeometry.coprodSpec_coprodMk (R S : Type u) [CommRing R] [CommRing S] (x : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))) :

(coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) x) = (PrimeSpectrum.primeSpectrumProd R S).symm x

theorem AlgebraicGeometry.coprodSpec_apply (R S : Type u) [CommRing R] [CommRing S] (x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))) :

(coprodSpec R S) x = (PrimeSpectrum.primeSpectrumProd R S).symm ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))).symm x)

theorem AlgebraicGeometry.isIso_stalkMap_coprodSpec (R S : Type u) [CommRing R] [CommRing S] (x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))) :

CategoryTheory.IsIso (Scheme.Hom.stalkMap (coprodSpec R S) x)

instance AlgebraicGeometry.instIsIsoSchemeCoprodSpec (R S : Type u) [CommRing R] [CommRing S] :

CategoryTheory.IsIso (coprodSpec R S)

instance AlgebraicGeometry.instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec (R S : CommRingCat ᵒᵖ) :

CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison Scheme.Spec R S)

instance AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec :

CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) Scheme.Spec

instance AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec :

CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) Scheme.Spec

instance AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite {J : Type u_1} [Finite J] :

CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) Scheme.Spec

noncomputable def AlgebraicGeometry.sigmaSpec {ι : Type u} (R : ι → CommRingCat) :

(∐ fun (i : ι) => Spec (R i)) ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))

The canonical map ∐ Spec Rᵢ ⟶ Spec (Π Rᵢ). This is an isomorphism when the product is finite.

Instances For

@[simp]

theorem AlgebraicGeometry.ι_sigmaSpec {ι : Type u} (R : ι → CommRingCat) (i : ι) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (i : ι) => Spec (R i)) i) (sigmaSpec R) = Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) => ↑(R i)) i))

@[simp]

theorem AlgebraicGeometry.ι_sigmaSpec_assoc {ι : Type u} (R : ι → CommRingCat) (i : ι) {Z : Scheme} (h : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (i : ι) => Spec (R i)) i) (CategoryTheory.CategoryStruct.comp (sigmaSpec R) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) => ↑(R i)) i))) h

instance AlgebraicGeometry.instIsOpenImmersionMapOfHomForallEvalRingHom {ι : Type u} (i : ι) (R : ι → Type (max u_1 u)) [(i : ι) → CommRing (R i)] :

IsOpenImmersion (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) => R x) i)))

instance AlgebraicGeometry.instIsOpenImmersionSigmaSpec {ι : Type u} (R : ι → CommRingCat) :

IsOpenImmersion (sigmaSpec R)

instance AlgebraicGeometry.instIsIsoSchemeSigmaSpecOfFinite {ι : Type u} [Finite ι] (R : ι → CommRingCat) :

CategoryTheory.IsIso (sigmaSpec R)

instance AlgebraicGeometry.instIsAffineSigmaObjScheme {σ : Type v} (g : σ → Scheme) [Finite σ] [∀ (i : σ), IsAffine (g i)] :

IsAffine (∐ g)

instance AlgebraicGeometry.instIsAffineCoprodScheme {X Y : Scheme} [IsAffine X] [IsAffine Y] :

IsAffine (X ⨿ Y)

theorem AlgebraicGeometry.IsAffineOpen.iSup_of_disjoint {σ : Type v} {X : Scheme} [Finite σ] {U : σ → X.Opens} (hU : ∀ (i : σ), IsAffineOpen (U i)) (hU' : Pairwise (Function.onFun Disjoint U)) :

IsAffineOpen (iSup U)

theorem AlgebraicGeometry.IsAffineOpen.biSup_of_disjoint {σ : Type v} {X : Scheme} {s : Set σ} (hs : s.Finite) {U : σ → X.Opens} (hU : ∀ i ∈ s, IsAffineOpen (U i)) (hU' : s.Pairwise (Function.onFun Disjoint U)) :

IsAffineOpen (⨆ i ∈ s, U i)

theorem AlgebraicGeometry.IsAffineOpen.sup_of_disjoint {X : Scheme} {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (H : Disjoint U V) :

IsAffineOpen (U ⊔ V)

@[instance 100]

instance AlgebraicGeometry.instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat {X : Scheme} [Finite ↥X] [DiscreteTopology ↥X] :

instance AlgebraicGeometry.instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion {U X Y : Scheme} (f : U ⟶ X) (g : U ⟶ Y) [IsOpenImmersion f] [IsOpenImmersion g] (i : CategoryTheory.Limits.WalkingPair) :

CategoryTheory.Mono (((CategoryTheory.Limits.span f g).comp Scheme.forget).map (CategoryTheory.Limits.WidePushoutShape.Hom.init i))

instance AlgebraicGeometry.instIsOpenImmersionMapWalkingSpanSchemeSpan {U X Y : Scheme} (f : U ⟶ X) (g : U ⟶ Y) [IsOpenImmersion f] [IsOpenImmersion g] {i j : CategoryTheory.Limits.WalkingSpan} (t : i ⟶ j) :

IsOpenImmersion ((CategoryTheory.Limits.span f g).map t)

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instCartesianMonoidalCategoryScheme :

CategoryTheory.CartesianMonoidalCategory Scheme

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instBraidedCategoryScheme :

CategoryTheory.BraidedCategory Scheme

theorem AlgebraicGeometry.Scheme.isAffine_of_isLimit {I : Type u_1} [CategoryTheory.Category.{v_1, u_1} I] {D : CategoryTheory.Functor I Scheme} (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), IsAffine (D.obj i)] :