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
    theorem AlgebraicGeometry.LocallyRingedSpace.ΓToStalk_stalkMap_apply {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X Y) (x : X.toTopCat) (a : (Y.presheaf.obj (Opposite.op ))) :
    (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x) ((Y.ΓToStalk (f.val.base x)) a) = (X.ΓToStalk x) ((f.val.c.app (Opposite.op )) a)

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

    Equations
    Instances For

      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

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

          @[reducible, inline]

          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
                    theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq {X : AlgebraicGeometry.LocallyRingedSpace} (s : Set (X.presheaf.obj (Opposite.op ))) :
                    X.toΓSpec.val.base ⁻¹' PrimeSpectrum.zeroLocus s = X.toRingedSpace.zeroLocus s

                    On a locally ringed space X, the preimage of the zero locus of the prime spectrum of Γ(X, ⊤) under toΓSpec agrees with the associated zero locus on X.

                    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.

                        The functor Spec.toLocallyRingedSpace : CommRingCatᵒᵖ ⥤ LocallyRingedSpace is fully faithful.

                        Equations
                        Instances For

                          The functor Spec : CommRingCatᵒᵖ ⥤ Scheme is fully faithful.

                          Equations
                          Instances For
                            @[simp]
                            theorem AlgebraicGeometry.Spec.homEquiv_symm_apply {R : CommRingCat} {S : CommRingCat} (f : R S) :
                            AlgebraicGeometry.Spec.homEquiv.symm f = AlgebraicGeometry.Spec.map f

                            Spec is fully faithful

                            Equations
                            • AlgebraicGeometry.Spec.homEquiv = { toFun := AlgebraicGeometry.Spec.preimage, invFun := AlgebraicGeometry.Spec.map, left_inv := , right_inv := }
                            Instances For
                              @[deprecated AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq]

                              Alias of AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq.


                              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).