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 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 (Opposite.op X))) (x : X.toTopCat) :
    r(X.toΓSpecFun x).asIdeal IsUnit ((X.presheaf.Γgerm x) r)

    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

                      The canonical map X ⟶ Spec Γ(X, ⊤). This is the unit of the Γ-Spec adjunction.

                      Equations
                      Instances For
                        @[deprecated AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen]

                        Alias of AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen.

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