Documentation

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Projective spectrum of a graded ring #

The projective spectrum of a graded commutative ring is the subtype of all homogenous ideals that are prime and do not contain the irrelevant ideal. It is naturally endowed with a topology: the Zariski topology.

Notation #

Main definitions #

theorem ProjectiveSpectrum.ext {R : Type u_1} {A : Type u_2} :
โˆ€ {inst : CommSemiring R} {inst_1 : CommRing A} {inst_2 : Algebra R A} {๐’œ : โ„• โ†’ Submodule R A} {inst_3 : GradedAlgebra ๐’œ} (x y : ProjectiveSpectrum ๐’œ), x.asHomogeneousIdeal = y.asHomogeneousIdeal โ†’ x = y
theorem ProjectiveSpectrum.ext_iff {R : Type u_1} {A : Type u_2} :
โˆ€ {inst : CommSemiring R} {inst_1 : CommRing A} {inst_2 : Algebra R A} {๐’œ : โ„• โ†’ Submodule R A} {inst_3 : GradedAlgebra ๐’œ} (x y : ProjectiveSpectrum ๐’œ), x = y โ†” x.asHomogeneousIdeal = y.asHomogeneousIdeal
structure ProjectiveSpectrum {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
Type u_2

The projective spectrum of a graded commutative ring is the subtype of all homogenous ideals that are prime and do not contain the irrelevant ideal.

Instances For
    def ProjectiveSpectrum.zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) :

    The zero locus of a set s of elements of a commutative ring A is the set of all relevant homogeneous prime ideals of the ring that contain the set s.

    An element f of A can be thought of as a dependent function on the projective spectrum of ๐’œ. At a point x (a homogeneous prime ideal) the function (i.e., element) f takes values in the quotient ring A modulo the prime ideal x. In this manner, zeroLocus s is exactly the subset of ProjectiveSpectrum ๐’œ where all "functions" in s vanish simultaneously.

    Instances For
      @[simp]
      theorem ProjectiveSpectrum.mem_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) (s : Set A) :
      x โˆˆ ProjectiveSpectrum.zeroLocus ๐’œ s โ†” s โŠ† โ†‘x.asHomogeneousIdeal
      @[simp]
      theorem ProjectiveSpectrum.zeroLocus_span {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) :
      def ProjectiveSpectrum.vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) :

      The vanishing ideal of a set t of points of the projective spectrum of a commutative ring R is the intersection of all the relevant homogeneous prime ideals in the set t.

      An element f of A can be thought of as a dependent function on the projective spectrum of ๐’œ. At a point x (a homogeneous prime ideal) the function (i.e., element) f takes values in the quotient ring A modulo the prime ideal x. In this manner, vanishingIdeal t is exactly the ideal of A consisting of all "functions" that vanish on all of t.

      Instances For
        theorem ProjectiveSpectrum.coe_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) :
        โ†‘(ProjectiveSpectrum.vanishingIdeal t) = {f | โˆ€ (x : ProjectiveSpectrum ๐’œ), x โˆˆ t โ†’ f โˆˆ x.asHomogeneousIdeal}
        theorem ProjectiveSpectrum.mem_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) (f : A) :
        f โˆˆ ProjectiveSpectrum.vanishingIdeal t โ†” โˆ€ (x : ProjectiveSpectrum ๐’œ), x โˆˆ t โ†’ f โˆˆ x.asHomogeneousIdeal
        @[simp]
        theorem ProjectiveSpectrum.vanishingIdeal_singleton {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) :
        ProjectiveSpectrum.vanishingIdeal {x} = x.asHomogeneousIdeal
        theorem ProjectiveSpectrum.gc_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

        zeroLocus and vanishingIdeal form a galois connection.

        theorem ProjectiveSpectrum.gc_set {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

        zeroLocus and vanishingIdeal form a galois connection.

        theorem ProjectiveSpectrum.gc_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        theorem ProjectiveSpectrum.zeroLocus_anti_mono {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {s : Set A} {t : Set A} (h : s โŠ† t) :
        theorem ProjectiveSpectrum.zeroLocus_anti_mono_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {s : Ideal A} {t : Ideal A} (h : s โ‰ค t) :
        theorem ProjectiveSpectrum.zeroLocus_anti_mono_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {s : HomogeneousIdeal ๐’œ} {t : HomogeneousIdeal ๐’œ} (h : s โ‰ค t) :
        theorem ProjectiveSpectrum.zeroLocus_bot {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘โŠฅ = Set.univ
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_singleton_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        ProjectiveSpectrum.zeroLocus ๐’œ {0} = Set.univ
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_empty {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        theorem ProjectiveSpectrum.zeroLocus_empty_of_one_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {s : Set A} (h : 1 โˆˆ s) :
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_singleton_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_univ {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        theorem ProjectiveSpectrum.zeroLocus_sup_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : Ideal A) (J : Ideal A) :
        theorem ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : HomogeneousIdeal ๐’œ) (J : HomogeneousIdeal ๐’œ) :
        theorem ProjectiveSpectrum.zeroLocus_union {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) (s' : Set A) :
        theorem ProjectiveSpectrum.zeroLocus_iSup_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {ฮณ : Sort u_3} (I : ฮณ โ†’ Ideal A) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(โจ† (i : ฮณ), I i) = โ‹‚ (i : ฮณ), ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I i)
        theorem ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {ฮณ : Sort u_3} (I : ฮณ โ†’ HomogeneousIdeal ๐’œ) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(โจ† (i : ฮณ), I i) = โ‹‚ (i : ฮณ), ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I i)
        theorem ProjectiveSpectrum.zeroLocus_iUnion {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {ฮณ : Sort u_3} (s : ฮณ โ†’ Set A) :
        ProjectiveSpectrum.zeroLocus ๐’œ (โ‹ƒ (i : ฮณ), s i) = โ‹‚ (i : ฮณ), ProjectiveSpectrum.zeroLocus ๐’œ (s i)
        theorem ProjectiveSpectrum.zeroLocus_bUnion {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set (Set A)) :
        ProjectiveSpectrum.zeroLocus ๐’œ (โ‹ƒ (s' : Set A) (_ : s' โˆˆ s), s') = โ‹‚ (s' : Set A) (_ : s' โˆˆ s), ProjectiveSpectrum.zeroLocus ๐’œ s'
        theorem ProjectiveSpectrum.vanishingIdeal_iUnion {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {ฮณ : Sort u_3} (t : ฮณ โ†’ Set (ProjectiveSpectrum ๐’œ)) :
        ProjectiveSpectrum.vanishingIdeal (โ‹ƒ (i : ฮณ), t i) = โจ… (i : ฮณ), ProjectiveSpectrum.vanishingIdeal (t i)
        theorem ProjectiveSpectrum.zeroLocus_inf {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : Ideal A) (J : Ideal A) :
        theorem ProjectiveSpectrum.union_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) (s' : Set A) :
        theorem ProjectiveSpectrum.zeroLocus_mul_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : Ideal A) (J : Ideal A) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I * J) = ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I โˆช ProjectiveSpectrum.zeroLocus ๐’œ โ†‘J
        theorem ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : HomogeneousIdeal ๐’œ) (J : HomogeneousIdeal ๐’œ) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I * J) = ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I โˆช ProjectiveSpectrum.zeroLocus ๐’œ โ†‘J
        theorem ProjectiveSpectrum.zeroLocus_singleton_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (g : A) :
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_singleton_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (n : โ„•) (hn : 0 < n) :
        theorem ProjectiveSpectrum.mem_compl_zeroLocus_iff_not_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {f : A} {I : ProjectiveSpectrum ๐’œ} :
        I โˆˆ (ProjectiveSpectrum.zeroLocus ๐’œ {f})แถœ โ†” ยฌf โˆˆ I.asHomogeneousIdeal
        instance ProjectiveSpectrum.zariskiTopology {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

        The Zariski topology on the prime spectrum of a commutative ring is defined via the closed sets of the topology: they are exactly those sets that are the zero locus of a subset of the ring.

        def ProjectiveSpectrum.top {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

        The underlying topology of Proj is the projective spectrum of graded ring A.

        Instances For
          theorem ProjectiveSpectrum.isOpen_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (U : Set (ProjectiveSpectrum ๐’œ)) :
          theorem ProjectiveSpectrum.isClosed_iff_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (Z : Set (ProjectiveSpectrum ๐’œ)) :
          IsClosed Z โ†” โˆƒ s, Z = ProjectiveSpectrum.zeroLocus ๐’œ s
          theorem ProjectiveSpectrum.isClosed_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) :
          def ProjectiveSpectrum.basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (r : A) :

          basicOpen r is the open subset containing all prime ideals not containing r.

          Instances For
            @[simp]
            theorem ProjectiveSpectrum.mem_basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (x : ProjectiveSpectrum ๐’œ) :
            x โˆˆ ProjectiveSpectrum.basicOpen ๐’œ f โ†” ยฌf โˆˆ x.asHomogeneousIdeal
            theorem ProjectiveSpectrum.mem_coe_basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (x : ProjectiveSpectrum ๐’œ) :
            x โˆˆ โ†‘(ProjectiveSpectrum.basicOpen ๐’œ f) โ†” ยฌf โˆˆ x.asHomogeneousIdeal
            theorem ProjectiveSpectrum.isOpen_basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {a : A} :
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (r : A) :
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            theorem ProjectiveSpectrum.basicOpen_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (g : A) :
            theorem ProjectiveSpectrum.basicOpen_mul_le_left {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (g : A) :
            theorem ProjectiveSpectrum.basicOpen_mul_le_right {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (g : A) :
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (n : โ„•) (hn : 0 < n) :
            theorem ProjectiveSpectrum.basicOpen_eq_union_of_projection {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) :
            ProjectiveSpectrum.basicOpen ๐’œ f = โจ† (i : โ„•), ProjectiveSpectrum.basicOpen ๐’œ (โ†‘(GradedAlgebra.proj ๐’œ i) f)

            The specialization order #

            We endow ProjectiveSpectrum ๐’œ with a partial order, where x โ‰ค y if and only if y โˆˆ closure {x}.

            instance ProjectiveSpectrum.instPartialOrderProjectiveSpectrum {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            @[simp]
            theorem ProjectiveSpectrum.as_ideal_le_as_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) (y : ProjectiveSpectrum ๐’œ) :
            x.asHomogeneousIdeal โ‰ค y.asHomogeneousIdeal โ†” x โ‰ค y
            @[simp]
            theorem ProjectiveSpectrum.as_ideal_lt_as_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) (y : ProjectiveSpectrum ๐’œ) :
            x.asHomogeneousIdeal < y.asHomogeneousIdeal โ†” x < y
            theorem ProjectiveSpectrum.le_iff_mem_closure {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) (y : ProjectiveSpectrum ๐’œ) :