Theorems · Definition · algebraic geometry

AlgebraicGeometry.Proj.map

{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 ℬ ⟶ AlgebraicGeometry.Proj 𝒜)

Functoriality of Proj.

Defined in

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRingSetLikeAddSubgroupClassCommRingSetLikeAddSubgroupClassGradedRingGradedRing