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

noncomputable def AlgebraicGeometry.specULiftZIsTerminal : CategoryTheory.Limits.IsTerminal (Spec (CommRingCat.of (ULift.{u, 0} ℤ)))

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_base (X : Scheme) : X.emptyTo.base = TopCat.ofHom { toFun := fun (x : PEmpty.{u + 1}) => x.elim, continuous_toFun := ⋯ }

@[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✝)

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

noncomputable def AlgebraicGeometry.specPunitIsInitial : CategoryTheory.Limits.IsInitial (Spec (CommRingCat.of PUnit.{u + 1}))

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

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

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 u} (f : ι → Scheme) (i j : ι) (x : ↥(f i)) (y : ↥(f j)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι f i).base) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι f j).base) y ↔ ⟨i, x⟩ = ⟨j, y⟩

theorem AlgebraicGeometry.disjoint_opensRange_sigmaι {ι : Type u} (f : ι → Scheme) (i j : ι) (h : i ≠ j) : Disjoint (Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι f i)) (Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι f j))

The images of each component in the coproduct is disjoint.

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

The cover of ∐ X by the Xᵢ.

@[simp]

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

@[simp]

theorem AlgebraicGeometry.sigmaOpenCover_map {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] (b : σ) : (sigmaOpenCover g).map b = CategoryTheory.Limits.Sigma.ι g b

@[simp]

theorem AlgebraicGeometry.sigmaOpenCover_f {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] (x : ↥(CategoryTheory.Limits.colimit (CategoryTheory.Discrete.functor g))) : (sigmaOpenCover g).f x = ((Scheme.IsLocallyDirected.openCover (CategoryTheory.Discrete.functor g)).f x).as

@[simp]

theorem AlgebraicGeometry.sigmaOpenCover_J {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] : (sigmaOpenCover g).J = σ

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.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι f i).base) 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 ⇑(CategoryTheory.ConcreteCategory.hom (α x).base))) : 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.ConcreteCategory.hom CategoryTheory.Limits.coprod.inl.base)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.coprod.inr.base))

theorem AlgebraicGeometry.isCompl_opensRange_inl_inr (X Y : Scheme) : IsCompl (Scheme.Hom.opensRange CategoryTheory.Limits.coprod.inl) (Scheme.Hom.opensRange CategoryTheory.Limits.coprod.inr)

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.ConcreteCategory.hom CategoryTheory.Limits.coprod.inl.base) x

@[simp]

theorem AlgebraicGeometry.coprodMk_inr (X Y : Scheme) (x : ↥Y) : (coprodMk X Y) (Sum.inr x) = (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.coprod.inr.base) 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.

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.

@[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))) : (CategoryTheory.ConcreteCategory.hom (coprodSpec R S).base) ((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))) : (CategoryTheory.ConcreteCategory.hom (coprodSpec R S).base) 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.

@[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.instIsAffineSigmaObjSchemeOfFinite {ι : Type u} (f : ι → Scheme) [Finite ι] [∀ (i : ι), IsAffine (f i)] : IsAffine (∐ f)

instance AlgebraicGeometry.instIsAffineCoprodScheme (X Y : Scheme) [IsAffine X] [IsAffine Y] : IsAffine (X ⨿ Y)

noncomputable instance AlgebraicGeometry.instCartesianMonoidalCategoryScheme : CategoryTheory.CartesianMonoidalCategory Scheme

noncomputable instance AlgebraicGeometry.instBraidedCategoryScheme : CategoryTheory.BraidedCategory Scheme