Documentation

Mathlib.AlgebraicGeometry.Limits

(Co)Limits of Schemes #

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

Todo #

source
noncomputable def AlgebraicGeometry.specZIsTerminal :
CategoryTheory.Limits.IsTerminal (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (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.
Instances For
    source
    noncomputable instance AlgebraicGeometry.instHasTerminalScheme :
    CategoryTheory.Limits.HasTerminal AlgebraicGeometry.Scheme
    Equations
    source
    noncomputable instance AlgebraicGeometry.instIsAffineTerminalScheme :
    AlgebraicGeometry.IsAffine (⊤_ AlgebraicGeometry.Scheme)
    Equations
    source
    noncomputable instance AlgebraicGeometry.instHasFiniteLimitsScheme :
    CategoryTheory.Limits.HasFiniteLimits AlgebraicGeometry.Scheme
    Equations
    source
    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.
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.emptyTo_val_base_apply (X : AlgebraicGeometry.Scheme) (x : ↑↑∅.toPresheafedSpace) :
      X.emptyTo.val.base x = PEmpty.elim x
      source
      @[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)
      source
      theorem AlgebraicGeometry.Scheme.empty_ext {X : AlgebraicGeometry.Scheme} (f : ∅ ⟶ X) (g : ∅ ⟶ X) :
      f = g
      source
      theorem AlgebraicGeometry.Scheme.eq_emptyTo {X : AlgebraicGeometry.Scheme} (f : ∅ ⟶ X) :
      f = X.emptyTo
      source
      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 := ⋯ }
      source
      noncomputable def AlgebraicGeometry.emptyIsInitial :
      CategoryTheory.Limits.IsInitial ∅

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

      Equations
      Instances For
        source
        @[simp]
        theorem AlgebraicGeometry.emptyIsInitial_to :
        AlgebraicGeometry.emptyIsInitial.to = AlgebraicGeometry.Scheme.emptyTo
        source
        noncomputable instance AlgebraicGeometry.instIsEmptyαTopologicalSpaceCarrierCommRingCatEmpty :
        IsEmpty ↑↑AlgebraicGeometry.Scheme.empty.toPresheafedSpace
        Equations
        source
        noncomputable instance AlgebraicGeometry.spec_punit_isEmpty :
        IsEmpty ↑↑(AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of PUnit.{u_1 + 1} ))).toPresheafedSpace
        Equations
        source
        noncomputable instance AlgebraicGeometry.isOpenImmersion_of_isEmpty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsEmpty ↑↑X.toPresheafedSpace] :
        AlgebraicGeometry.IsOpenImmersion f
        Equations
        • ⋯ = ⋯
        source
        noncomputable instance AlgebraicGeometry.isIso_of_isEmpty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsEmpty ↑↑Y.toPresheafedSpace] :
        CategoryTheory.IsIso f
        Equations
        • ⋯ = ⋯
        source
        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
        Instances For
          source
          noncomputable def AlgebraicGeometry.specPunitIsInitial :
          CategoryTheory.Limits.IsInitial (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of PUnit.{u_1 + 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.
          Instances For
            source
            noncomputable instance AlgebraicGeometry.isAffine_of_isEmpty {X : AlgebraicGeometry.Scheme} [IsEmpty ↑↑X.toPresheafedSpace] :
            AlgebraicGeometry.IsAffine X
            Equations
            • ⋯ = ⋯
            source
            noncomputable instance AlgebraicGeometry.instHasInitialScheme :
            CategoryTheory.Limits.HasInitial AlgebraicGeometry.Scheme
            Equations
            source
            noncomputable instance AlgebraicGeometry.initial_isEmpty :
            IsEmpty ↑↑(⊥_ AlgebraicGeometry.Scheme).toPresheafedSpace
            Equations
            source
            theorem AlgebraicGeometry.bot_isAffineOpen (X : AlgebraicGeometry.Scheme) :
            AlgebraicGeometry.IsAffineOpen ⊥
            source
            noncomputable instance AlgebraicGeometry.instHasStrictInitialObjectsScheme :
            CategoryTheory.Limits.HasStrictInitialObjects AlgebraicGeometry.Scheme
            Equations