congruence — Mathlib

English

If H ensures that F maps r-related morphisms equally, then the lift of F along r yields a functor lifting F, i.e., functor r composed with lift r F H equals F.

Русский

Если условие H обеспечивает одинаковость отображения F для r-связанных морфизмов, то подъём lift r F H образует функтор, и композиция functor r с lift равна F.

LaTeX

$$$\mathrm{functor}\ r \;\circ\; \mathrm{lift}\ r F H = F.$$$

Lean4

theorem congruence : Congruence fun X Y => Relation.EqvGen (@CompClosure C _ r X Y) :=
  by
  convert inferInstanceAs (Congruence (functor r).homRel)
  ext
  rw [functor_homRel_eq_compClosure_eqvGen]

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