Documentation

Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Adjunction between Γ and Spec #

We define the adjunction ΓSpec.adjunction : Γ ⊣ Spec by defining the unit (toΓSpec, in multiple steps in this file) and counit (done in Spec.lean) and checking that they satisfy the left and right triangle identities. The constructions and proofs make use of maps and lemmas defined and proved in structure_sheaf.lean extensively.

Notice that since the adjunction is between contravariant functors, you get to choose one of the two categories to have arrows reversed, and it is equally valid to present the adjunction as Spec ⊣ Γ (Spec.to_LocallyRingedSpace.right_op ⊣ Γ), in which case the unit and the counit would switch to each other.

Main definition #

The map from the global sections to a stalk.

Equations
  • X.ΓToStalk x = X.presheaf.germ x, trivial
Instances For

    The canonical map from the underlying set to the prime spectrum of Γ(X).

    Equations
    Instances For
      theorem AlgebraicGeometry.LocallyRingedSpace.not_mem_prime_iff_unit_in_stalk (X : AlgebraicGeometry.LocallyRingedSpace) (r : (AlgebraicGeometry.LocallyRingedSpace.Γ.obj { unop := X })) (x : X.toTopCat) :
      r(X.toΓSpecFun x).asIdeal IsUnit ((X.ΓToStalk x) r)
      theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preim_basicOpen_eq (X : AlgebraicGeometry.LocallyRingedSpace) (r : (AlgebraicGeometry.LocallyRingedSpace.Γ.obj { unop := X })) :
      X.toΓSpecFun ⁻¹' (PrimeSpectrum.basicOpen r).carrier = (X.toRingedSpace.basicOpen r).carrier

      The preimage of a basic open in Spec Γ(X) under the unit is the basic open in X defined by the same element (they are equal as sets).

      @[simp]
      theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecBase_apply (X : AlgebraicGeometry.LocallyRingedSpace) :
      ∀ (a : X.toTopCat), X.toΓSpecBase a = X.toΓSpecFun a

      The canonical (bundled) continuous map from the underlying topological space of X to the prime spectrum of its global sections.

      Equations
      • X.toΓSpecBase = { toFun := X.toΓSpecFun, continuous_toFun := }
      Instances For
        @[reducible, inline]

        The preimage in X of a basic open in Spec Γ(X) (as an open set).

        Equations
        Instances For
          theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq (X : AlgebraicGeometry.LocallyRingedSpace) (r : (AlgebraicGeometry.LocallyRingedSpace.Γ.obj { unop := X })) :
          X.toΓSpecMapBasicOpen r = X.toRingedSpace.basicOpen r

          The preimage is the basic open in X defined by the same element r.

          @[reducible, inline]
          abbrev AlgebraicGeometry.LocallyRingedSpace.toToΓSpecMapBasicOpen (X : AlgebraicGeometry.LocallyRingedSpace) (r : (AlgebraicGeometry.LocallyRingedSpace.Γ.obj { unop := X })) :
          X.presheaf.obj { unop := } X.presheaf.obj { unop := X.toΓSpecMapBasicOpen r }

          The map from the global sections Γ(X) to the sections on the (preimage of) a basic open.

          Equations
          • X.toToΓSpecMapBasicOpen r = X.presheaf.map (X.toΓSpecMapBasicOpen r).leTop.op
          Instances For

            r is a unit as a section on the basic open defined by r.

            Define the sheaf hom on individual basic opens for the unit.

            Equations
            Instances For

              Characterization of the sheaf hom on basic opens, direction ← (next lemma) is used at various places, but → is not used in this file.

              The sheaf hom on all basic opens, commuting with restrictions.

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

                The canonical morphism of sheafed spaces from X to the spectrum of its global sections.

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

                  The map on stalks induced by the unit commutes with maps from Γ(X) to stalks (in Spec Γ(X) and in X).

                  The canonical morphism from X to the spectrum of its global sections.

                  Equations
                  • X.toΓSpec = { val := X.toΓSpecSheafedSpace, prop := }
                  Instances For

                    The adjunction Γ ⊣ Spec from CommRingᵒᵖ to LocallyRingedSpace.

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

                      The adjunction Γ ⊣ Spec from CommRingᵒᵖ to Scheme.

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

                        Immediate consequences of the adjunction.