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

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.

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) : ∅ ⟶ 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_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.toPresheafedSpace)ᵒᵖ) : 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)

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 : emptyIsInitial.to = Scheme.emptyTo

instance AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme : IsEmpty ↑↑∅.toPresheafedSpace

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

@[instance 100]

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

@[instance 100]

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

noncomputable def AlgebraicGeometry.isInitialOfIsEmpty {X : 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 (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]

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

instance AlgebraicGeometry.instHasInitialScheme : CategoryTheory.Limits.HasInitial Scheme

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

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

instance AlgebraicGeometry.instHasStrictInitialObjectsScheme : CategoryTheory.Limits.HasStrictInitialObjects Scheme

instance AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty {X : Scheme} [IsEmpty ↑↑X.toPresheafedSpace] (U : X.Opens) : Subsingleton ↑(X.presheaf.obj (Opposite.op U))

@[instance 100]

instance AlgebraicGeometry.instIsAffineOfSubsingletonCarrierCarrierCommRingCat {X : Scheme} [Subsingleton ↑↑X.toPresheafedSpace] : IsAffine X

noncomputable def AlgebraicGeometry.disjointGlueData' {ι : Type u} (f : ι → Scheme) : CategoryTheory.GlueData' 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'_t {ι : Type u} (f : ι → Scheme) (x✝ x✝¹ : ι) (x✝² : x✝ ≠ x✝¹) : (disjointGlueData' f).t x✝ x✝¹ x✝² = CategoryTheory.CategoryStruct.id ∅

@[simp]

theorem AlgebraicGeometry.disjointGlueData'_f {ι : Type u} (f : ι → Scheme) (x✝ x✝¹ : ι) (x✝² : x✝ ≠ x✝¹) : (disjointGlueData' f).f x✝ x✝¹ x✝² = (f x✝).emptyTo

@[simp]

theorem AlgebraicGeometry.disjointGlueData'_V {ι : Type u} (f : ι → Scheme) (x✝ x✝¹ : ι) (x✝² : x✝ ≠ x✝¹) : (disjointGlueData' f).V x✝ x✝¹ x✝² = ∅

@[simp]

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

@[simp]

theorem AlgebraicGeometry.disjointGlueData'_t' {ι : Type u} (f : ι → Scheme) (x✝ x✝¹ x✝² : ι) (x✝³ : x✝ ≠ x✝¹) (x✝⁴ : x✝ ≠ x✝²) (x✝⁵ : x✝¹ ≠ x✝²) : (disjointGlueData' f).t' x✝ x✝¹ x✝² x✝³ x✝⁴ x✝⁵ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f x✝).emptyTo (f x✝).emptyTo) (CategoryTheory.Limits.pullback (f x✝¹).emptyTo (f x✝¹).emptyTo).emptyTo

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def AlgebraicGeometry.toLocallyRingedSpaceCoproductCofan {ι : Type u} (f : ι → Scheme) : CategoryTheory.Limits.Cofan (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 : ι → Scheme) : CategoryTheory.Limits.IsColimit (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 : ι → Scheme) : CategoryTheory.CreatesColimit (CategoryTheory.Discrete.functor f) Scheme.forgetToLocallyRingedSpace

Equations

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

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

instance AlgebraicGeometry.instHasCoproductsSchemeOfUnivLE [UnivLE.{v, u}] : CategoryTheory.Limits.HasCoproducts Scheme

noncomputable def AlgebraicGeometry.sigmaIsoGlued {ι : Type u} (f : ι → Scheme) : ∐ f ≅ (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 {ι : Type u} (f : ι → Scheme) (i : (disjointGlueData f).J) : CategoryTheory.CategoryStruct.comp ((disjointGlueData f).ι i) (sigmaIsoGlued f).inv = CategoryTheory.Limits.Sigma.ι f i

@[simp]

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

@[simp]

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

@[simp]

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

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

instance AlgebraicGeometry.instIsOpenImmersionιScheme_1 {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] (i : σ) : IsOpenImmersion (CategoryTheory.Limits.Sigma.ι g i)

theorem AlgebraicGeometry.sigmaι_eq_iff {ι : Type u} (f : ι → Scheme) (i j : ι) (x : ↑↑(f i).toPresheafedSpace) (y : ↑↑(f j).toPresheafedSpace) : (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.

theorem AlgebraicGeometry.exists_sigmaι_eq {σ : Type v} (g : σ → Scheme) [Small.{u, v} σ] (x : ↑↑(∐ g).toPresheafedSpace) : ∃ (i : σ) (y : ↑↑(g i).toPresheafedSpace), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι g i).base) y = x

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

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

The open cover of the coproduct.

Equations

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

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

noncomputable def AlgebraicGeometry.sigmaMk {ι : Type u} (f : ι → 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 : ι → Scheme) (i : ι) (x : ↑↑(f i).toPresheafedSpace) : (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.

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.toPresheafedSpace ⊕ ↑↑Y.toPresheafedSpace ≃ₜ ↑↑(X ⨿ Y).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.coprodMk_inl (X Y : Scheme) (x : ↑↑X.toPresheafedSpace) : (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.toPresheafedSpace) : (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.

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.

@[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)).toPresheafedSpace ⊕ ↑↑(Spec (CommRingCat.of S)).toPresheafedSpace) : (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)).toPresheafedSpace) : (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)).toPresheafedSpace) : 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))

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