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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

One or more equations did not get rendered due to their size.

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)

Equations

AlgebraicGeometry.instOverTerminalScheme X = { hom := CategoryTheory.Limits.terminal.from X }

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) :

The map from the empty scheme.

Equations

One or more equations did not get rendered due to their size.

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} :

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

@[implicit_reducible]

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

Unique (∅ ⟶ X)

Equations

X.hom_unique_of_empty_source = { default := X.emptyTo, uniq := ⋯ }

noncomputable def AlgebraicGeometry.emptyIsInitial :

CategoryTheory.Limits.IsInitial ∅

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

Equations

AlgebraicGeometry.emptyIsInitial = CategoryTheory.Limits.IsInitial.ofUnique ∅

Instances For

@[simp]

theorem AlgebraicGeometry.emptyIsInitial_to :

emptyIsInitial.to = Scheme.emptyTo

instance AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme :

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 .

Equations

AlgebraicGeometry.isInitialOfIsEmpty = AlgebraicGeometry.emptyIsInitial.ofIso (CategoryTheory.asIso (AlgebraicGeometry.emptyIsInitial.to X))

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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

AlgebraicGeometry.specPunitIsInitial = AlgebraicGeometry.specPUnitIsInitial

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

Equations

One or more equations did not get rendered due to their size.

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

Equations

One or more equations did not get rendered due to their size.

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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

One or more equations did not get rendered due to their size.

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

Equations

One or more equations did not get rendered due to their size.

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.

Equations

One or more equations did not get rendered due to their size.

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

Equations

One or more equations did not get rendered due to their size.

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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

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

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

Equations

AlgebraicGeometry.instCartesianMonoidalCategoryScheme = CategoryTheory.CartesianMonoidalCategory.ofHasFiniteProducts

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instBraidedCategoryScheme :

CategoryTheory.BraidedCategory Scheme

Equations

AlgebraicGeometry.instBraidedCategoryScheme = CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory

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)] :