Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen

∀ {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 𝒜))
  {p : ProjectiveSpectrum ℬ}
  (c :
    HomogeneousLocalization.NumDenSameDeg 𝒜
      ((AlgebraicGeometry.ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl),
  (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.Proj.toSheafedSpace ℬ).presheaf.germ
          ((TopologicalSpace.Opens.map (AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom.base).obj
            (Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den))))
          p ⋯))
      ((CategoryTheory.ConcreteCategory.hom
          ((AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom.c.app
            (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den))))
        (AlgebraicGeometry.sectionInBasicOpen 𝒜 ((AlgebraicGeometry.ProjectiveSpectrum.comap f hf) p) c)) =
    (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.Proj.toSheafedSpace ℬ).presheaf.germ (ProjectiveSpectrum.basicOpen ℬ (f ↑c.den)) p ⋯))
      (AlgebraicGeometry.sectionInBasicOpen ℬ p (HomogeneousLocalization.NumDenSameDeg.map f ⋯ c))

Defined in

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingSetLikeAddSubgroupClassCommRingSetLikeAddSubgroupClassGradedRingGradedRing