sectR — Mathlib

English

Let C and D be categories and Z an object of C. There is a functor R_Z: D → C × D defined by R_Z(Y) = (Z, Y) on objects and R_Z(f) = (id_Z, f) on morphisms.

Русский

Пусть C и D — категории, Z — объект C. Существует функтор R_Z: D → C × D, задаваемый на объектах R_Z(Y) = (Z, Y) и на морфизмах R_Z(f) = (id_Z, f).

LaTeX

$$$R_Z: D \to C \times D$, $R_Z(Y) = (Z,Y)$, $R_Z(f) = (\mathrm{Id}_Z, f)$.$$

Lean4

/-- `sectR Z D` is the functor `D ⥤ C × D` given by `Y ↦ (Z, Y)` . -/
@[simps]
def sectR {C : Type u₁} [Category.{v₁} C] (Z : C) (D : Type u₂) [Category.{v₂} D] : D ⥤ C × D
    where
  obj X := (Z, X)
  map f := (𝟙 Z, f)

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