preservesInjectiveObjects_of_isEquivalence

English

If F is an equivalence, then F preserves injective objects.

Русский

Если F - эквивалентность, то F сохраняет инъективные объекты.

LaTeX

$$$$\\forall F \\;[F\\IsEquivalence] \\;\\Rightarrow \\; F\\PreservesInjectiveObjects.$$$$

Lean4

instance (priority := low) preservesInjectiveObjects_of_isEquivalence {F : C ⥤ D} [IsEquivalence F] :
    F.PreservesInjectiveObjects :=
  preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms F.asEquivalence.symm.toAdjunction

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