toCostructuredArrow_comp_proj — Mathlib

English

Equality of projections: the structured arrow to CostructuredArrow composes to recover G.

Русский

Равенство проекций: структурированная стрелка в CostructuredArrow после композиции дает G.

LaTeX

$$$ (G.toCostructuredArrow F X f h) \;\; \; \; \; \; = G$$$

Lean4

@[simp]
theorem toCostructuredArrow_comp_proj (G : E ⥤ C) (F : C ⥤ D) (X : D) (f : (Y : E) → F.obj (G.obj Y) ⟶ X)
    (h : ∀ {Y Z : E} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y) :
    G.toCostructuredArrow F X f h ⋙ CostructuredArrow.proj _ _ = G :=
  rfl

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