prod'CompFst — Mathlib

English

The composition of the product F ×' G with the first projection fst is naturally isomorphic to F: (F ×' G) ⋅ fst ≅ F.

Русский

Композиция произведения F ×' G с проекцией fst естественно изоморфна F: (F ×' G) ⋅ fst ≅ F.

LaTeX

$$$(F \\mathrm{prod}' G) \\circ \\mathrm{fst} \\cong F$$$

Lean4

/-- The product `F.prod' G` followed by projection on the first component is isomorphic to `F` -/
@[simps!]
def prod'CompFst (F : A ⥤ B) (G : A ⥤ C) : F.prod' G ⋙ CategoryTheory.Prod.fst B C ≅ F :=
  NatIso.ofComponents fun _ => Iso.refl _

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