instIsStableUnderRetractsIsInternallyProjective

English

The class of internally projective objects is closed under retracts in a monoidal closed category.

Русский

Класс внутренних проективных объектов замкнут относительно редуцирования (retracts) в моноидальной замкнутой категории.

LaTeX

$$$ (\\text{isInternallyProjective}).IsStableUnderRetracts.$$$

Lean4

instance : (isInternallyProjective (C := C)).IsStableUnderRetracts where
  of_retract {Y X} r
    h :=
    have : InternallyProjective X := ⟨h⟩
    have : Retract (ihom Y) (ihom X) := r.op.map internalHom
    preservesEpimorphisms.ofRetract this

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