equalizerSubobject_arrow' — Mathlib

English

With HasEqualizer f g, the inverse of the equalizerSubobjectIso f g composed with the equalizerSubobject f g arrow recovers the equalizer morphism: (equalizerSubobjectIso f g).inv ≫ (equalizerSubobject f g).arrow = equalizer.ι f g.

Русский

При наличии HasEqualizer f g обратная часть изоморфизма equalizerSubobject f g, композиция с стрелой подобъекта равенства возвращает исходную стрелу эквалайзера.

LaTeX

$$$$(equalizerSubobjectIso f g).inv \\circ (equalizerSubobject f g).arrow = equalizer.ι f g$$$$

Lean4

@[reassoc (attr := simp)]
theorem equalizerSubobject_arrow' :
    (equalizerSubobjectIso f g).inv ≫ (equalizerSubobject f g).arrow = equalizer.ι f g := by
  simp [equalizerSubobjectIso]

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