toOpen_comp_comap — Mathlib

English

Same as above but stated as a ring hom equality for the basic open, expressed in terms of IsLocalization.map.

Русский

Аналогично для открытого базового множества, выражено через IsLocalization.map.

LaTeX

$$$comap_basicOpen f x = IsLocalization.map (M := .powers x) (T := .powers (f x))_ f (Submonoid.powers_le.mpr (Submonoid.mem_powers _))$$$

Lean4

@[elementwise, reassoc]
theorem toOpen_comp_comap (f : R →+* S) (U : Opens (PrimeSpectrum.Top R)) :
    (toOpen R U ≫ CommRingCat.ofHom (comap f U (Opens.comap (PrimeSpectrum.comap f) U) fun _ => id)) =
      CommRingCat.ofHom f ≫ toOpen S _ :=
  CommRingCat.hom_ext <| RingHom.ext fun _ => Subtype.eq <| funext fun _ => Localization.localRingHom_to_map _ _ _ _ _

Похожие утверждения