(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_base_apply (X : AlgebraicGeometry.Scheme) (x : ↑↑∅.toPresheafedSpace) : X.emptyTo.base x = PEmpty.elim x

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

theorem AlgebraicGeometry.Scheme.empty_ext_iff {X : AlgebraicGeometry.Scheme} {f : ∅ ⟶ X} {g : ∅ ⟶ X} : f = g ↔ True

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'_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'_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'_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_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

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

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 : (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_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_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).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 := ⋯, IsOpen := ⋯ }

@[simp]

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

@[simp]

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

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 : AlgebraicGeometry.Scheme) (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 : AlgebraicGeometry.Scheme) (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 : AlgebraicGeometry.Scheme) (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 : AlgebraicGeometry.Scheme) (Y : AlgebraicGeometry.Scheme) : AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.coprod.inl

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

noncomputable def AlgebraicGeometry.coprodOpenCover (X : AlgebraicGeometry.Scheme) (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 : Type u) (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.

theorem AlgebraicGeometry.coprodSpec_inl_assoc (R : Type u) (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_inl (R : Type u) (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_inr_assoc (R : Type u) (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

@[simp]

theorem AlgebraicGeometry.coprodSpec_inr (R : Type u) (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_coprodMk (R : Type u) (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 : Type u) (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 : Type u) (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 : Type u) (S : Type u) [CommRing R] [CommRing S] : CategoryTheory.IsIso (AlgebraicGeometry.coprodSpec R S)

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec (R : CommRingCatᵒᵖ) (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

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

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

Equations

• AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec = CategoryTheory.Limits.preservesColimitsOfShapePemptyOfPreservesInitial AlgebraicGeometry.Scheme.Spec

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

Equations

• AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFintype = CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial AlgebraicGeometry.Scheme.Spec J

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

Equations

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

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

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

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

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 : AlgebraicGeometry.Scheme) (Y : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] : AlgebraicGeometry.IsAffine (X ⨿ Y)

Equations

• ⋯ = ⋯