Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe

∀ {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 : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (U : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Proj.toSheafedSpace 𝒜).toPresheafedSpace)ᵒᵖ)
  (s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op (Opposite.unop U))))
  (y :
    ↥(Opposite.unop
        (Opposite.op
          ((TopologicalSpace.Opens.map (TopCat.ofHom (AlgebraicGeometry.ProjectiveSpectrum.comap f hf))).obj
            (Opposite.unop U))))),
  ↑((CommRingCat.Hom.hom ((AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom.c.app U)) s) y =
    AlgebraicGeometry.Proj.comapStructureSheafFun f hf (Opposite.unop U)
      ((TopologicalSpace.Opens.map (TopCat.ofHom (AlgebraicGeometry.ProjectiveSpectrum.comap f hf))).obj
        (Opposite.unop U))
      ⋯ (↑s) y

Defined in

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingSetLikeAddSubgroupClassCommRingSetLikeAddSubgroupClassGradedRingGradedRing