(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 instance AlgebraicGeometry.instOverTerminalScheme (X : AlgebraicGeometry.Scheme) : X.Over (⊤_ AlgebraicGeometry.Scheme)

Equations

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

noncomputable instance AlgebraicGeometry.instIsOverTerminalScheme {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.Scheme.Hom.IsOver f (⊤_ AlgebraicGeometry.Scheme)

Equations

• ⋯ = ⋯

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_c_app (X : AlgebraicGeometry.Scheme) (x✝ : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ) : X.emptyTo.c.app x✝ = CommRingCat.punitIsTerminal.from (X.presheaf.obj x✝)

@[simp]

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

theorem AlgebraicGeometry.Scheme.empty_ext {X : AlgebraicGeometry.Scheme} (f 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 Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsEmpty ↑↑X.toPresheafedSpace] : AlgebraicGeometry.IsOpenImmersion f

Equations

• ⋯ = ⋯

@[instance 100]

noncomputable instance AlgebraicGeometry.isIso_of_isEmpty {X 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'_f {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (x✝ x✝¹ : ι) (x✝² : x✝ ≠ x✝¹) : (AlgebraicGeometry.disjointGlueData' f).f x✝ x✝¹ x✝² = (f x✝).emptyTo

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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 = { toGlueData := CategoryTheory.GlueData.ofGlueData' (AlgebraicGeometry.disjointGlueData' f), f_open := ⋯ }

@[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_U {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (a✝ : (AlgebraicGeometry.disjointGlueData' f).J) : (AlgebraicGeometry.disjointGlueData f).U a✝ = f a✝

@[simp]

theorem AlgebraicGeometry.disjointGlueData_t {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i 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_J {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) : (AlgebraicGeometry.disjointGlueData f).J = ι

@[simp]

theorem AlgebraicGeometry.disjointGlueData_f {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i j : (AlgebraicGeometry.disjointGlueData' f).J) : (AlgebraicGeometry.disjointGlueData f).f i j = (AlgebraicGeometry.disjointGlueData' f).f' i 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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 {ι : 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_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_hom {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f i) (AlgebraicGeometry.sigmaIsoGlued f).hom = (AlgebraicGeometry.disjointGlueData 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

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).base x = (CategoryTheory.Limits.Sigma.ι f j).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).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 := ⋯, map_prop := ⋯ }

@[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).base x

noncomputable def AlgebraicGeometry.coprodIsoSigma (X Y : AlgebraicGeometry.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 : AlgebraicGeometry.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 }) (AlgebraicGeometry.coprodIsoSigma X Y).inv = CategoryTheory.Limits.coprod.inl

theorem AlgebraicGeometry.ι_right_coprodIsoSigma_inv (X Y : AlgebraicGeometry.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 }) (AlgebraicGeometry.coprodIsoSigma X Y).inv = CategoryTheory.Limits.coprod.inr

noncomputable instance AlgebraicGeometry.instIsOpenImmersionInlScheme (X Y : AlgebraicGeometry.Scheme) : AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.coprod.inl

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.instIsOpenImmersionInrScheme (X Y : AlgebraicGeometry.Scheme) : AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.coprod.inr

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.isCompl_range_inl_inr (X Y : AlgebraicGeometry.Scheme) : IsCompl (Set.range ⇑CategoryTheory.Limits.coprod.inl.base) (Set.range ⇑CategoryTheory.Limits.coprod.inr.base)

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

noncomputable def AlgebraicGeometry.coprodMk (X Y : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : (AlgebraicGeometry.coprodMk X Y) (Sum.inl x) = CategoryTheory.Limits.coprod.inl.base x

@[simp]

theorem AlgebraicGeometry.coprodMk_inr (X Y : AlgebraicGeometry.Scheme) (x : ↑↑Y.toPresheafedSpace) : (AlgebraicGeometry.coprodMk X Y) (Sum.inr x) = CategoryTheory.Limits.coprod.inr.base x

noncomputable def AlgebraicGeometry.coprodOpenCover (X Y : AlgebraicGeometry.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.

noncomputable def AlgebraicGeometry.coprodSpec (R S : Type u) [CommRing R] [CommRing S] : AlgebraicGeometry.Spec (CommRingCat.of R) ⨿ AlgebraicGeometry.Spec (CommRingCat.of S) ⟶ AlgebraicGeometry.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 (AlgebraicGeometry.coprodSpec R S) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.fst R S))

theorem AlgebraicGeometry.coprodSpec_inl_assoc (R S : Type u) [CommRing R] [CommRing S] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (R × S)) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.coprodSpec R S) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.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 (AlgebraicGeometry.coprodSpec R S) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.snd R S))

