instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair

English

If HasImage f and for every Z and arrows g,h: image f ⟶ Z, the limit of the parallel pair (g,h) exists, then factorThroughImage f is epi.

Русский

Если существует образ f и для каждого Z и стрелок g,h: image f → Z существует предел параллельной пары, то factorThroughImage f — эпиморфизм.

LaTeX

$$$ [HasImage(f)] \\; [\\forall Z, \\forall g,h: image(f) \\to Z, \\mathrm{HasLimit}(\\mathrm{parallelPair}(g,h))] \\; \\Rightarrow \\mathrm{Epi}(\\mathrm{factorThruImage}(f)) $$$

Lean4

instance [HasImage f] [∀ {Z : C} (g h : image f ⟶ Z), HasLimit (parallelPair g h)] : Epi (factorThruImage f) :=
  ⟨fun _ _ w => image.ext f w⟩

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