homFamily — Mathlib

English

For a morphism property P on a category C, the homFamily assigns to each index f in P.toSet the underlying morphism f.1.hom: left object to right object. In other words, each indexed morphism is exactly the hom contained in its index.

Русский

Для категории C и свойствоморфизмов P семейство homFamily сопоставляет каждому индексу f из P.toSet соответствующий ему морфизм f.1.hom: левая вершина → правая вершина. Другими словами, каждая индексированная стрелка равна своей исходной стрелке.

LaTeX

$$$\mathrm{homFamily}(f) = f.1.hom$$$

Lean4

/-- The family of morphisms indexed by `P.toSet` which corresponds
to `P : MorphismProperty C`, see `MorphismProperty.ofHoms_homFamily`. -/
def homFamily (f : P.toSet) : f.1.left ⟶ f.1.right :=
  f.1.hom

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