functor_homRel_eq_compClosure_eqvGen

English

For any X,Y in C and f,g: X ⟶ Y, the quotient functor’s homRel relation equals the generators of the equivalence generated by CompClosure.

Русский

Для любых X,Y в C и функторных гомов f,g: X ⟶ Y, отношение HomRel, задаваемое квотным функтором, равно общим образцам эквивалентности, породившей CompClosure.

LaTeX

$$$\forall X,Y:\; (f,g : X\to Y),\; (\mathrm{functor}\ r).homRel f g \iff \mathrm{Relation.EqvGen}(\mathrm{CategoryTheory.Quotient.CompClosure}\ r) f g.$$$

Lean4

theorem functor_homRel_eq_compClosure_eqvGen {X Y : C} (f g : X ⟶ Y) :
    (functor r).homRel f g ↔ Relation.EqvGen (@CompClosure C _ r X Y) f g :=
  Quot.eq

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