Theorems · Definition · algebraic geometry

AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan

{σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              {ι : Type u_2} →
                (f : ι → A) →
                  {m : ι → ℕ} →
                    (∀ (i : ι), f i ∈ 𝒜 (m i)) →
                      (∀ (i : ι), 0 < m i) →
                        (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f) →
                          (AlgebraicGeometry.Proj 𝒜).AffineOpenCover

Given a family of homogeneous elements f of positive degree that spans the irrelevant ideal, Spec (A_f)₀ ⟶ Proj A forms an affine open cover of Proj A.

Defined in

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Cited by

0 results in Mathlib

Foundations

Depth 159 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingSetLikeAddSubgroupClassGradedRing