English
A variant of the basic open/spec away compatibility, establishing the commutation of maps under localization away from a product x = f g.
Русский
Альтернативная версия совместимости базового открытого множества/спекта вдали от произведения x = f g, выражающая совместимость отображений локализации.
LaTeX
$$Eq (AlgebraicGeometry.Scheme.instCategory.comp (AlgebraicGeometry.basicOpenIsoSpecAway x).inv ((AlgebraicGeometry.Spec R).homOfLE ⋯)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ⋯)$$
Lean4
@[reassoc]
theorem basicOpenIsoSpecAway_inv_homOfLE {R : CommRingCat.{u}} (f g x : R) (hx : x = f * g) :
haveI : IsLocalization.Away (f * g) (Localization.Away x) := by rw [hx]; infer_instance
(basicOpenIsoSpecAway x).inv ≫ (Spec R).homOfLE (by simp [hx, PrimeSpectrum.basicOpen_mul]) =
Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv :=
by
subst hx
rw [← cancel_mono (Scheme.Opens.ι _)]
simp only [basicOpenIsoSpecAway, Category.assoc, Scheme.homOfLE_ι, IsOpenImmersion.isoOfRangeEq_inv_fac]
simp only [← Spec.map_comp, ← CommRingCat.ofHom_comp]
congr
ext x
exact (IsLocalization.Away.awayToAwayRight_eq f g x).symm
