English
Equivalence of injectivity between M and ULift M preserved via the Baer construction; the logical equivalence asserts the same injectivity property in the lifted context.
Русский
Эквивалентность инъективности между M и ULift M сохраняется через конструкцию Баера; эквивалентность утверждает ту же инъективность в поднятом контексте.
LaTeX
$$$ \\text{injective\_iff\_ulift\_injective} : \\text{Module.Injective } R M \\iff \\text{Module.Injective } R (ULift M)$$$
Lean4
theorem injective_of_ulift_injective (inj : Module.Injective R (ULift.{v'} M)) : Module.Injective R M where
out X Y _ _ _ _ f hf
g :=
let eX := ULift.moduleEquiv.{_, _, v'} (R := R) (M := X)
have ⟨g', hg'⟩ :=
inj.out (ULift.moduleEquiv.{_, _, v'}.symm.toLinearMap ∘ₗ f ∘ₗ eX.toLinearMap)
(by exact ULift.moduleEquiv.symm.injective.comp <| hf.comp eX.injective)
(ULift.moduleEquiv.symm.toLinearMap ∘ₗ g ∘ₗ eX.toLinearMap)
⟨ULift.moduleEquiv.toLinearMap ∘ₗ g' ∘ₗ ULift.moduleEquiv.symm.toLinearMap, fun x ↦ by
exact congr(ULift.down $(hg' ⟨x⟩))⟩
