mathlib3 documentation

algebra.module.injective

Injective modules #

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

Main definitions #

Main statements #

@[class]
structure module.injective (R : Type u) [ring R] (Q : Type (max u v)) [add_comm_group Q] [module R 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
def module.Baer (R : Type u) [ring R] (Q : Type (max u v)) [add_comm_group Q] [module R 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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R 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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a b : module.Baer.extension_of i 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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a b : module.Baer.extension_of i f} :
@[protected, instance]
def module.Baer.extension_of.has_inf {R : Type u} [ring R] {Q : Type (max u v)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R 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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : set (module.Baer.extension_of i f)} (hchain : is_chain has_le.le c) :
noncomputable def module.Baer.extension_of.max {R : Type u} [ring R] {Q : Type (max u v)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : set (module.Baer.extension_of i f)} (hchain : is_chain has_le.le 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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : set (module.Baer.extension_of i f)} (hchain : is_chain has_le.le c) (hnonempty : c.nonempty) (a : module.Baer.extension_of i f) (ha : a c) :
@[protected, instance]
noncomputable def module.Baer.extension_of.inhabited {R : Type u} [ring R] {Q : Type (max u v)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact (function.injective i)] :
Equations
noncomputable def module.Baer.extension_of_max {R : Type u} [ring R] {Q : Type (max u v)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact (function.injective i)] :

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

Equations
noncomputable def module.Baer.extension_of_max_adjoin.fst {R : Type u} [ring R] {Q : Type (max u v)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [fact (function.injective i)] {y : N} (x : ((module.Baer.extension_of_max i f).to_linear_pmap.domain submodule.span R {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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [fact (function.injective i)] {y : N} (x : ((module.Baer.extension_of_max i f).to_linear_pmap.domain submodule.span R {y})) :
R

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

Equations
noncomputable def module.Baer.extension_of_max_adjoin.ideal {R : Type u} [ring R] {Q : Type (max u v)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact (function.injective i)] (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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact (function.injective i)] (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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact (function.injective i)] (h : module.Baer R 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_wd' {R : Type u} [ring R] {Q : Type (max u v)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact (function.injective i)] (h : module.Baer R 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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact (function.injective i)] (h : module.Baer R Q) {y : N} (r r' : R) (eq1 : r y = r' y) :
noncomputable def module.Baer.extension_of_max_adjoin {R : Type u} [ring R] {Q : Type (max u v)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact (function.injective i)] (h : module.Baer R 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)} [add_comm_group Q] [module R Q] {M N : Type (max u v)} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [fact (function.injective i)] (h : module.Baer R Q) {y : N} :
@[protected]
theorem module.Baer.injective {R : Type u} [ring R] {Q : Type (max u v)} [add_comm_group Q] [module R Q] (h : module.Baer R 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.