Documentation

Mathlib.AlgebraicGeometry.AffineScheme

Affine schemes #

We define the category of AffineSchemes as the essential image of Spec. We also define predicates about affine schemes and affine open sets.

Main definitions #

The category of affine schemes

Instances For

    A Scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.

    Instances

      Construct an affine scheme from a scheme and the information that it is affine. Also see AffineScheme.of for a typeclass version.

      Instances For

        Construct an affine scheme from a scheme. Also see AffineScheme.mk for a non-typeclass version.

        Instances For

          The category of affine schemes is equivalent to the category of commutative rings.

          Instances For

            An open subset of a scheme is affine if the open subscheme is affine.

            Instances For

              The set of affine opens as a subset of opens X.

              Instances For

                The open immersion Spec 𝒪ₓ(U) ⟶ X for an affine U.

                Instances For
                  theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (h : U = V) (W : (TopologicalSpace.Opens (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op V)))).toPresheafedSpace)ᵒᵖ) :
                  (AlgebraicGeometry.Scheme.Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op).op).val.c.app W = CategoryTheory.eqToHom (_ : (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op V)))).presheaf.obj W = ((AlgebraicGeometry.Scheme.Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op).op).val.base _* (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).presheaf).obj W)
                  instance AlgebraicGeometry.algebra_section_section_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) :
                  Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen X f)))

                  The canonical map Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(Spec_Γ_identity.inv f)) This is an isomorphism, as witnessed by an is_iso instance.

                  Instances For
                    theorem AlgebraicGeometry.isLocalization_of_eq_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (i : V U) (hU : AlgebraicGeometry.IsAffineOpen U) (r : ↑(X.presheaf.obj (Opposite.op U))) (e : V = AlgebraicGeometry.Scheme.basicOpen X r) :
                    IsLocalization.Away r ↑(X.presheaf.obj (Opposite.op V))
                    noncomputable def AlgebraicGeometry.IsAffineOpen.primeIdealOf {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : { x // x U }) :
                    PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))

                    The prime ideal of 𝒪ₓ(U) corresponding to a point x : U.

                    Instances For
                      theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens X.toPresheafedSpace) [AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U)))] :

                      The basic open set of a section f on an affine open as an X.affineOpens.

                      Instances For
                        theorem AlgebraicGeometry.of_affine_open_cover {X : AlgebraicGeometry.Scheme} (V : ↑(AlgebraicGeometry.Scheme.affineOpens X)) (S : Set ↑(AlgebraicGeometry.Scheme.affineOpens X)) {P : ↑(AlgebraicGeometry.Scheme.affineOpens X)Prop} (hP₁ : (U : ↑(AlgebraicGeometry.Scheme.affineOpens X)) → (f : ↑(X.presheaf.obj (Opposite.op U))) → P UP (AlgebraicGeometry.Scheme.affineBasicOpen X f)) (hP₂ : (U : ↑(AlgebraicGeometry.Scheme.affineOpens X)) → (s : Finset ↑(X.presheaf.obj (Opposite.op U))) → Ideal.span s = ((f : { x // x s }) → P (AlgebraicGeometry.Scheme.affineBasicOpen X f)) → P U) (hS : ⋃ (i : S), i = Set.univ) (hS' : (U : S) → P U) :
                        P V

                        Let P be a predicate on the affine open sets of X satisfying

                        1. If P holds on U, then P holds on the basic open set of every section on U.
                        2. If P holds for a family of basic open sets covering U, then P holds for U.
                        3. There exists an affine open cover of X each satisfying P.

                        Then P holds for every affine open of X.

                        This is also known as the Affine communication lemma in [The rising sea][RisingSea].