preserves_epi — Mathlib

English

In a monoidal closed category, if P is internally projective, then the object ihom P preserves epimorphisms.

Русский

В моноидальной замкнутой категории, если P внутри проективен, то ihom P сохраняет эпиморфизмы.

LaTeX

$$$ (\\mathrm{ihom}(P)).\\mathrm{PreservesEpimorphisms}.$$$

Lean4

instance preserves_epi (P : C) [InternallyProjective P] : (ihom P).PreservesEpimorphisms :=
  isInternallyProjective.prop_of_is P

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