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 #

source
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
source
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
source
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
    source
    theorem ProjectiveSpectrum.isPrime {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (self : ProjectiveSpectrum ๐’œ) :
    self.asHomogeneousIdeal.toIdeal.IsPrime
    source
    theorem ProjectiveSpectrum.not_irrelevant_le {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (self : ProjectiveSpectrum ๐’œ) :
    ยฌHomogeneousIdeal.irrelevant ๐’œ โ‰ค self.asHomogeneousIdeal
    source
    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) :
    Set (ProjectiveSpectrum ๐’œ)

    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.

    Equations
    Instances For
      source
      @[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
      source
      @[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) :
      ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(Ideal.span s) = ProjectiveSpectrum.zeroLocus ๐’œ s
      source
      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 ๐’œ)) :
      HomogeneousIdeal ๐’œ

      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.

      Equations
      Instances For
        source
        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 : A | โˆ€ x โˆˆ t, f โˆˆ x.asHomogeneousIdeal}
        source
        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 โˆˆ t, f โˆˆ x.asHomogeneousIdeal
        source
        @[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
        source
        theorem ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) (I : Ideal A) :
        t โŠ† ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I โ†” I โ‰ค (ProjectiveSpectrum.vanishingIdeal t).toIdeal
        source
        theorem ProjectiveSpectrum.gc_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        GaloisConnection (fun (I : Ideal A) => ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I) fun (t : (Set (ProjectiveSpectrum ๐’œ))แต’แตˆ) => (ProjectiveSpectrum.vanishingIdeal t).toIdeal

        zeroLocus and vanishingIdeal form a galois connection.

        source
        theorem ProjectiveSpectrum.gc_set {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        GaloisConnection (fun (s : Set A) => ProjectiveSpectrum.zeroLocus ๐’œ s) fun (t : (Set (ProjectiveSpectrum ๐’œ))แต’แตˆ) => โ†‘(ProjectiveSpectrum.vanishingIdeal t)

        zeroLocus and vanishingIdeal form a galois connection.

        source
        theorem ProjectiveSpectrum.gc_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        GaloisConnection (fun (I : HomogeneousIdeal ๐’œ) => ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I) fun (t : (Set (ProjectiveSpectrum ๐’œ))แต’แตˆ) => ProjectiveSpectrum.vanishingIdeal t
        source
        theorem ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) (s : Set A) :
        t โŠ† ProjectiveSpectrum.zeroLocus ๐’œ s โ†” s โŠ† โ†‘(ProjectiveSpectrum.vanishingIdeal t)
        source
        theorem ProjectiveSpectrum.subset_vanishingIdeal_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) :
        s โŠ† โ†‘(ProjectiveSpectrum.vanishingIdeal (ProjectiveSpectrum.zeroLocus ๐’œ s))
        source
        theorem ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : Ideal A) :
        I โ‰ค (ProjectiveSpectrum.vanishingIdeal (ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I)).toIdeal
        source
        theorem ProjectiveSpectrum.homogeneousIdeal_le_vanishingIdeal_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : HomogeneousIdeal ๐’œ) :
        I โ‰ค ProjectiveSpectrum.vanishingIdeal (ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I)
        source
        theorem ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) :
        t โŠ† ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(ProjectiveSpectrum.vanishingIdeal t)
        source
        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) :
        ProjectiveSpectrum.zeroLocus ๐’œ t โŠ† ProjectiveSpectrum.zeroLocus ๐’œ s
        source
        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) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘t โŠ† ProjectiveSpectrum.zeroLocus ๐’œ โ†‘s
        source
        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) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘t โŠ† ProjectiveSpectrum.zeroLocus ๐’œ โ†‘s
        source
        theorem ProjectiveSpectrum.vanishingIdeal_anti_mono {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {s : Set (ProjectiveSpectrum ๐’œ)} {t : Set (ProjectiveSpectrum ๐’œ)} (h : s โŠ† t) :
        ProjectiveSpectrum.vanishingIdeal t โ‰ค ProjectiveSpectrum.vanishingIdeal s
        source
        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
        source
        @[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
        source
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_empty {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        ProjectiveSpectrum.zeroLocus ๐’œ โˆ… = Set.univ
        source
        @[simp]
        theorem ProjectiveSpectrum.vanishingIdeal_univ {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        ProjectiveSpectrum.vanishingIdeal โˆ… = โŠค
        source
        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) :
        ProjectiveSpectrum.zeroLocus ๐’œ s = โˆ…
        source
        @[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 ๐’œ] :
        ProjectiveSpectrum.zeroLocus ๐’œ {1} = โˆ…
        source
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_univ {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        ProjectiveSpectrum.zeroLocus ๐’œ Set.univ = โˆ…
        source
        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) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I โŠ” J) = ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I โˆฉ ProjectiveSpectrum.zeroLocus ๐’œ โ†‘J
        source
        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 ๐’œ) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I โŠ” J) = ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I โˆฉ ProjectiveSpectrum.zeroLocus ๐’œ โ†‘J
        source
        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) :
        ProjectiveSpectrum.zeroLocus ๐’œ (s โˆช s') = ProjectiveSpectrum.zeroLocus ๐’œ s โˆฉ ProjectiveSpectrum.zeroLocus ๐’œ s'
        source
        theorem ProjectiveSpectrum.vanishingIdeal_union {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) (t' : Set (ProjectiveSpectrum ๐’œ)) :
        ProjectiveSpectrum.vanishingIdeal (t โˆช t') = ProjectiveSpectrum.vanishingIdeal t โŠ“ ProjectiveSpectrum.vanishingIdeal t'
        source
        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)
        source
        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)
        source
        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)
        source
        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' โˆˆ s, s') = โ‹‚ s' โˆˆ s, ProjectiveSpectrum.zeroLocus ๐’œ s'
        source
        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)
        source
        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) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I โŠ“ J) = ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I โˆช ProjectiveSpectrum.zeroLocus ๐’œ โ†‘J
        source
        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) :
        ProjectiveSpectrum.zeroLocus ๐’œ s โˆช ProjectiveSpectrum.zeroLocus ๐’œ s' = ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(Ideal.span s โŠ“ Ideal.span s')
        source
        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
        source
        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
        source
        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) :
        ProjectiveSpectrum.zeroLocus ๐’œ {f * g} = ProjectiveSpectrum.zeroLocus ๐’œ {f} โˆช ProjectiveSpectrum.zeroLocus ๐’œ {g}
        source
        @[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) :
        ProjectiveSpectrum.zeroLocus ๐’œ {f ^ n} = ProjectiveSpectrum.zeroLocus ๐’œ {f}
        source
        theorem ProjectiveSpectrum.sup_vanishingIdeal_le {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) (t' : Set (ProjectiveSpectrum ๐’œ)) :
        ProjectiveSpectrum.vanishingIdeal t โŠ” ProjectiveSpectrum.vanishingIdeal t' โ‰ค ProjectiveSpectrum.vanishingIdeal (t โˆฉ t')
        source
        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
        source
        instance ProjectiveSpectrum.zariskiTopology {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        TopologicalSpace (ProjectiveSpectrum ๐’œ)

        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.

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

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

        Equations
        Instances For
          source
          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 ๐’œ)) :
          IsOpen U โ†” โˆƒ (s : Set A), Uแถœ = ProjectiveSpectrum.zeroLocus ๐’œ s
          source
          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 : Set A), Z = ProjectiveSpectrum.zeroLocus ๐’œ s
          source
          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) :
          IsClosed (ProjectiveSpectrum.zeroLocus ๐’œ s)
          source
          theorem ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) :
          ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(ProjectiveSpectrum.vanishingIdeal t) = closure t
          source
          theorem ProjectiveSpectrum.vanishingIdeal_closure {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) :
          ProjectiveSpectrum.vanishingIdeal (closure t) = ProjectiveSpectrum.vanishingIdeal t
          source
          def ProjectiveSpectrum.basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (r : A) :
          TopologicalSpace.Opens (ProjectiveSpectrum ๐’œ)

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

          Equations
          Instances For
            source
            @[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
            source
            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
            source
            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} :
            IsOpen โ†‘(ProjectiveSpectrum.basicOpen ๐’œ a)
            source
            @[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) :
            โ†‘(ProjectiveSpectrum.basicOpen ๐’œ r) = (ProjectiveSpectrum.zeroLocus ๐’œ {r})แถœ
            source
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            ProjectiveSpectrum.basicOpen ๐’œ 1 = โŠค
            source
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            ProjectiveSpectrum.basicOpen ๐’œ 0 = โŠฅ
            source
            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) :
            ProjectiveSpectrum.basicOpen ๐’œ (f * g) = ProjectiveSpectrum.basicOpen ๐’œ f โŠ“ ProjectiveSpectrum.basicOpen ๐’œ g
            source
            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) :
            ProjectiveSpectrum.basicOpen ๐’œ (f * g) โ‰ค ProjectiveSpectrum.basicOpen ๐’œ f
            source
            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) :
            ProjectiveSpectrum.basicOpen ๐’œ (f * g) โ‰ค ProjectiveSpectrum.basicOpen ๐’œ g
            source
            @[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) :
            ProjectiveSpectrum.basicOpen ๐’œ (f ^ n) = ProjectiveSpectrum.basicOpen ๐’œ f
            source
            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)
            source
            theorem ProjectiveSpectrum.isTopologicalBasis_basic_opens {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            TopologicalSpace.IsTopologicalBasis (Set.range fun (r : A) => โ†‘(ProjectiveSpectrum.basicOpen ๐’œ r))

            The specialization order #

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

            source
            instance ProjectiveSpectrum.instPartialOrder {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            PartialOrder (ProjectiveSpectrum ๐’œ)
            Equations
            source
            @[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
            source
            @[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
            source
            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 ๐’œ) :
            x โ‰ค y โ†” y โˆˆ closure {x}