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

Equations
Instances For

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

    Instances

      The canonical isomorphism X ≅ Spec Γ(X) for an affine scheme.

      Equations
      Instances For

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

        Equations
        Instances For

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

          Equations
          Instances For

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

            Equations
            Instances For

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

              Equations
              Instances For
                Equations
                • =
                Equations
                • =
                instance AlgebraicGeometry.Scheme.affineBasisCoverIsAffine (X : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.J) :
                AlgebraicGeometry.IsAffine (X.affineBasisCover.obj i)
                Equations
                • =
                def AlgebraicGeometry.IsAffineOpen.fromSpec {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) :
                AlgebraicGeometry.Scheme.Spec.obj { unop := X.presheaf.obj { unop := U } } X

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem AlgebraicGeometry.IsAffineOpen.SpecΓIdentity_hom_app_fromSpec {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) :
                  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SpecΓIdentity.hom.app (X.presheaf.obj { unop := U })) (hU.fromSpec.val.c.app { unop := U }) = (AlgebraicGeometry.Scheme.Spec.obj { unop := X.presheaf.obj { unop := U } }).presheaf.map (CategoryTheory.eqToHom ).op
                  theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj { unop := U })) :
                  (hU.fromSpec.val.c.app { unop := U }) x = ((AlgebraicGeometry.Scheme.Spec.obj { unop := X.presheaf.obj { unop := U } }).presheaf.map (CategoryTheory.eqToHom )) ((AlgebraicGeometry.toSpecΓ (X.presheaf.obj { unop := U })) x)
                  theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_self {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) :
                  hU.fromSpec.val.c.app { unop := U } = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SpecΓIdentity.inv.app (X.presheaf.obj { unop := U })) ((AlgebraicGeometry.Scheme.Spec.obj { unop := X.presheaf.obj { unop := U } }).presheaf.map (CategoryTheory.eqToHom ).op)
                  theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen' {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) :
                  hU.fromSpec⁻¹ᵁ X.basicOpen f = (AlgebraicGeometry.Scheme.Spec.obj { unop := X.presheaf.obj { unop := U } }).basicOpen ((AlgebraicGeometry.SpecΓIdentity.inv.app (X.presheaf.obj { unop := U })) f)
                  theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) :
                  hU.fromSpec⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f
                  theorem AlgebraicGeometry.IsAffineOpen.opensFunctor_map_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) :
                  @[simp]
                  theorem AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) :
                  (AlgebraicGeometry.Scheme.Spec.obj { unop := X.presheaf.obj { unop := U } }).basicOpen ((hU.fromSpec.val.c.app { unop := U }) f) = PrimeSpectrum.basicOpen f
                  theorem AlgebraicGeometry.IsAffineOpen.basicOpenIsAffine {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) :
                  theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) {V : TopologicalSpace.Opens X.toPresheafedSpace} (x : V) (h : x U) :
                  ∃ (f : (X.presheaf.obj { unop := U })), X.basicOpen f V x X.basicOpen f
                  def AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) :
                  X.presheaf.obj { unop := X.basicOpen f } (AlgebraicGeometry.Scheme.Spec.obj { unop := X.presheaf.obj { unop := U } }).presheaf.obj { unop := PrimeSpectrum.basicOpen f }

                  Given an affine open U and some f : U, this is the canonical map Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(f)) This is an isomorphism, as witnessed by an IsIso instance.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    instance AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) :
                    CategoryTheory.IsIso (hU.basicOpenSectionsToAffine f)
                    Equations
                    • =
                    theorem AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) :
                    IsLocalization.Away f (X.presheaf.obj { unop := X.basicOpen f })
                    instance AlgebraicGeometry.isLocalization_away_of_isAffine {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (r : (X.presheaf.obj { unop := })) :
                    IsLocalization.Away r (X.presheaf.obj { unop := X.basicOpen r })
                    Equations
                    • =
                    theorem AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) {V : TopologicalSpace.Opens X.toPresheafedSpace} (i : V U) (e : V = X.basicOpen f) :
                    IsLocalization.Away f (X.presheaf.obj { unop := V })
                    Equations
                    • =
                    theorem AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj { unop := U })) (g : (X.presheaf.obj { unop := X.basicOpen f })) :
                    ∃ (f' : (X.presheaf.obj { unop := U })), X.basicOpen f' = X.basicOpen g
                    theorem AlgebraicGeometry.exists_basicOpen_le_affine_inter {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) {V : TopologicalSpace.Opens X.toPresheafedSpace} (hV : AlgebraicGeometry.IsAffineOpen V) (x : X.toPresheafedSpace) (hx : x U V) :
                    ∃ (f : (X.presheaf.obj { unop := U })) (g : (X.presheaf.obj { unop := V })), X.basicOpen f = X.basicOpen g x X.basicOpen f
                    noncomputable def AlgebraicGeometry.IsAffineOpen.primeIdealOf {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : U) :
                    PrimeSpectrum (X.presheaf.obj { unop := U })

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

                    Equations
                    Instances For
                      theorem AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : U) :
                      hU.fromSpec.val.base (hU.primeIdealOf x) = x
                      theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (y : PrimeSpectrum (X.presheaf.obj { unop := U })) (hy : hU.fromSpec.val.base y U) :
                      IsLocalization.AtPrime ((X.presheaf.stalk (hU.fromSpec.val.base y))) y.asIdeal
                      theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : U) :
                      IsLocalization.AtPrime ((X.presheaf.stalk x)) (hU.primeIdealOf x).asIdeal
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.affineBasicOpen_coe (X : AlgebraicGeometry.Scheme) {U : X.affineOpens} (f : (X.presheaf.obj { unop := U })) :
                      (X.affineBasicOpen f) = X.basicOpen f
                      def AlgebraicGeometry.Scheme.affineBasicOpen (X : AlgebraicGeometry.Scheme) {U : X.affineOpens} (f : (X.presheaf.obj { unop := U })) :
                      X.affineOpens

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

                      Equations
                      • X.affineBasicOpen f = X.basicOpen f,
                      Instances For
                        theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (s : Set (X.presheaf.obj { unop := U })) :
                        ⨆ (f : s), X.basicOpen f = U Ideal.span s =
                        theorem AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (s : Set (X.presheaf.obj { unop := U })) :
                        U ⨆ (f : s), X.basicOpen f Ideal.span s =
                        theorem AlgebraicGeometry.of_affine_open_cover {X : AlgebraicGeometry.Scheme} (V : X.affineOpens) (S : Set X.affineOpens) {P : X.affineOpensProp} (hP₁ : ∀ (U : X.affineOpens) (f : (X.presheaf.obj { unop := U })), P UP (X.affineBasicOpen f)) (hP₂ : ∀ (U : X.affineOpens) (s : Finset (X.presheaf.obj { unop := U })), Ideal.span s = (∀ (f : { x : (X.presheaf.obj { unop := U }) // x s }), P (X.affineBasicOpen 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].