English
The sheaf hom on all basic opens is compatible with restriction maps and forms a natural transformation.
Русский
Гомохраняемая оболочка на всех базовых открытых множеств совместима с ограничениями и образует естественное преобразование.
LaTeX
$$$toΓSpecCBasicOpens : (inducedFunctor basicOpen).op \Rightarrow (structureSheaf \circ Γ).$$$
Lean4
/-- Characterization of the sheaf hom on basic opens,
direction ← (next lemma) is used at various places, but → is not used in this file. -/
theorem toΓSpecCApp_iff
(f :
(structureSheaf <| Γ.obj <| op X).val.obj (op <| basicOpen r) ⟶ X.presheaf.obj (op <| X.toΓSpecMapBasicOpen r)) :
toOpen _ (basicOpen r) ≫ f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r :=
by
have loc_inst := IsLocalization.to_basicOpen (Γ.obj (op X)) r
refine ConcreteCategory.ext_iff.trans ?_
rw [← @IsLocalization.Away.lift_comp _ _ _ _ _ _ _ r loc_inst _ (X.isUnit_res_toΓSpecMapBasicOpen r)]
constructor
· intro h
ext : 1
exact IsLocalization.ringHom_ext (Submonoid.powers r) h
apply congr_arg
