English
The toOpensFunctor for X is locally full with respect to the Grothendieck topology on Opens carrier, meaning every morphism between images locally lifts to a morphism in AffineZariskiSite.
Русский
Функтор toOpensFunctor для X локально полный относительно топологии Гротендикса на Opens-carrier: каждый морфизм между образами локально поднимается до морфизма в AffineZariskiSite.
LaTeX
$$$(toOpensFunctor X).IsLocallyFull\big(Opens.grothendieckTopology X.carrier.carrier\big)$$$
Lean4
instance : (toOpensFunctor X).IsLocallyFull (Opens.grothendieckTopology X) where
functorPushforward_imageSieve_mem := by
intro U V h x hx
obtain ⟨f, hfU, hxf⟩ := V.2.exists_basicOpen_le ⟨x, hx⟩ (h.le hx)
exact
⟨X.basicOpen f, homOfLE hfU,
⟨V.basicOpen f, ⟨_, (X.basicOpen_res f h.op).trans (inf_eq_right.mpr hfU)⟩, 𝟙 _, ⟨⟨f, rfl⟩, rfl⟩, rfl⟩, hxf⟩
