instUnopOfProjectiveOpposite — Mathlib

English

If J is Projective in C, then unop J is Injective in Cᵒᵖ.

Русский

Если J проективен в C, то unop J инъективен в противоположной категории.

LaTeX

$$$$\text{Projective}(J) \Rightarrow \text{Injective}(\mathrm{unop}(J))$$$$

Lean4

instance {P : Cᵒᵖ} [Projective P] : Injective no_index (unop P) where
  factors g f mono := ⟨(@Projective.factorThru Cᵒᵖ _ P _ _ _ g.op f.op _).unop, Quiver.Hom.op_inj (by simp)⟩

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