English
The inverse of awayι composed with fst yields the localization map to the first projection.
Русский
Обратное awayι после fst даёт локализационную карту к первой проекции.
LaTeX
$$$(awayι 𝒜 f deg).inv \\circ \\mathrm{Limits.pullback.fst} = \\mathrm{Spec.map}(...)$$$
Lean4
theorem awayι_preimage_basicOpen :
awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g = PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg) :=
by
ext1
trans Set.range (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg rfl))).base
· rw [← pullbackAwayιIso_inv_fst 𝒜 f_deg hm g_deg hm' rfl]
simp only [TopologicalSpace.Opens.map_coe, Scheme.comp_coeBase, TopCat.hom_comp, ContinuousMap.coe_comp,
Set.range_comp]
rw [Set.range_eq_univ.mpr (by exact (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' rfl).inv.homeomorph.surjective), ←
opensRange_awayι _ _ g_deg hm']
simp [IsOpenImmersion.range_pullback_fst_of_right]
· letI := (awayMap (f := f) 𝒜 g_deg rfl).toAlgebra
letI := HomogeneousLocalization.Away.isLocalization_mul f_deg g_deg rfl hm.ne'
exact PrimeSpectrum.localization_away_comap_range _ _
