pullbackAwayιIso_hom_awayι — Mathlib

English

For homogeneous 𝒜, and elements f,g with degrees, the left-hand composition of pullbackAwayιIso's hom with Spec.map(awayMap ...) equals the first projection of the pullback.

Русский

Для данных 𝒜, f, g и связанные элементы степень, композиция слева путей pullbackAwayιIso.hom и Spec.map(awayMap ...) равна fst-проекции в pullback.

LaTeX

$$$\\left(\\mathrm{pullbackAwayιIso} \\ 𝒜\\ f\\ hm\\ g\\ gm\\ hx\\right).hom \\circ \\mathrm{Spec.map}(\\mathrm{awayMap}\\ 𝒜\\ g_{deg}\\ hx) \;=\; \\mathrm{Limits.pullback.fst}\\ _\\ _$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackAwayιIso_hom_awayι :
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫
        awayι 𝒜 x (hx ▸ SetLike.mul_mem_graded f_deg g_deg) (hm.trans_le (m.le_add_right m')) =
      Limits.pullback.fst _ _ ≫ awayι 𝒜 f f_deg hm :=
  IsOpenImmersion.isoOfRangeEq_hom_fac ..

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