enoughProjectives_of_enoughInjectives_op

English

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

Русский

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

LaTeX

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

Lean4

theorem enoughProjectives_of_enoughInjectives_op [EnoughInjectives Cᵒᵖ] : EnoughProjectives C :=
  ⟨fun X => ⟨{ p := _, f := (Injective.ι (op X)).unop }⟩⟩

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