quotientFunctor_map_id — Mathlib

English

The quotient functor maps identity morphisms to identities in the target category.

Русский

Кваттор-функтор отображает тождества морфизмов в тождественные элементы целевой категории.

LaTeX

$$$\forall X: V,\ (FreeRefl.quotientFunctor V).map (𝟙rq X).toPath = 𝟙_. $$$

Lean4

@[simp]
theorem quotientFunctor_map_id (V) [ReflQuiver V] (X : V) : (FreeRefl.quotientFunctor V).map (𝟙rq X).toPath = 𝟙 _ :=
  Quotient.sound _ .mk

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