imageUnopOp_inv_comp_op_factorThruImage

English

The inverse of the imageUnopOp g composed with the opposite of the factor-through-image of g.unop is the image inclusion map of g.

Русский

Обратная imageUnopOp g после композиции с противоположной частью factorThruImage(g.unop) даёт образовую инъекцию g.

LaTeX

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

Lean4

theorem imageUnopOp_inv_comp_op_factorThruImage : (imageUnopOp g).inv ≫ (factorThruImage g.unop).op = image.ι g := by
  rw [Iso.inv_comp_eq, imageUnopOp_hom_comp_image_ι]

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