English
If there exists an injective Module.Injective R Q, then Q is Baer, i.e., Baer objects arise from injective modules via a uniform construction.
Русский
Если существует инъективное модульное отображение, то Q является Баеровым модулем; Баеровы объекты возникают из инъективных модулей устойчивой конструкцией.
LaTeX
$$$ \\text{If } \\text{inj}: \\text{Module.Injective } R Q, \\text{ then } Q \\text{ is Baer}$$$
Lean4
protected theorem of_injective [Small.{v} R] (inj : Module.Injective R Q) : Module.Baer R Q :=
by
intro I g
let eI := Shrink.linearEquiv R I
let eR := Shrink.linearEquiv R R
obtain ⟨g', hg'⟩ :=
Module.Injective.out (eR.symm.toLinearMap ∘ₗ I.subtype ∘ₗ eI.toLinearMap)
(eR.symm.injective.comp <| Subtype.val_injective.comp eI.injective) (g ∘ₗ eI.toLinearMap)
exact ⟨g' ∘ₗ eR.symm.toLinearMap, fun x mx ↦ by simpa [eI, eR] using hg' (equivShrink I ⟨x, mx⟩)⟩
