English
The preimage of a basicOpen under a morphism of Locally Ringed Spaces coincides with the basicOpen of the pushed-forward section on the domain.
Русский
Обратное образ базового открытого множества по гомоморфизму локально кольцевых пространств совпадает с базовым открытым множеством над образуемой секцией на области определения.
LaTeX
$$$$ (Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) = @RingedSpace.basicOpen X.toRingedSpace (f.c.app _ s). $$$$
Lean4
theorem preimage_basicOpen {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) {U : Opens Y} (s : Y.presheaf.obj (op U)) :
(Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
@RingedSpace.basicOpen X.toRingedSpace ((Opens.map f.base).obj U) (f.c.app _ s) :=
by
ext x
constructor
· rintro ⟨hxU, hx⟩
rw [SetLike.mem_coe, X.toRingedSpace.mem_basicOpen _ _ hxU]
delta toRingedSpace
rw [← stalkMap_germ_apply]
exact (f.stalkMap _).hom.isUnit_map hx
· rintro ⟨hxU, hx⟩
simp only [Opens.map_coe, Set.mem_preimage, SetLike.mem_coe, toRingedSpace] at hx ⊢
rw [RingedSpace.mem_basicOpen _ s (f.base x) hxU]
rw [← stalkMap_germ_apply] at hx
exact (isUnit_map_iff (f.toShHom.stalkMap _).hom _).mp hx
