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

noncomputable instance AlgebraicGeometry.instHasTerminalScheme : CategoryTheory.Limits.HasTerminal AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.instHasTerminalScheme = ⋯

noncomputable instance AlgebraicGeometry.instIsAffineTerminalScheme : AlgebraicGeometry.IsAffine (⊤_ AlgebraicGeometry.Scheme)

Equations

• AlgebraicGeometry.instIsAffineTerminalScheme = ⋯

noncomputable instance AlgebraicGeometry.instHasFiniteLimitsScheme : CategoryTheory.Limits.HasFiniteLimits AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.instHasFiniteLimitsScheme = ⋯

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

The map from the empty scheme.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.emptyTo_val_base_apply (X : AlgebraicGeometry.Scheme) (x : ↑↑∅.toPresheafedSpace) : X.emptyTo.val.base x = PEmpty.elim x

@[simp]

theorem AlgebraicGeometry.Scheme.emptyTo_val_c_app (X : AlgebraicGeometry.Scheme) (U : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ) : X.emptyTo.val.c.app U = CommRingCat.punitIsTerminal.from (X.presheaf.obj U)

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

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

noncomputable instance AlgebraicGeometry.Scheme.hom_unique_of_empty_source (X : AlgebraicGeometry.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 ∅

@[simp]

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

noncomputable instance AlgebraicGeometry.instIsEmptyαTopologicalSpaceCarrierCommRingCatEmptyCollectionScheme : IsEmpty ↑↑∅.toPresheafedSpace

Equations

• AlgebraicGeometry.instIsEmptyαTopologicalSpaceCarrierCommRingCatEmptyCollectionScheme = ⋯

noncomputable instance AlgebraicGeometry.spec_punit_isEmpty : IsEmpty ↑↑(AlgebraicGeometry.Spec (CommRingCat.of PUnit.{u + 1} )).toPresheafedSpace

Equations

• AlgebraicGeometry.spec_punit_isEmpty = ⋯

@[instance 100]

noncomputable instance AlgebraicGeometry.isOpenImmersion_of_isEmpty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsEmpty ↑↑X.toPresheafedSpace] : AlgebraicGeometry.IsOpenImmersion f

Equations

• ⋯ = ⋯

@[instance 100]

noncomputable instance AlgebraicGeometry.isIso_of_isEmpty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsEmpty ↑↑Y.toPresheafedSpace] : CategoryTheory.IsIso f

Equations

• ⋯ = ⋯

noncomputable def AlgebraicGeometry.isInitialOfIsEmpty {X : AlgebraicGeometry.Scheme} [IsEmpty ↑↑X.toPresheafedSpace] : 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))

noncomputable def AlgebraicGeometry.specPunitIsInitial : CategoryTheory.Limits.IsInitial (AlgebraicGeometry.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.

@[instance 100]

noncomputable instance AlgebraicGeometry.isAffine_of_isEmpty {X : AlgebraicGeometry.Scheme} [IsEmpty ↑↑X.toPresheafedSpace] : AlgebraicGeometry.IsAffine X

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.instHasInitialScheme : CategoryTheory.Limits.HasInitial AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.instHasInitialScheme = ⋯

noncomputable instance AlgebraicGeometry.initial_isEmpty : IsEmpty ↑↑(⊥_ AlgebraicGeometry.Scheme).toPresheafedSpace

Equations

• AlgebraicGeometry.initial_isEmpty = ⋯

theorem AlgebraicGeometry.isAffineOpen_bot (X : AlgebraicGeometry.Scheme) : AlgebraicGeometry.IsAffineOpen ⊥

noncomputable instance AlgebraicGeometry.instHasStrictInitialObjectsScheme : CategoryTheory.Limits.HasStrictInitialObjects AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.instHasStrictInitialObjectsScheme = ⋯

noncomputable def AlgebraicGeometry.disjointGlueData' {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : CategoryTheory.GlueData' AlgebraicGeometry.Scheme

(Implementation Detail) The glue data associated to a disjoint union.

Equations

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

@[simp]

theorem AlgebraicGeometry.disjointGlueData'_J {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : (AlgebraicGeometry.disjointGlueData' f).J = ι

@[simp]

theorem AlgebraicGeometry.disjointGlueData'_V {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : ∀ (x x_1 : ι) (x_2 : x ≠ x_1), (AlgebraicGeometry.disjointGlueData' f).V x x_1 x_2 = ∅

@[simp]

theorem AlgebraicGeometry.disjointGlueData'_U {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : ∀ (a : ι), (AlgebraicGeometry.disjointGlueData' f).U a = f a

