equalizerSubobject_arrow — Mathlib

English

Let f,g: X → Y with HasEqualizer f g. The morphism from the equalizerSubobject to X given by the equalizerSubobjectIso f g, followed by the equalizer insertion, equals the original equalizerSubobject arrow.

Русский

Пусть f,g: X → Y с HasEqualizer f g. Морфизм из equalizerSubobject f g в X, полученный через равноправный изоморфизм, затем включение равенизера, дает стрелу равенизера.

LaTeX

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

Lean4

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

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