English
The preimage of a basic open under the base map is described by a comap to a basic open in the other space; explicitly, a basic open in the target corresponds to a basic open determined by pbo of t.num.1 in the source.
Русский
Первообразная базовая открытость под отображением базиса задаётся через сопоставление базовых открытых в другой области; явно, базовая открытость на цели соответствует открытости определённой pbo в источнике.
LaTeX
$$$$(\mathrm{Opens.map} (toSpec\;\mathcal{A}f).base).\mathrm{obj}(\mathrm{sbo}(\mathrm{HomogeneousLocalization.mk}\;t)) = \mathrm{Opens.comap}\langle\_,\mathrm{continuous\_subtype\_val}\rangle (\mathrm{pbo}\;t.num.1)$$$$
Lean4
theorem toSpec_preimage_basicOpen {f} (t : NumDenSameDeg 𝒜 (.powers f)) :
(Opens.map (toSpec 𝒜 f).base).obj (sbo (HomogeneousLocalization.mk t)) =
Opens.comap ⟨_, continuous_subtype_val⟩ (pbo t.num.1) :=
Opens.ext <|
Opens.map_coe _ _ ▸ by
convert (ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen f t)
exact funext fun _ => toSpec_base_apply_eq _ _
