imageUnopOp_hom_comp_image_ι — Mathlib

English

The opposite of the composition of the image inclusion for g.unop with imageUnopOp g is equal to the canonical factor-through-image of g.

Русский

Обратная сторона композиции инъекции образа g.unop с imageUnopOp g равна каноническому фактору через образ для g.

LaTeX

$$$ (\mathrm{op}(\mathrm{image}.\iota\, g^{\mathrm{unop}})) \circ (\mathrm{imageUnopOp}\, g)^{\mathrm{hom}} = \mathrm{factorThruImage}(g). $$$

Lean4

theorem imageUnopOp_hom_comp_image_ι : (imageUnopOp g).hom ≫ image.ι g = (factorThruImage g.unop).op := by
  simp only [← cancel_epi (image.ι g.unop).op, ← Category.assoc, image_ι_op_comp_imageUnopOp_hom, ← op_comp, image.fac,
    Quiver.Hom.op_unop]

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