map — Mathlib

English

For a functor F: C ⥤ D ⥤ E, map₂Functor promotes F to a functor ThinSkeleton C → ThinSkeleton D ⥤ ThinSkeleton E.

Русский

Для функторa F: C ⥤ D ⥤ E отображение map₂Functor поднимает F до функторa ThinSkeleton C → ThinSkeleton D ⥤ ThinSkeleton E.

LaTeX

$$map₂Functor (F) : ThinSkeleton C → ThinSkeleton D ⥤ ThinSkeleton E$$

Lean4

/-- A functor `C ⥤ D` computably lowers to a functor `ThinSkeleton C ⥤ ThinSkeleton D`. -/
@[simps]
def map (F : C ⥤ D) : ThinSkeleton C ⥤ ThinSkeleton D
    where
  obj := Quotient.map F.obj fun _ _ ⟨hX⟩ => ⟨F.mapIso hX⟩
  map {X} {Y} := Quotient.recOnSubsingleton₂ X Y fun _ _ k => homOfLE (k.le.elim fun t => ⟨F.map t⟩)

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