English
For X ∈ LocallyRingedSpace, R a commutative ring, f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R), and an open U in the spectrum, the open-structure map composed with the homEquiv component equals the action of f via the presheaf map on X.
Русский
Для X ∈ LocallyRingedSpace, кольца R, гомоморфизма f и открытого множества U структура открытого участка в сочетании с компонентой гомэквививалентности равна применению f через отображение пресшефов на X.
LaTeX
$$$StructureSheaf.toOpen\ R U.unop ≫ (locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R) f).c.app U = f.unop ≫ X.presheaf.map (homOfLE le_top).op$$$
Lean4
theorem toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app {X : LocallyRingedSpace} {R : Type u} [CommRing R]
(f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) (U) :
StructureSheaf.toOpen R U.unop ≫ (locallyRingedSpaceAdjunction.homEquiv X (op <| CommRingCat.of R) f).c.app U =
f.unop ≫ X.presheaf.map (homOfLE le_top).op :=
by
rw [← StructureSheaf.toOpen_res _ _ _ (homOfLE le_top), Category.assoc,
NatTrans.naturality _ (homOfLE (le_top (a := U.unop))).op, show (toOpen R ⊤) = (toOpen R ⊤).op.unop from rfl, ←
locallyRingedSpaceAdjunction_counit_app']
simp_rw [← Γ_map_op]
rw [← Γ.rightOp_map_unop, ← Category.assoc, ← unop_comp, ← Adjunction.homEquiv_counit, Equiv.symm_apply_apply]
rfl
