enoughInjectives_of_enoughProjectives_op

English

If the opposite category C^{op} has enough projectives, then C has enough injectives.

Русский

Если в противоположной категории C^{op} существует достаточно проективных объектов, то в категории C существуют достаточно инъективных объектов.

LaTeX

$$$$\\forall \\mathcal{C} \\;\\big( \\text{EnoughProjectives}(\\mathcal{C}^{op}) \\Rightarrow \\text{EnoughInjectives}(\\mathcal{C}) \\big).$$$$

Lean4

theorem enoughInjectives_of_enoughProjectives_op [EnoughProjectives Cᵒᵖ] : EnoughInjectives C :=
  ⟨fun X => ⟨⟨_, inferInstance, (Projective.π (op X)).unop, inferInstance⟩⟩⟩

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