equalizerComparison_comp_π — Mathlib

English

For any functor G, equalizerComparison f g G followed by equalizer.ι (G.map f) (G.map g) equals G.map (equalizer.ι f g).

Русский

Для любой функторной отображающей функции G, композиция equalizerComparison f g G с equalizer.ι (G.map f) (G.map g) равна G.map (equalizer.ι f g).

LaTeX

$$$ equalizerComparison\; f\; g\; G \\; \\circ \\; equalizer.\\iota (G.map f) (G.map g) = G.map (equalizer.\\iota f g)$$$

Lean4

@[reassoc (attr := simp)]
theorem equalizerComparison_comp_π [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] :
    equalizerComparison f g G ≫ equalizer.ι (G.map f) (G.map g) = G.map (equalizer.ι f g) :=
  equalizer.lift_ι _ _

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