ulift_injective_of_injective — Mathlib

English

If M is an R-module, then the ULift of M is also an injective R-module provided M is injective; the lifting preserves injectivity.

Русский

Если M модуль над R, то ULift(M) также является инъективным R-модулем, если M инъективен; перенос сохраняет инъективность.

LaTeX

$$$ \\text{ulift\_injective\_of\_injective }(R,M) : \\text{Module.Injective } R (ULift M)$$$

Lean4

theorem ulift_injective_of_injective [Small.{v} R] (inj : Module.Injective R M) : Module.Injective R (ULift.{v'} M) :=
  Module.Baer.injective fun I g ↦
    have ⟨g', hg'⟩ := Module.Baer.iff_injective.mpr inj I (ULift.moduleEquiv.toLinearMap ∘ₗ g)
    ⟨ULift.moduleEquiv.symm.toLinearMap ∘ₗ g', fun r hr ↦ ULift.ext _ _ <| hg' r hr⟩

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