pullbackObjIso_inv_comp_fst — Mathlib

English

Within a category with pullbacks, for functors F,G,H and arrows f: F ⟶ H, g: G ⟶ H, the inverse of the pullback object iso composed with the first projection corresponds to the first projection at the component level d, expressing compatibility of the iso with projections.

Русский

В категории с pullbacks, для функторов F,G,H и стрелок f: F ⟶ H, g: G ⟶ H, обращённый к первому проецированию компонентный изоморфизм pullbackObjIso f g d совпадает с проекцией на первый компонент на уровне компонент d.

LaTeX

$$$ (pullbackObjIso\, f\, g\, d).inv \\;\\circ\\; (pullback.fst\\, f\\, g).app\\, d = pullback.fst\\left( f.{\\rm app}\\, d\\right)\\left( g.{\\rm app}\\, d\\right) $$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackObjIso_inv_comp_fst (f : F ⟶ H) (g : G ⟶ H) (d : D) :
    (pullbackObjIso f g d).inv ≫ (pullback.fst f g).app d = pullback.fst (f.app d) (g.app d) := by simp [pullbackObjIso]

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