mapVertexGroup — Mathlib

English

A functor induces a monoid homomorphism between the vertex groups of its source and target objects, via the functor’s action on arrows.

Русский

Функтор индуцирует однородный гомоморфизм между вершиновыми группами объектов источника и целевого объекта через действия функторa на стрелы.

LaTeX

$$$\\forall \\varphi : C ⥤ D,\\; \\forall c,\\; (c ⟶ c) \\to^* (\\varphi.obj c ⟶ \\varphi.obj c)$ является моноидовым гомоморфизмом.$$

Lean4

/-- A functor defines a morphism of vertex group. -/
@[simps]
def mapVertexGroup {D : Type v} [Groupoid D] (φ : C ⥤ D) (c : C) : (c ⟶ c) →* (φ.obj c ⟶ φ.obj c)
    where
  toFun := φ.map
  map_one' := φ.map_id c
  map_mul' := φ.map_comp

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