functor_map_eq_iff — Mathlib

English

For any X,Y in C and f,f' : X ⟶ Y, the equality of their images under the quotient functor is equivalent to f and f' being r-related.

Русский

Для любых X,Y и морфизмов f,f': X ⟶ Y, равенство отображений под функтором Quotient эквивалентно тому, что f и f' связаны через r.

LaTeX

$$$\forall X,Y:\; f,f' : X\to Y,\; (\mathrm{functor}\ r).map f = (\mathrm{functor}\ r).map f' \iff r\ f\ f'.$$$

Lean4

theorem functor_map_eq_iff [h : Congruence r] {X Y : C} (f f' : X ⟶ Y) :
    (functor r).map f = (functor r).map f' ↔ r f f' :=
  by
  dsimp [functor]
  rw [Equivalence.quot_mk_eq_iff, compClosure_eq_self r]
  simpa only [compClosure_eq_self r] using h.equivalence

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