English
An R-module Q satisfies Baer's criterion if any R-linear map from an ideal I of R extends to a linear map from R to Q.
Русский
Модуль Q над кольцом R удовлетворяет критерию Баера, если любой линейный отображение из идеала I в Q может быть продолжено до отображения R → Q.
LaTeX
$$$ \text{Baer}(R,Q) := \forall I : \text{Ideal}(R)\; \forall g:I \to_ℓ[R] Q\; \exists g' : R \to_ℓ[R] Q, \forall x (mem : x \in I), g' x = g \langle x, mem\rangle$$$
Lean4
/-- An `R`-module `Q` satisfies Baer's criterion if any `R`-linear map from an `Ideal R` extends to
an `R`-linear map `R ⟶ Q` -/
def Baer : Prop :=
∀ (I : Ideal R) (g : I →ₗ[R] Q), ∃ g' : R →ₗ[R] Q, ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
