inr_ — Mathlib

English

The functor inr_ : D ⥤ C ⊕ D sends each object of D to its image in the right component of the sum and acts on morphisms by lifting via ULift.

Русский

Функтор inr_ : D ⥤ C ⊕ D переводит каждый объект D в правый компонент суммы и действует на морфизмах через ULift.

LaTeX

$$$$ \mathrm{inr}_{C}(D) : D \to C \oplus D, \quad \mathrm{obj}(X) = \mathrm{inr}(X), \quad \mathrm{map}(f) = \mathrm{ULift.up}(f). $$$$

Lean4

/-- `inr_` is the functor `X ↦ inr X`. -/
@[simps! obj]
def inr_ : D ⥤ C ⊕ D where
  obj X := inr X
  map f := ULift.up f

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