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

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

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

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

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

@[deprecated AlgebraicGeometry.Scheme.IsLocallyDirected.openCover (since := "2025-06-02")]

def AlgebraicGeometry.sigmaOpenCover {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] :

(CategoryTheory.Limits.colimit F).OpenCover

The open cover of the coproduct.

Equations

@AlgebraicGeometry.sigmaOpenCover = @AlgebraicGeometry.Scheme.IsLocallyDirected.openCover

Instances For

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

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

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

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.

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

(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

instance AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite_1 {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.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

Equations

AlgebraicGeometry.instCartesianMonoidalCategoryScheme = CategoryTheory.CartesianMonoidalCategory.ofHasFiniteProducts

noncomputable instance AlgebraicGeometry.instBraidedCategoryScheme :

CategoryTheory.BraidedCategory Scheme

Equations

AlgebraicGeometry.instBraidedCategoryScheme = CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory