of_equivalence — Mathlib

English

If e: C ≌ D is an equivalence and D has enough injectives, then C has enough injectives.

Русский

Если e: C ≌ D является эквивалентностью, и D имеет достаточно инъективных объектов, то C тоже имеет достаточно инъективных.

LaTeX

$$$$\\forall {C D},\\; e : C \\simeq D \\;[\\text{EnoughInjectives}(D)]\\Rightarrow \\text{EnoughInjectives}(C).$$$$

Lean4

/-- An equivalence of categories transfers enough injectives. -/
theorem of_equivalence {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] (e : C ⥤ D) [e.IsEquivalence]
    [EnoughInjectives D] : EnoughInjectives C :=
  EnoughInjectives.of_adjunction (adj := e.asEquivalence.toAdjunction)

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