Theorems · Definition · algebraic geometry

AlgebraicGeometry.Proj.mapAffineOpenCover

{A B σ τ : Type u} →
  [inst : CommRing A] →
    [inst_1 : SetLike σ A] →
      [inst_2 : AddSubgroupClass σ A] →
        [inst_3 : CommRing B] →
          [inst_4 : SetLike τ B] →
            [inst_5 : AddSubgroupClass τ B] →
              {𝒜 : ℕ → σ} →
                {ℬ : ℕ → τ} →
                  [inst_6 : GradedRing 𝒜] →
                    [inst_7 : GradedRing ℬ] →
                      (f : 𝒜 →+*ᵍ ℬ) →
                        HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜) →
                          (AlgebraicGeometry.Proj ℬ).AffineOpenCover

Given a graded ring hom f : 𝒜 →+*ᵍ ℬ satisfying the hypothesis ℬ₊ ≤ 𝒜₊.map f, we obtain an affine open cover of Proj ℬ consisting of D(f(s)) for s ∈ A positive degree.

Defined in

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingSetLikeAddSubgroupClassCommRingSetLikeAddSubgroupClassGradedRingGradedRing