# Documentation

Mathlib.Algebra.Module.Injective

# Injective modules #

## 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.injective: an R-module is injective if it is Baer.
class Module.Injective (R : Type u) [Ring R] (Q : TypeMax) [] [Module R Q] :
• out : ∀ (X Y : TypeMax) [inst : ] [inst_1 : ] [inst_2 : Module R X] [inst_3 : Module R Y] (f : X →ₗ[R] Y), ∀ (g : X →ₗ[R] Q), h, ∀ (x : X), h (f x) = g x

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

Instances
def Module.Baer (R : Type u) [Ring R] (Q : TypeMax) [] [Module R Q] :

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

Instances For
structure Module.Baer.ExtensionOf {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) extends :
Type (max u v)
• domain :
• toFun : { x // x s.domain } →ₗ[R] Q
• le : s.domain
• is_extension : ∀ (m : M), f m = s.toLinearPMap { val := i m, property := (_ : i m s.domain) }

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
theorem Module.Baer.ExtensionOf.ext {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a : } {b : } (domain_eq : a.domain = b.domain) (to_fun_eq : ∀ ⦃x : { x // x a.domain }⦄ ⦃y : { x // x b.domain }⦄, x = ya.toLinearPMap x = b.toLinearPMap y) :
a = b
theorem Module.Baer.ExtensionOf.ext_iff {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a : } {b : } :
a = b x, ∀ ⦃x : { x // x a.domain }⦄ ⦃y : { x // x b.domain }⦄, x = ya.toLinearPMap x = b.toLinearPMap y
instance Module.Baer.instInfExtensionOf {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) :
instance Module.Baer.instSemilatticeInfExtensionOf {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) :
theorem Module.Baer.chain_linearPMap_of_chain_extensionOf {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : } (hchain : IsChain (fun x x_1 => x x_1) c) :
IsChain (fun x x_1 => x x_1) ((fun x => x.toLinearPMap) '' c)
def Module.Baer.ExtensionOf.max {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : } (hchain : IsChain (fun x x_1 => x x_1) c) (hnonempty : ) :

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

Instances For
theorem Module.Baer.ExtensionOf.le_max {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : } (hchain : IsChain (fun x x_1 => x x_1) c) (hnonempty : ) (a : ) (ha : a c) :
a Module.Baer.ExtensionOf.max hchain hnonempty
instance Module.Baer.ExtensionOf.inhabited {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] :
def Module.Baer.extensionOfMax {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] :

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

Instances For
theorem Module.Baer.extensionOfMax_is_max {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (a : ) :
@[reducible]
def Module.Baer.supExtensionOfMaxSingleton {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (y : N) :
Instances For
def Module.Baer.ExtensionOfMaxAdjoin.fst {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [] {y : N} (x : { x // }) :
{ x // x ().toLinearPMap.domain }

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

Instances For
def Module.Baer.ExtensionOfMaxAdjoin.snd {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [] {y : N} (x : { x // }) :
R

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

Instances For
theorem Module.Baer.ExtensionOfMaxAdjoin.eqn {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [] {y : N} (x : { x // }) :
def Module.Baer.ExtensionOfMaxAdjoin.ideal {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (y : N) :

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

Instances For
def Module.Baer.ExtensionOfMaxAdjoin.idealTo {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (y : N) :
{ x // } →ₗ[R] Q

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

Instances For
def Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) (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 φ

Instances For
theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) (y : N) (x : R) (mem : ) :
↑() x = ↑() { val := x, property := mem }
theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd' {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} (r : R) (eq1 : r y = 0) :
↑() r = 0
theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} (r : R) (r' : R) (eq1 : r y = r' y) :
↑() r = ↑() r'
theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_eq {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} (r : R) (hr : r y ().toLinearPMap.domain) :
↑() r = ().toLinearPMap { val := r y, property := hr }
def Module.Baer.ExtensionOfMaxAdjoin.extensionToFun {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} :
{ x // }Q

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

Instances For
theorem Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} (x : { x // }) (a : { x // x ().toLinearPMap.domain }) (r : R) (eq1 : x = a + r y) :
= ().toLinearPMap a + ↑() r
def Module.Baer.extensionOfMaxAdjoin {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) (y : N) :

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

Instances For
theorem Module.Baer.extensionOfMax_le {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} :
theorem Module.Baer.extensionOfMax_to_submodule_eq_top {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] {M : Type (max u v)} {N : Type (max u v)} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) :
().toLinearPMap.domain =
theorem Module.Baer.injective {R : Type u} [Ring R] {Q : TypeMax} [] [Module R Q] (h : ) :

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.