theorem AlgebraicGeometry.coprodSpec_inr_assoc (R S : Type u) [CommRing R] [CommRing S] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (R × S)) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.coprodSpec R S) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.snd R S))) h

theorem AlgebraicGeometry.coprodSpec_coprodMk (R S : Type u) [CommRing R] [CommRing S] (x : ↑↑(AlgebraicGeometry.Spec (CommRingCat.of R)).toPresheafedSpace ⊕ ↑↑(AlgebraicGeometry.Spec (CommRingCat.of S)).toPresheafedSpace) : (AlgebraicGeometry.coprodSpec R S).base ((AlgebraicGeometry.coprodMk (AlgebraicGeometry.Spec (CommRingCat.of R)) (AlgebraicGeometry.Spec (CommRingCat.of S))) x) = (PrimeSpectrum.primeSpectrumProd R S).symm x

theorem AlgebraicGeometry.coprodSpec_apply (R S : Type u) [CommRing R] [CommRing S] (x : ↑↑(AlgebraicGeometry.Spec (CommRingCat.of R) ⨿ AlgebraicGeometry.Spec (CommRingCat.of S)).toPresheafedSpace) : (AlgebraicGeometry.coprodSpec R S).base x = (PrimeSpectrum.primeSpectrumProd R S).symm ((AlgebraicGeometry.coprodMk (AlgebraicGeometry.Spec (CommRingCat.of R)) (AlgebraicGeometry.Spec (CommRingCat.of S))).symm x)

theorem AlgebraicGeometry.isIso_stalkMap_coprodSpec (R S : Type u) [CommRing R] [CommRing S] (x : ↑↑(AlgebraicGeometry.Spec (CommRingCat.of R) ⨿ AlgebraicGeometry.Spec (CommRingCat.of S)).toPresheafedSpace) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.coprodSpec R S) x)

noncomputable instance AlgebraicGeometry.instIsIsoSchemeCoprodSpec (R S : Type u) [CommRing R] [CommRing S] : CategoryTheory.IsIso (AlgebraicGeometry.coprodSpec R S)

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec (R S : CommRingCatᵒᵖ) : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison AlgebraicGeometry.Scheme.Spec R S)

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) AlgebraicGeometry.Scheme.Spec

Equations

• AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec = ⋯

noncomputable instance AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) AlgebraicGeometry.Scheme.Spec

Equations

• AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec = ⋯

noncomputable instance AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFintype {J : Type u_1} [Fintype J] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) AlgebraicGeometry.Scheme.Spec

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite {J : Type u_1} [Finite J] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) AlgebraicGeometry.Scheme.Spec

Equations

• ⋯ = ⋯

noncomputable def AlgebraicGeometry.sigmaSpec {ι : Type u} (R : ι → CommRingCat) : (∐ fun (i : ι) => AlgebraicGeometry.Spec (R i)) ⟶ AlgebraicGeometry.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 : ι) => AlgebraicGeometry.Spec (R i)) i) (AlgebraicGeometry.sigmaSpec R) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) => ↑(R i)) i))

theorem AlgebraicGeometry.ι_sigmaSpec_assoc {ι : Type u} (R : ι → CommRingCat) (i : ι) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (i : ι) => AlgebraicGeometry.Spec (R i)) i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.sigmaSpec R) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) => ↑(R i)) i))) h

noncomputable instance AlgebraicGeometry.instIsIsoSchemeSigmaSpecOfFinite {ι : Type u} [Finite ι] (R : ι → CommRingCat) : CategoryTheory.IsIso (AlgebraicGeometry.sigmaSpec R)

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.instIsAffineSigmaObjSchemeOfFinite {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) [Finite ι] [∀ (i : ι), AlgebraicGeometry.IsAffine (f i)] : AlgebraicGeometry.IsAffine (∐ f)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