pullbackObjIso_inv_comp_snd — Mathlib

English

In a HasPullbacks setting, with F,G,H: D ⥤ C and arrows f, g to H, for any d ∈ D, the inverse-then-snd composition equals the componentwise snd on d, showing compatibility of the isomorphism with the second projection.

Русский

В условиях HasPullbacks для F,G,H: D ⥤ C и стрелок f, g к H, для любого d ∈ D композиция inv затем snd равна snd на компоненте d, демонстрируя совместимость изоморфизма с второй проекцией.

LaTeX

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

Lean4

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

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