factorThruImage — Mathlib

English

There is a canonical morphism factorThruImage : G ⟶ image f whose composition with image.ι f equals f; i.e., f factors through its image.

Русский

Существует каноническое отображение factorThruImage : G ⟶ image f, такое что композиция factorThruImage ; image.ι f равна f; то есть f factors through image f.

LaTeX

$$$(\\mathrm{factorThruImage}\\ f) \\;\\; ≫ \\;\\; \\mathrm{image.ι}_f = f$$$

Lean4

/-- The corestriction map to the image -/
def factorThruImage : G ⟶ image f :=
  ofHom f.hom.rangeRestrict

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