inclusion — Mathlib

English

The embedding functor associated to an inclusion h maps objects by s ↦ ⟨s.val, le_objs h s.prop⟩ and arrows by f ↦ ⟨f.val, h f.prop⟩, preserving identities and composition.

Русский

Встраивающий функтор, связанный с включением h, отображает объекты как ⟨s.val, h s.prop⟩ и стрелки как ⟨f.val, h f.prop⟩, сохраняет тождества и композицию.

LaTeX

$${S T : Subgroupoid C} → (h : S ≤ T) → Functor S.objs.Elem T.objs.Elem$$

Lean4

/-- The functor associated to the embedding of subgroupoids -/
def inclusion {S T : Subgroupoid C} (h : S ≤ T) : S.objs ⥤ T.objs
    where
  obj s := ⟨s.val, le_objs h s.prop⟩
  map f := ⟨f.val, @h ⟨_, _, f.val⟩ f.prop⟩
  map_id _ := rfl
  map_comp _ _ := rfl

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