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.
theorem Module.injective_iff (R : Type u) [Ring R] (Q : Type v) [] [Module R Q] :
∀ ⦃X Y : Type v⦄ [inst : ] [inst_1 : ] [inst_2 : Module R X] [inst_3 : Module R Y] (f : X →ₗ[R] Y), ∀ (g : X →ₗ[R] Q), ∃ (h : Y →ₗ[R] Q), ∀ (x : X), h (f x) = g x
class Module.Injective (R : Type u) [Ring R] (Q : Type v) [] [Module R Q] :

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
theorem Module.Injective.out {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] [self : ] ⦃X : Type v⦄ ⦃Y : Type v⦄ [] [] [Module R X] [Module R Y] (f : X →ₗ[R] Y) :
∀ (g : X →ₗ[R] Q), ∃ (h : Y →ₗ[R] Q), ∀ (x : X), h (f x) = g x
theorem Module.injective_object_of_injective_module (R : Type u) [Ring R] (Q : Type v) [] [Module R Q] [inj : ] :
theorem Module.injective_module_of_injective_object (R : Type u) [Ring R] (Q : Type v) [] [Module R Q] [inj : ] :
theorem Module.injective_iff_injective_object (R : Type u) [Ring R] (Q : Type v) [] [Module R Q] :
def Module.Baer (R : Type u) [Ring R] (Q : Type v) [] [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

Equations
• = ∀ (I : ) (g : I →ₗ[R] Q), ∃ (g' : R →ₗ[R] Q), ∀ (x : R) (mem : x I), g' x = g x, mem
Instances For
structure Module.Baer.ExtensionOf {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) extends :
Type (max u_2 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.

• domain :
• toFun : self.domain →ₗ[R] Q
• le : self.domain
• is_extension : ∀ (m : M), f m = self.toLinearPMap i m,
Instances For
theorem Module.Baer.ExtensionOf.le {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} (self : ) :
self.domain
theorem Module.Baer.ExtensionOf.is_extension {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} (self : ) (m : M) :
f m = self.toLinearPMap i m,
theorem Module.Baer.ExtensionOf.ext {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [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 : a.domain⦄ ⦃y : b.domain⦄, x = ya.toLinearPMap x = b.toLinearPMap y) :
a = b
theorem Module.Baer.ExtensionOf.ext_iff {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a : } {b : } :
a = b ∃ (_ : a.domain = b.domain), ∀ ⦃x : a.domain⦄ ⦃y : b.domain⦄, x = ya.toLinearPMap x = b.toLinearPMap y
instance Module.Baer.instInfExtensionOf {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) :
Equations
• One or more equations did not get rendered due to their size.
instance Module.Baer.instSemilatticeInfExtensionOf {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) :
Equations
theorem Module.Baer.chain_linearPMap_of_chain_extensionOf {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [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 : N →ₗ.[R] Q) => x x_1) ((fun (x : ) => x.toLinearPMap) '' c)
def Module.Baer.ExtensionOf.max {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [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 : c.Nonempty) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Module.Baer.ExtensionOf.le_max {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [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 : c.Nonempty) (a : ) (ha : a c) :
a Module.Baer.ExtensionOf.max hchain hnonempty
instance Module.Baer.ExtensionOf.inhabited {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] :
Equations
• One or more equations did not get rendered due to their size.
def Module.Baer.extensionOfMax {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [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.

Equations
• = .choose
Instances For
theorem Module.Baer.extensionOfMax_is_max {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (a : ) :
@[reducible, inline]
abbrev Module.Baer.supExtensionOfMaxSingleton {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (y : N) :
Equations
Instances For
def Module.Baer.ExtensionOfMaxAdjoin.fst {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [] {y : N} (x : ) :
.domain

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

Equations
• = .choose
Instances For
def Module.Baer.ExtensionOfMaxAdjoin.snd {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [] {y : N} (x : ) :
R

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

Equations
• = .choose
Instances For
theorem Module.Baer.ExtensionOfMaxAdjoin.eqn {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [] {y : N} (x : ) :
def Module.Baer.ExtensionOfMaxAdjoin.ideal {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (y : N) :

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

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [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 φ

Equations
• = .choose
Instances For
theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) (y : N) (x : R) (mem : ) :
= x, mem
theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd' {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} (r : R) (eq1 : r y = 0) :
= 0
theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [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'
theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_eq {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} (r : R) (hr : r y .domain) :
= .toLinearPMap r y, hr
def Module.Baer.ExtensionOfMaxAdjoin.extensionToFun {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} :
Q

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) {y : N} (x : ) (a : .domain) (r : R) (eq1 : x = a + r y) :
= .toLinearPMap a +
def Module.Baer.extensionOfMaxAdjoin {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Module.Baer.extensionOfMax_le {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [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 : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [] (h : ) :
.domain =
theorem Module.Baer.extension_property {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] {M : Type u_1} {N : Type u_2} [] [] [Module R M] [Module R N] (h : ) (f : M →ₗ[R] N) (hf : ) (g : M →ₗ[R] Q) :
∃ (h : N →ₗ[R] Q), h ∘ₗ f = g
theorem Module.Baer.extension_property_addMonoidHom {Q : Type v} [] {M : Type u_1} {N : Type u_2} [] [] (h : ) (f : M →+ N) (hf : ) (g : M →+ Q) :
∃ (h : N →+ Q), h.comp f = g
theorem Module.Baer.injective {R : Type u} [Ring R] {Q : Type v} [] [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.

theorem Module.Baer.of_injective {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] [] (inj : ) :
theorem Module.Baer.iff_injective {R : Type u} [Ring R] {Q : Type v} [] [Module R Q] [] :
theorem Module.ulift_injective_of_injective (R : Type u) [Ring R] {M : Type v} [] [Module R M] [] (inj : ) :
theorem Module.injective_of_ulift_injective (R : Type u) [Ring R] {M : Type v} [] [Module R M] (inj : Module.Injective R ()) :
theorem Module.injective_iff_ulift_injective (R : Type u) [Ring R] (M : Type v) [] [Module R M] [] :
instance ModuleCat.ulift_injective_of_injective (R : Type u) [Ring R] (M : Type v) [] [Module R M] [] [inj : ] :
Equations
• =
theorem Module.Injective.extension_property (R : Type uR) [Ring R] [] (M : Type uM) [] [Module R M] [inj : ] (P : Type uP) [] [Module R P] (P' : Type uP') [] [Module R P'] (f : P →ₗ[R] P') (hf : ) (g : P →ₗ[R] M) :
∃ (h : P' →ₗ[R] M), h ∘ₗ f = g