@[simp]

theorem AlgebraicGeometry.disjointGlueData'_f {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : ∀ (x x_1 : ι) (x_2 : x ≠ x_1), (AlgebraicGeometry.disjointGlueData' f).f x x_1 x_2 = (f x).emptyTo

@[simp]

theorem AlgebraicGeometry.disjointGlueData'_t {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : ∀ (x x_1 : ι) (x_2 : x ≠ x_1), (AlgebraicGeometry.disjointGlueData' f).t x x_1 x_2 = CategoryTheory.CategoryStruct.id ((fun (x x_3 : ι) (x : x ≠ x_3) => ∅) x x_1 x_2)

@[simp]

theorem AlgebraicGeometry.disjointGlueData'_t' {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : ∀ (x x_1 x_2 : ι) (x_3 : x ≠ x_1) (x_4 : x ≠ x_2) (x_5 : x_1 ≠ x_2), (AlgebraicGeometry.disjointGlueData' f).t' x x_1 x_2 x_3 x_4 x_5 = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((fun (x x_6 : ι) (x_7 : x ≠ x_6) => (f x).emptyTo) x x_1 x_3) ((fun (x x_6 : ι) (x_7 : x ≠ x_6) => (f x).emptyTo) x x_2 x_4)) (CategoryTheory.Limits.pullback ((fun (x x_6 : ι) (x_7 : x ≠ x_6) => (f x).emptyTo) x_1 x_2 x_5) ((fun (x x_6 : ι) (x_7 : x ≠ x_6) => (f x).emptyTo) x_1 x ⋯)).emptyTo

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

(Implementation Detail) The glue data associated to a disjoint union.

Equations

• AlgebraicGeometry.disjointGlueData f = let __spread.0 := CategoryTheory.GlueData.ofGlueData' (AlgebraicGeometry.disjointGlueData' f); { toGlueData := __spread.0, f_open := ⋯ }

@[simp]

theorem AlgebraicGeometry.disjointGlueData_f {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : (AlgebraicGeometry.disjointGlueData' f).J) (j : (AlgebraicGeometry.disjointGlueData' f).J) : (AlgebraicGeometry.disjointGlueData f).f i j = (AlgebraicGeometry.disjointGlueData' f).f' i j

@[simp]

theorem AlgebraicGeometry.disjointGlueData_t {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : (AlgebraicGeometry.disjointGlueData' f).J) (j : (AlgebraicGeometry.disjointGlueData' f).J) : (AlgebraicGeometry.disjointGlueData f).t i j = if h : i = j then CategoryTheory.eqToHom ⋯ else CategoryTheory.eqToHom ⋯

@[simp]

theorem AlgebraicGeometry.disjointGlueData_U {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : ∀ (a : (AlgebraicGeometry.disjointGlueData' f).J), (AlgebraicGeometry.disjointGlueData f).U a = f a

@[simp]

theorem AlgebraicGeometry.disjointGlueData_V {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (ij : (AlgebraicGeometry.disjointGlueData' f).J × (AlgebraicGeometry.disjointGlueData' f).J) : (AlgebraicGeometry.disjointGlueData f).V ij = if ij.1 = ij.2 then f ij.1 else ∅

@[simp]

theorem AlgebraicGeometry.disjointGlueData_J {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : (AlgebraicGeometry.disjointGlueData f).J = ι

noncomputable def AlgebraicGeometry.toLocallyRingedSpaceCoproductCofan {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : CategoryTheory.Limits.Cofan (AlgebraicGeometry.Scheme.toLocallyRingedSpace ∘ f)

(Implementation Detail) The cofan in LocallyRingedSpace associated to a disjoint union.

Equations

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

noncomputable def AlgebraicGeometry.toLocallyRingedSpaceCoproductCofanIsColimit {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : CategoryTheory.Limits.IsColimit (AlgebraicGeometry.toLocallyRingedSpaceCoproductCofan f)

(Implementation Detail) The cofan in LocallyRingedSpace associated to a disjoint union is a colimit.

Equations

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

noncomputable instance AlgebraicGeometry.instCreatesColimitSchemeLocallyRingedSpaceDiscreteFunctorForgetToLocallyRingedSpace {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : CategoryTheory.CreatesColimit (CategoryTheory.Discrete.functor f) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

Equations

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

noncomputable instance AlgebraicGeometry.instCreatesColimitsOfShapeSchemeLocallyRingedSpaceDiscreteForgetToLocallyRingedSpace {ι : Type u} : CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete ι) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

Equations

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

noncomputable instance AlgebraicGeometry.instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTop {ι : Type u} : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) AlgebraicGeometry.Scheme.forgetToTop

Equations

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

noncomputable instance AlgebraicGeometry.instHasCoproductsScheme : CategoryTheory.Limits.HasCoproducts AlgebraicGeometry.Scheme

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.instHasCoproductsScheme_1 : CategoryTheory.Limits.HasCoproducts AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.instHasCoproductsScheme_1 = ⋯

noncomputable instance AlgebraicGeometry.instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTop_1 {ι : Type} : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) AlgebraicGeometry.Scheme.forgetToTop

Equations

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

noncomputable instance AlgebraicGeometry.instPreservesColimitsOfShapeSchemeLocallyRingedSpaceDiscreteForgetToLocallyRingedSpace {ι : Type} : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

Equations

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

noncomputable def AlgebraicGeometry.sigmaIsoGlued {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : ∐ f ≅ (AlgebraicGeometry.disjointGlueData f).glued

(Implementation Detail) Coproduct of schemes is isomorphic to the disjoint union.

Equations

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

@[simp]

theorem AlgebraicGeometry.ι_sigmaIsoGlued_inv_assoc {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : (AlgebraicGeometry.disjointGlueData f).J) {Z : AlgebraicGeometry.Scheme} (h : ∐ f ⟶ Z) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.disjointGlueData f).ι i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.sigmaIsoGlued f).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f i) h

@[simp]

theorem AlgebraicGeometry.ι_sigmaIsoGlued_inv {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : (AlgebraicGeometry.disjointGlueData f).J) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.disjointGlueData f).ι i) (AlgebraicGeometry.sigmaIsoGlued f).inv = CategoryTheory.Limits.Sigma.ι f i

@[simp]

theorem AlgebraicGeometry.ι_sigmaIsoGlued_hom_assoc {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : ι) {Z : AlgebraicGeometry.Scheme} (h : (AlgebraicGeometry.disjointGlueData f).glued ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.sigmaIsoGlued f).hom h) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.disjointGlueData f).ι i) h

