Documentation

Mathlib.AlgebraicGeometry.Limits

(Co)Limits of Schemes #

We construct various limits and colimits in the category of schemes.

TODO #

Spec ℤ is the terminal object in the category of schemes.

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

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.Scheme.emptyTo (X : Scheme) :

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 := }
Equations

The empty scheme is the initial object in the category of schemes.

Equations
@[instance 100]
@[instance 100]

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]

(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✝¹) :
@[simp]
theorem AlgebraicGeometry.disjointGlueData'_V {ι : Type u} (f : ιScheme) (x✝ x✝¹ : ι) (x✝² : x✝ x✝¹) :
(disjointGlueData' f).V x✝ x✝¹ x✝² =
@[simp]
theorem AlgebraicGeometry.disjointGlueData'_t' {ι : Type u} (f : ιScheme) (x✝ x✝¹ x✝² : ι) (x✝³ : x✝ x✝¹) (x✝⁴ : x✝ x✝²) (x✝⁵ : x✝¹ x✝²) :
@[simp]
theorem AlgebraicGeometry.disjointGlueData'_U {ι : Type u} (f : ιScheme) (a✝ : ι) :
(disjointGlueData' f).U a✝ = f a✝
@[simp]
@[simp]
theorem AlgebraicGeometry.disjointGlueData'_f {ι : Type u} (f : ιScheme) (x✝ x✝¹ : ι) (x✝² : x✝ x✝¹) :
(disjointGlueData' f).f x✝ x✝¹ x✝² = (f x✝).emptyTo
noncomputable def AlgebraicGeometry.disjointGlueData {ι : Type u} (f : ιScheme) :

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

Equations
@[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_f {ι : Type u} (f : ιScheme) (i j : (disjointGlueData' f).J) :
@[simp]
theorem AlgebraicGeometry.disjointGlueData_J {ι : Type u} (f : ιScheme) :
@[simp]
theorem AlgebraicGeometry.disjointGlueData_U {ι : Type u} (f : ιScheme) (a✝ : (disjointGlueData' f).J) :
(disjointGlueData f).U a✝ = f a✝
@[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

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

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

(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 def AlgebraicGeometry.sigmaIsoGlued {ι : Type u} (f : ιScheme) :

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

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

The images of each component in the coproduct is disjoint.

theorem AlgebraicGeometry.exists_sigmaι_eq {σ : Type v} (g : σScheme) [Small.{u, v} σ] (x : ↥( g)) :
noncomputable def AlgebraicGeometry.sigmaOpenCover {σ : Type v} (g : σScheme) [Small.{u, v} σ] :

The open cover of the coproduct.

Equations
@[simp]
theorem AlgebraicGeometry.sigmaOpenCover_obj {σ : Type v} (g : σScheme) [Small.{u, v} σ] (a✝ : σ) :
(sigmaOpenCover g).obj a✝ = g a✝
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.
@[simp]
theorem AlgebraicGeometry.sigmaMk_mk {ι : Type u} (f : ιScheme) (i : ι) (x : (f i)) :
theorem AlgebraicGeometry.isOpenImmersion_sigmaDesc {σ : Type v} (g : σScheme) [Small.{u, v} σ] {X : Scheme} (α : (i : σ) → g i X) [∀ (i : σ), IsOpenImmersion (α i)] ( : Pairwise (Function.onFun Disjoint fun (x : σ) => Set.range (CategoryTheory.ConcreteCategory.hom (α x).base))) :
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))) :

S is the disjoint union of Xᵢ if the Xᵢ are covering, pairwise disjoint open subschemes of S.

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

The open cover of the coproduct of two schemes.

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

If X and Y are open disjoint and covering open subschemes of S, S is the disjoint union of X and Y.

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.
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
@[simp]
theorem AlgebraicGeometry.ι_sigmaSpec {ι : Type u} (R : ιCommRingCat) (i : ι) :
instance AlgebraicGeometry.instIsOpenImmersionMapOfHomForallEvalRingHom {ι : Type u} (i : ι) (R : ιType (max u_1 u)) [(i : ι) → CommRing (R i)] :
instance AlgebraicGeometry.instIsAffineSigmaObjSchemeOfFinite {ι : Type u} (f : ιScheme) [Finite ι] [∀ (i : ι), IsAffine (f i)] :