pullbackAwayιIso_hom_SpecMap_awayMap_left

English

Similarly, the right-hand composition equals the second projection of the pullback.

Русский

Аналогично, правая композиция равна второй проекции pullback.

LaTeX

$$$\\left(\\mathrm{pullbackAwayιIso} \\ 𝒜\\ f\\ hm\\ g\\ hm' hx\\right).hom \\circ \\mathrm{Spec.map}(\\mathrm{awayMap} 𝒜 f_deg (hx.trans (mul\\_comm _ _))) = \\mathrm{Limits.pullback.snd} _ _$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackAwayιIso_hom_SpecMap_awayMap_left :
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) =
      Limits.pullback.fst _ _ :=
  by rw [← cancel_mono (awayι 𝒜 f f_deg hm), ← pullbackAwayιIso_hom_awayι, Category.assoc, SpecMap_awayMap_awayι]

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