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

    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_val_c_app (X : AlgebraicGeometry.Scheme) (U : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
      X.emptyTo.val.c.app U = CommRingCat.punitIsTerminal.from (X.presheaf.obj U)
      @[simp]
      theorem AlgebraicGeometry.Scheme.emptyTo_val_base_apply (X : AlgebraicGeometry.Scheme) (x : .toPresheafedSpace) :
      X.emptyTo.val.base x = PEmpty.elim x
      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]
        Equations
        • =
        @[instance 100]
        noncomputable instance AlgebraicGeometry.isIso_of_isEmpty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) [IsEmpty Y.toPresheafedSpace] :
        Equations
        • =

        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]
            noncomputable instance AlgebraicGeometry.isAffine_of_isEmpty {X : AlgebraicGeometry.Scheme} [IsEmpty X.toPresheafedSpace] :
            Equations
            • =

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

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

              Equations
              Instances For

                (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

                    (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 : ιAlgebraicGeometry.Scheme) (i : ι) (j : ι) (x : (f i).toPresheafedSpace) (y : (f j).toPresheafedSpace) :
                      (CategoryTheory.Limits.Sigma.ι f i).val.base x = (CategoryTheory.Limits.Sigma.ι f j).val.base y i, x = j, y
                      theorem AlgebraicGeometry.exists_sigmaι_eq {ι : Type u} (f : ιAlgebraicGeometry.Scheme) (x : ( f).toPresheafedSpace) :
                      ∃ (i : ι) (y : (f i).toPresheafedSpace), (CategoryTheory.Limits.Sigma.ι f i).val.base y = x
                      noncomputable def AlgebraicGeometry.sigmaOpenCover {ι : Type u} (f : ιAlgebraicGeometry.Scheme) :
                      ( f).OpenCover

                      The open cover of the coproduct.

                      Equations
                      Instances For
                        @[simp]
                        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.
                        Instances For
                          @[simp]
                          theorem AlgebraicGeometry.sigmaMk_mk {ι : Type u} (f : ιAlgebraicGeometry.Scheme) (i : ι) (x : (f i).toPresheafedSpace) :

                          (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
                            theorem AlgebraicGeometry.isCompl_range_inl_inr (X : AlgebraicGeometry.Scheme) (Y : AlgebraicGeometry.Scheme) :
                            IsCompl (Set.range CategoryTheory.Limits.coprod.inl.val.base) (Set.range CategoryTheory.Limits.coprod.inr.val.base)
                            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.
                            Instances For
                              @[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.val.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.val.base x

                              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
                                  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
                                  Instances For
                                    Equations
                                    • =