adj_homEquiv — Mathlib

English

The adjunction between the quiver construction and the categorical construction agrees with the Paths equivalence: the hom-equivalence adj.homEquiv(Quiv.of V)(Cat.of C) equals pathsEquiv(V, C).

Русский

Смежение между конструированием квира и категориальным конструированием совпадает с эквивалентностью путей: adj.homEquiv(Quiv.of V)(Cat.of C) = pathsEquiv(V, C).

LaTeX

$$$\operatorname{adj.homEquiv}(\operatorname{Quiv.of} V)(\operatorname{Cat.of} C) = \operatorname{pathsEquiv}(V := V)(C := C).$$$

Lean4

@[simp]
theorem adj_homEquiv {V C : Type u} [Quiver.{max u v + 1} V] [Category.{max u v} C] :
    adj.homEquiv (Quiv.of V) (Cat.of C) = pathsEquiv (V := V) (C := C) :=
  rfl

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