pullbackAwayιIso_inv_snd — Mathlib

English

Continuation of the equality of open covers under the construction using the irrelevant ideal and its image under f.

Русский

Продолжение равенства открытых покрытий при отражении нерелевантного идеала и его образе под f.

LaTeX

$$$\\text{openCoverOfMapIrrelevantEqTop 𝒜 f hf} = X.OpenCover$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackAwayιIso_inv_snd :
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv ≫ Limits.pullback.snd _ _ =
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg (hx.trans (mul_comm _ _)))) :=
  by rw [← pullbackAwayιIso_hom_SpecMap_awayMap_right (hx := hx) .., Iso.inv_hom_id_assoc]

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