factorThruImage_comp_imageUnopOp_inv

English

The opposite of the image inclusion composed with imageUnopOp g equals the opposite of the universal morphism through the image of g.unop.

Русский

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

LaTeX

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

Lean4

theorem factorThruImage_comp_imageUnopOp_inv : factorThruImage g ≫ (imageUnopOp g).inv = (image.ι g.unop).op := by
  rw [Iso.comp_inv_eq, image_ι_op_comp_imageUnopOp_hom]

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