English
Let X be a scheme with an affine basis cover. For a point x ∈ X and a refinement parameter r arising from the local affine chart, the base of the affine basis cover maps surjectively onto the base of the affine cover, establishing a compatibility between the two coverings at the level of underlying topological spaces.
Русский
Пусть X — схема с аффинной основой покрытия. Для точки x ∈ X и параметра r, возникающего из локального аффинного диаграммы, клин affineBasisCover.f⟨x,r⟩:base отображает базу-образ соответствующего базисного покрытия так, что образ базовой карты совпадает с базой аффинного покрытия, обеспечивая совместимость двух покрытий на уровне топологического пространства.
LaTeX
$$$\operatorname{Set.range} \bigl(X.\text{affineBasisCover.f }\langle x,r\rangle).\text{base} \;=\; (X.\text{affineCover.f } x).\text{base}'' (\operatorname{PrimeSpectrum.basicOpen} r).1$$$
Lean4
theorem affineBasisCover_map_range (X : Scheme.{u}) (x : X) (r : (X.local_affine x).choose_spec.choose) :
Set.range (X.affineBasisCover.f ⟨x, r⟩).base = (X.affineCover.f x).base '' (PrimeSpectrum.basicOpen r).1 :=
by
simp only [affineBasisCover, Precoverage.ZeroHypercover.bind_toPreZeroHypercover, PreZeroHypercover.bind_f,
comp_coeBase, TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp]
congr
exact (PrimeSpectrum.localization_away_comap_range (Localization.Away r) r :)
