Commit 2024-06-10 11:04 5e33eb3b
View on Github →feat(AlgebraicGeometry/GammaSpecAdjunction): a missing lemma (#13412) Added the following lemma: Let $X$ be a locally ringed space, $R$ a ring and $U \subseteq \mathrm{Spec} R$ an open set. Then for any $f : R \to \Gamma(\mathcal O_X, X)$, if we denote $F$ as the corresponding morphism $X \to \mathrm{Spec} R$ under the gamma spec adjunction we have that the composition $res^{\mathrm{X}}_{F^{-1}U} \circ f$ is equal to the composition $(R \to \mathcal{O}_{\mathrm{Spec} R}(U)\circ F(U)$
lemma toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app
{X : LocallyRingedSpace} {R : Type u} [CommRing R]
(f : LocallyRingedSpace.Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) (U) :
StructureSheaf.toOpen R U.unop ≫
(locallyRingedSpaceAdjunction.homEquiv X (op <| CommRingCat.of R) f).1.c.app U =
f.unop ≫ X.presheaf.map (homOfLE le_top).op := by
found usefuly by Andrew during #12371