Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Proj.map_comp

∀ {A B C σ τ ψ : 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 : CommRing C]
  [inst_7 : SetLike ψ C] [inst_8 : AddSubgroupClass ψ C] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} {𝒞 : ℕ → ψ} [inst_9 : GradedRing 𝒜]
  [inst_10 : GradedRing ℬ] [inst_11 : GradedRing 𝒞] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (hg : HomogeneousIdeal.irrelevant 𝒞 ≤ HomogeneousIdeal.map g (HomogeneousIdeal.irrelevant ℬ)),
  AlgebraicGeometry.Proj.map (g.comp f) ⋯ =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.map g hg) (AlgebraicGeometry.Proj.map f hf)

Defined in

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingSetLikeAddSubgroupClassCommRingSetLikeAddSubgroupClassCommRingSetLikeAddSubgroupClassGradedRingGradedRingGradedRing