instOppositeOpOfProjective — Mathlib

English

If J is Projective in C, then op J has an injective unop image in the opposite direction.

Русский

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

LaTeX

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

Lean4

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

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