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.
Instances For

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      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.
      Instances For
        @[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✝)
        @[simp]
        theorem AlgebraicGeometry.Scheme.emptyTo_base_apply (X : Scheme) (x : .toPresheafedSpace) :
        X.emptyTo.base x = PEmpty.elim x
        theorem AlgebraicGeometry.Scheme.eq_emptyTo {X : Scheme} (f : X) :
        f = X.emptyTo
        Equations
        • X.hom_unique_of_empty_source = { default := X.emptyTo, uniq := }

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

        Equations
        Instances For
          @[instance 100]
          instance AlgebraicGeometry.isOpenImmersion_of_isEmpty {X Y : Scheme} (f : X Y) [IsEmpty X.toPresheafedSpace] :
          @[instance 100]
          instance AlgebraicGeometry.isIso_of_isEmpty {X Y : Scheme} (f : X Y) [IsEmpty Y.toPresheafedSpace] :
          noncomputable def AlgebraicGeometry.isInitialOfIsEmpty {X : Scheme} [IsEmpty X.toPresheafedSpace] :

          A scheme is initial if its underlying space is empty .

          Equations
          Instances For

            Spec 0 is the initial object in the category of schemes.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[instance 100]
              instance AlgebraicGeometry.isAffine_of_isEmpty {X : Scheme} [IsEmpty X.toPresheafedSpace] :
              instance AlgebraicGeometry.initial_isEmpty :
              IsEmpty (⊥_ Scheme).toPresheafedSpace

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[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'_t {ι : Type u} (f : ιScheme) (x✝ x✝¹ : ι) (x✝² : x✝ x✝¹) :
                (disjointGlueData' f).t x✝ x✝¹ x✝² = CategoryTheory.CategoryStruct.id ((fun (x x_1 : ι) (x : x x_1) => ) x✝ x✝¹ x✝²)
                @[simp]
                theorem AlgebraicGeometry.disjointGlueData'_J {ι : Type u} (f : ιScheme) :
                @[simp]
                theorem AlgebraicGeometry.disjointGlueData'_U {ι : Type u} (f : ιScheme) (a✝ : ι) :
                (disjointGlueData' f).U a✝ = f a✝
                @[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 ((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'_V {ι : Type u} (f : ιScheme) (x✝ x✝¹ : ι) (x✝² : x✝ x✝¹) :
                (disjointGlueData' f).V x✝ x✝¹ x✝² =
                noncomputable def AlgebraicGeometry.disjointGlueData {ι : Type u} (f : ιScheme) :

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

                Equations
                Instances For
                  @[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) :
                  @[simp]
                  theorem AlgebraicGeometry.disjointGlueData_f {ι : Type u} (f : ιScheme) (i j : (disjointGlueData' f).J) :
                  (disjointGlueData f).f i j = (disjointGlueData' f).f' i j

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

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

                    (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.
                    Instances For
                      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.
                      Instances For
                        theorem AlgebraicGeometry.sigmaι_eq_iff {ι : Type u} (f : ι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

                        The images of each component in the coproduct is disjoint.

                        theorem AlgebraicGeometry.exists_sigmaι_eq {ι : Type u} (f : ιScheme) (x : ( f).toPresheafedSpace) :
                        ∃ (i : ι) (y : (f i).toPresheafedSpace), (CategoryTheory.Limits.Sigma.ι f i).base y = x
                        noncomputable def AlgebraicGeometry.sigmaOpenCover {ι : Type u} (f : ιScheme) :
                        ( f).OpenCover

                        The open cover of the coproduct.

                        Equations
                        Instances For
                          @[simp]
                          @[simp]
                          theorem AlgebraicGeometry.sigmaOpenCover_obj {ι : Type u} (f : ιScheme) (a✝ : ι) :
                          (sigmaOpenCover f).obj a✝ = f a✝
                          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.
                          Instances For
                            @[simp]
                            theorem AlgebraicGeometry.sigmaMk_mk {ι : Type u} (f : ιScheme) (i : ι) (x : (f i).toPresheafedSpace) :
                            (sigmaMk f) i, x = (CategoryTheory.Limits.Sigma.ι f i).base x

                            (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.
                            Instances For
                              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.
                              Instances For
                                @[simp]
                                theorem AlgebraicGeometry.coprodMk_inl (X Y : Scheme) (x : X.toPresheafedSpace) :
                                @[simp]
                                theorem AlgebraicGeometry.coprodMk_inr (X Y : Scheme) (x : Y.toPresheafedSpace) :
                                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.
                                Instances For

                                  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.
                                  Instances For
                                    theorem AlgebraicGeometry.coprodSpec_coprodMk (R S : Type u) [CommRing R] [CommRing S] (x : (Spec (CommRingCat.of R)).toPresheafedSpace (Spec (CommRingCat.of S)).toPresheafedSpace) :
                                    theorem AlgebraicGeometry.coprodSpec_apply (R S : Type u) [CommRing R] [CommRing S] (x : (Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace) :
                                    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
                                    Instances For
                                      @[simp]
                                      theorem AlgebraicGeometry.ι_sigmaSpec {ι : Type u} (R : ιCommRingCat) (i : ι) :
                                      instance AlgebraicGeometry.instIsAffineSigmaObjSchemeOfFinite {ι : Type u} (f : ιScheme) [Finite ι] [∀ (i : ι), IsAffine (f i)] :