prod'CompSnd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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