sectL — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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