comap_basicOpen — Mathlib

English

The map toOpen composed with comap f equals the map obtained by first applying comap to S and then toOpen on the target open.

Русский

Картирование toOpen составленное с comap f равно отображению, полученному сначала применив comap к S, затем toOpen на целевом открытом.

LaTeX

$$$(toOpen R U) \\circ (comap f U (Opens.comap(PrimeSpectrum.comap f) U)) = (ofHom f) \\circ toOpen S$$$

Lean4

theorem comap_basicOpen (f : R →+* S) (x : R) :
    comap f (PrimeSpectrum.basicOpen x) (PrimeSpectrum.basicOpen (f x)) (PrimeSpectrum.comap_basicOpen f x).le =
      IsLocalization.map (M := .powers x) (T := .powers (f x)) _ f (Submonoid.powers_le.mpr (Submonoid.mem_powers _)) :=
  IsLocalization.ringHom_ext (.powers x) <| by simpa [CommRingCat.hom_ext_iff] using toOpen_comp_comap f _

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