@[simp]

theorem AlgebraicGeometry.ι_sigmaIsoGlued_hom {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f i) (AlgebraicGeometry.sigmaIsoGlued f).hom = (AlgebraicGeometry.disjointGlueData f).ι i

noncomputable instance AlgebraicGeometry.instIsOpenImmersionιScheme {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : ι) : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.Sigma.ι f i)

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.sigmaι_eq_iff {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : ι) (j : ι) (x : ↑↑(f i).toPresheafedSpace) (y : ↑↑(f j).toPresheafedSpace) : (CategoryTheory.Limits.Sigma.ι f i).val.base x = (CategoryTheory.Limits.Sigma.ι f j).val.base y ↔ ⟨i, x⟩ = ⟨j, y⟩

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

The images of each component in the coproduct is disjoint.

theorem AlgebraicGeometry.exists_sigmaι_eq {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (x : ↑↑(∐ f).toPresheafedSpace) : ∃ (i : ι) (y : ↑↑(f i).toPresheafedSpace), (CategoryTheory.Limits.Sigma.ι f i).val.base y = x

theorem AlgebraicGeometry.iSup_opensRange_sigmaι {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : ⨆ (i : ι), AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι f i) = ⊤

noncomputable def AlgebraicGeometry.sigmaOpenCover {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : (∐ f).OpenCover

The open cover of the coproduct.

Equations

• AlgebraicGeometry.sigmaOpenCover f = { J := ι, obj := f, map := CategoryTheory.Limits.Sigma.ι f, f := fun (x : ↑↑(∐ f).toPresheafedSpace) => ⋯.choose, covers := ⋯, IsOpen := ⋯ }

@[simp]

theorem AlgebraicGeometry.sigmaOpenCover_map {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (b : ι) : (AlgebraicGeometry.sigmaOpenCover f).map b = CategoryTheory.Limits.Sigma.ι f b

@[simp]

theorem AlgebraicGeometry.sigmaOpenCover_obj {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : ∀ (a : ι), (AlgebraicGeometry.sigmaOpenCover f).obj a = f a

noncomputable def AlgebraicGeometry.sigmaMk {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : (i : ι) × ↑↑(f i).toPresheafedSpace ≃ₜ ↑↑(∐ f).toPresheafedSpace

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.

@[simp]

theorem AlgebraicGeometry.sigmaMk_mk {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : ι) (x : ↑↑(f i).toPresheafedSpace) : (AlgebraicGeometry.sigmaMk f) ⟨i, x⟩ = (CategoryTheory.Limits.Sigma.ι f i).val.base x