iso_inv_ι — Mathlib

English

The inverse of PreservesEqualizer.iso composed with G.map equalizer.ι equals equalizer.ι of the mapped equalizers.

Русский

Обратное к PreservesEqualizer.iso, композиция с G.map equalizer.ι равна равнопроизводителю на отображениях, полученных применением G.map к f,g.

LaTeX

$$$(\\text{PreservesEqualizer.iso } G f g)^{-1} \\circ G(\\text{equalizer.ι } f g) = \\text{equalizer.ι}(G.map f)(G.map g)$$$

Lean4

@[simp]
theorem iso_inv_ι : (PreservesEqualizer.iso G f g).inv ≫ G.map (equalizer.ι f g) = equalizer.ι (G.map f) (G.map g) :=
  by
  rw [← Iso.cancel_iso_hom_left (PreservesEqualizer.iso G f g), ← Category.assoc, Iso.hom_inv_id]
  simp

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