(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 { carrier := ℤ, commRing := Int.instCommRing })

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

noncomputable def AlgebraicGeometry.specULiftZIsTerminal : CategoryTheory.Limits.IsTerminal (Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })

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

instance AlgebraicGeometry.instHasTerminalScheme : CategoryTheory.Limits.HasTerminal Scheme

instance AlgebraicGeometry.instIsAffineTerminalScheme : IsAffine (⊤_ Scheme)

instance AlgebraicGeometry.instHasFiniteLimitsScheme : CategoryTheory.Limits.HasFiniteLimits Scheme

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.

@[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) : f = X.emptyTo

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.

@[simp]

theorem AlgebraicGeometry.emptyIsInitial_to : emptyIsInitial.to = Scheme.emptyTo

instance AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme : IsEmpty ↥∅

instance AlgebraicGeometry.spec_punit_isEmpty : IsEmpty ↥(Spec { carrier := PUnit.{u + 1}, commRing := PUnit.commRing })

@[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 .

noncomputable def AlgebraicGeometry.specPUnitIsInitial : CategoryTheory.Limits.IsInitial (Spec { carrier := PUnit.{u + 1}, commRing := PUnit.commRing })

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

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

def AlgebraicGeometry.specPunitIsInitial : CategoryTheory.Limits.IsInitial (Spec { carrier := PUnit.{u + 1}, commRing := PUnit.commRing })

Alias of AlgebraicGeometry.specPUnitIsInitial.

---

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

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] : IsAffine 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] : IsAffine 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) : IsAffineOpen U

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) : IsEmpty ↥Z

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ᵢ.

@[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.

@[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.

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

@[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.

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) : (X ⨿ Y).presheaf.obj (Opposite.op U) ≅ X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inl.base).obj U)) ⨯ Y.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inr.base).obj U))

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

@[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]

theorem AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc {X Y : Scheme} (U : (X ⨿ Y).Opens) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inl.base).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coprodPresheafObjIso U).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (Hom.app CategoryTheory.Limits.coprod.inl U) h

@[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]

theorem AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc {X Y : Scheme} (U : (X ⨿ Y).Opens) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inr.base).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coprodPresheafObjIso U).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp (Hom.app CategoryTheory.Limits.coprod.inr U) h

noncomputable def AlgebraicGeometry.coprodSpec (R S : Type u) [CommRing R] [CommRing S] : Spec { carrier := R, commRing := inst✝ } ⨿ Spec { carrier := S, commRing := inst✝¹ } ⟶ Spec { carrier := R × S, commRing := Prod.instCommRing }

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

@[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 { carrier := R × S, commRing := Prod.instCommRing } ⟶ 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 { carrier := R × S, commRing := Prod.instCommRing } ⟶ 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 { carrier := R, commRing := inst✝ }) ⊕ ↥(Spec { carrier := S, commRing := inst✝¹ })) : (coprodSpec R S) ((coprodMk (Spec { carrier := R, commRing := inst✝ }) (Spec { carrier := S, commRing := inst✝¹ })) x) = (PrimeSpectrum.primeSpectrumProd R S).symm x

theorem AlgebraicGeometry.coprodSpec_apply (R S : Type u) [CommRing R] [CommRing S] (x : ↥(Spec { carrier := R, commRing := inst✝ } ⨿ Spec { carrier := S, commRing := inst✝¹ })) : (coprodSpec R S) x = (PrimeSpectrum.primeSpectrumProd R S).symm ((coprodMk (Spec { carrier := R, commRing := inst✝ }) (Spec { carrier := S, commRing := inst✝¹ })).symm x)

theorem AlgebraicGeometry.isIso_stalkMap_coprodSpec (R S : Type u) [CommRing R] [CommRing S] (x : ↥(Spec { carrier := R, commRing := inst✝ } ⨿ Spec { carrier := S, commRing := inst✝¹ })) : 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 { carrier := (i : ι) → ↑(R i), commRing := Pi.commRing }

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

@[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 { carrier := (i : ι) → ↑(R i), commRing := Pi.commRing } ⟶ 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] : IsAffine 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)

noncomputable instance AlgebraicGeometry.instCartesianMonoidalCategoryScheme : CategoryTheory.CartesianMonoidalCategory Scheme

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)] : IsAffine c.pt