English
Compatibility of the StructureSheaf's open restriction with the Γ-Spec unit: the open restriction composed with the unit equals the presheaf map on the opens.
Русский
Совместимость ограничений структуры sheaf на открытом множестве с единицей Γ-Spec: открытое ограничение компонуется с единицей и равно отображению presheaf на открытые множества.
LaTeX
$$$\text{toOpen}_R U.unop ≫ X.toSpecΓ.app U = X.presheaf.map (homOfLE (by exact le_top)).op$$$
Lean4
@[reassoc (attr := simp)]
theorem toOpen_toSpecΓ_app {X : Scheme.{u}} (U) :
StructureSheaf.toOpen _ _ ≫ X.toSpecΓ.app U = X.presheaf.map (homOfLE (by exact le_top)).op :=
by
rw [← StructureSheaf.toOpen_res _ _ _ (homOfLE le_top), Category.assoc,
NatTrans.naturality _ (homOfLE (le_top (a := U))).op]
change
(ΓSpec.adjunction.counit.app (Scheme.Γ.rightOp.obj X)).unop ≫
(Scheme.Γ.rightOp.map (ΓSpec.adjunction.unit.app X)).unop ≫ _ =
_
rw [← Category.assoc, ← unop_comp, ΓSpec.adjunction.left_triangle_components]
dsimp
exact Category.id_comp _
