map_singleton — Mathlib

English

Mapping a singleton morphism via F yields the singleton of the mapped morphism; i.e., (singleton f).map F = singleton (F.map f).

Русский

Образ одинокого морфизма f через F равен единичной предсистеме на F.map f.

LaTeX

$$$ (\\mathrm{singleton} f).\\mathrm{map} F = \\mathrm{singleton} (F.map f) $$$

Lean4

@[simp]
theorem map_singleton {X Y : C} (f : X ⟶ Y) : (singleton f).map F = singleton (F.map f) := by
  rw [← ofArrows_pUnit.{_, _, 0}, map_ofArrows, ofArrows_pUnit]

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