# mathlib3documentation

algebra.module.injective

# Injective modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• module.injective: an R-module Q is injective if and only if every injective R-linear map descends to a linear map to Q, i.e. in the following diagram, if f is injective then there is an R-linear map h : Y ⟶ Q such that g = h ∘ f
X --- f ---> Y
|
| g
v
Q

• module.Baer: 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

## Main statements #

• module.Baer.criterion: an R-module is injective if it is Baer.
@[class]
structure module.injective (R : Type u) [ring R] (Q : Type (max u v)) [ Q] :
Prop

An R-module Q is injective if and only if every injective R-linear map descends to a linear map to Q, i.e. in the following diagram, if f is injective then there is an R-linear map h : Y ⟶ Q such that g = h ∘ f

X --- f ---> Y
|
| g
v
Q

theorem module.injective_object_of_injective_module (R : Type u) [ring R] (Q : Type (max u v)) [ Q] [ Q] :
theorem module.injective_module_of_injective_object (R : Type u) [ring R] (Q : Type (max u v)) [ Q]  :
theorem module.injective_iff_injective_object (R : Type u) [ring R] (Q : Type (max u v)) [ Q] :
def module.Baer (R : Type u) [ring R] (Q : Type (max u v)) [ Q] :
Prop

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

Equations
structure module.Baer.extension_of {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) :
Type (max u v)

If we view M as a submodule of N via the injective linear map i : M ↪ N, then a submodule between M and N is a submodule N' of N. To prove Baer's criterion, we need to consider pairs of (N', f') such that M ≤ N' ≤ N and f' extends f.

Instances for module.Baer.extension_of
@[ext]
theorem module.Baer.extension_of.ext {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a b : f} (domain_eq : a.to_linear_pmap.domain = b.to_linear_pmap.domain) (to_fun_eq : ⦃x : (a.to_linear_pmap.domain)⦄ ⦃y : (b.to_linear_pmap.domain)⦄, x = y (a.to_linear_pmap) x = (b.to_linear_pmap) y) :
a = b
theorem module.Baer.extension_of.ext_iff {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a b : f} :
a = b (domain_eq : , ⦃x : (a.to_linear_pmap.domain)⦄ ⦃y : (b.to_linear_pmap.domain)⦄, x = y (a.to_linear_pmap) x = (b.to_linear_pmap) y
@[protected, instance]
def module.Baer.extension_of.has_inf {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) :
Equations
@[protected, instance]
def module.Baer.extension_of.semilattice_inf {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) :
Equations
theorem module.Baer.chain_linear_pmap_of_chain_extension_of {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : set } (hchain : c) :
((λ (x : , x.to_linear_pmap) '' c)
noncomputable def module.Baer.extension_of.max {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : set } (hchain : c) (hnonempty : c.nonempty) :

The maximal element of every nonempty chain of extension_of i f.

Equations
theorem module.Baer.extension_of.le_max {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : set } (hchain : c) (hnonempty : c.nonempty) (a : f) (ha : a c) :
a hnonempty
@[protected, instance]
noncomputable def module.Baer.extension_of.inhabited {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] :
Equations
noncomputable def module.Baer.extension_of_max {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] :

Since every nonempty chain has a maximal element, by Zorn's lemma, there is a maximal extension_of i f.

Equations
theorem module.Baer.extension_of_max_is_max {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (a : f) :
noncomputable def module.Baer.extension_of_max_adjoin.fst {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [fact ] {y : N} (x : {y})) :

If x ∈ M ⊔ ⟨y⟩, then x = m + r • y, fst pick an arbitrary such m.

Equations
noncomputable def module.Baer.extension_of_max_adjoin.snd {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [fact ] {y : N} (x : {y})) :
R

If x ∈ M ⊔ ⟨y⟩, then x = m + r • y, snd pick an arbitrary such r.

Equations
theorem module.Baer.extension_of_max_adjoin.eqn {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [fact ] {y : N} (x : {y})) :
noncomputable def module.Baer.extension_of_max_adjoin.ideal {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (y : N) :

the ideal I = {r | r • y ∈ N}

Equations
noncomputable def module.Baer.extension_of_max_adjoin.ideal_to {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (y : N) :

A linear map I ⟶ Q by x ↦ f' (x • y) where f' is the maximal extension

Equations
noncomputable def module.Baer.extension_of_max_adjoin.extend_ideal_to {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) (y : N) :

Since we assumed Q being Baer, the linear map x ↦ f' (x • y) : I ⟶ Q extends to R ⟶ Q, call this extended map φ

Equations
theorem module.Baer.extension_of_max_adjoin.extend_ideal_to_is_extension {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) (y : N) (x : R) (mem : x ) :
= x, mem⟩
theorem module.Baer.extension_of_max_adjoin.extend_ideal_to_wd' {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) {y : N} (r : R) (eq1 : r y = 0) :
theorem module.Baer.extension_of_max_adjoin.extend_ideal_to_wd {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) {y : N} (r r' : R) (eq1 : r y = r' y) :
theorem module.Baer.extension_of_max_adjoin.extend_ideal_to_eq {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) {y : N} (r : R) (hr : r y ) :
= r y, hr⟩
noncomputable def module.Baer.extension_of_max_adjoin.extension_to_fun {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) {y : N} :
{y}) Q

We can finally define a linear map M ⊔ ⟨y⟩ ⟶ Q by x + r • y ↦ f x + φ r

Equations
theorem module.Baer.extension_of_max_adjoin.extension_to_fun_wd {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) {y : N} (x : {y})) (a : ) (r : R) (eq1 : x = a + r y) :
noncomputable def module.Baer.extension_of_max_adjoin {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) (y : N) :

The linear map M ⊔ ⟨y⟩ ⟶ Q by x + r • y ↦ f x + φ r is an extension of f

Equations
theorem module.Baer.extension_of_max_le {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) {y : N} :
theorem module.Baer.extension_of_max_to_submodule_eq_top {R : Type u} [ring R] {Q : Type (max u v)} [ Q] {M N : Type (max u v)} [ M] [ N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact ] (h : Q) :
@[protected]
theorem module.Baer.injective {R : Type u} [ring R] {Q : Type (max u v)} [ Q] (h : Q) :

Baer's criterion for injective module : a Baer module is an injective module, i.e. if every linear map from an ideal can be extended, then the module is injective.