projective_of_module_projective — Mathlib

English

If P is a projective module in the category of R-modules, then the corresponding object in ModuleCat is projective.

Русский

Если P — проектируемый модуль над R, тогда соответствующий объект в ModuleCat является проектируемым.

LaTeX

$$$ [Small.{v} R] [Module.Projective R P.carrier] \Rightarrow [ModuleCat.Projective R P] $$$

Lean4

instance projective_of_module_projective [Small.{v} R] [Projective P] : Module.Projective R P :=
  by
  refine Module.Projective.of_lifting_property ?_
  intro _ _ _ _ _ _ f g s
  have : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s
  exact ⟨(Projective.factorThru (↟g) (↟f)).hom, ModuleCat.hom_ext_iff.mp <| Projective.factorThru_comp (↟g) (↟f)⟩

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