Injective modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
module.injective: anR-moduleQis injective if and only if every injectiveR-linear map descends to a linear map toQ, i.e. in the following diagram, iffis injective then there is anR-linear maph : Y ⟶ Qsuch thatg = h ∘ fX --- f ---> Y | | g v Qmodule.Baer: anR-moduleQsatisfies Baer's criterion if anyR-linear map from anideal Rextends to anR-linear mapR ⟶ Q
Main statements #
module.Baer.criterion: anR-module is injective if it is Baer.
@[class]
structure
module.injective
(R : Type u)
[ring R]
(Q : Type (max u v))
[add_comm_group Q]
[module R Q] :
Prop
- out : ∀ (X Y : Type (max ? ?)) [_inst_4 : add_comm_group X] [_inst_5 : add_comm_group Y] [_inst_6 : module R X] [_inst_7 : module R Y] (f : X →ₗ[R] Y), function.injective ⇑f → ∀ (g : X →ₗ[R] Q), ∃ (h : Y →ₗ[R] Q), ∀ (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
theorem
module.injective_object_of_injective_module
(R : Type u)
[ring R]
(Q : Type (max u v))
[add_comm_group Q]
[module R Q]
[module.injective R Q] :
theorem
module.injective_module_of_injective_object
(R : Type u)
[ring R]
(Q : Type (max u v))
[add_comm_group Q]
[module R Q]
[category_theory.injective (Module.mk Q)] :
module.injective R Q
theorem
module.injective_iff_injective_object
(R : Type u)
[ring R]
(Q : Type (max u v))
[add_comm_group Q]
[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
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)
- to_linear_pmap : N →ₗ.[R] Q
- le : linear_map.range i ≤ self.to_linear_pmap.domain
- is_extension : ∀ (m : M), ⇑f m = ⇑(self.to_linear_pmap) ⟨⇑i m, _⟩
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
- module.Baer.extension_of.has_sizeof_inst
- module.Baer.extension_of.has_inf
- module.Baer.extension_of.semilattice_inf
- module.Baer.extension_of.inhabited
@[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} :
a = b ↔ ∃ (domain_eq : a.to_linear_pmap.domain = b.to_linear_pmap.domain), ∀ ⦃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)}
[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
- module.Baer.extension_of.has_inf i f = {inf := λ (X1 X2 : module.Baer.extension_of i f), {to_linear_pmap := {domain := (X1.to_linear_pmap ⊓ X2.to_linear_pmap).domain, to_fun := (X1.to_linear_pmap ⊓ X2.to_linear_pmap).to_fun}, le := _, is_extension := _}}
@[protected, instance]
def
module.Baer.extension_of.semilattice_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) :
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) :
is_chain has_le.le ((λ (x : module.Baer.extension_of i f), x.to_linear_pmap) '' 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
- module.Baer.extension_of.max hchain hnonempty = {to_linear_pmap := {domain := (linear_pmap.Sup ((λ (x : module.Baer.extension_of i f), x.to_linear_pmap) '' c) _).domain, to_fun := (linear_pmap.Sup ((λ (x : module.Baer.extension_of i f), x.to_linear_pmap) '' c) _).to_fun}, le := _, is_extension := _}
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) :
a ≤ module.Baer.extension_of.max hchain hnonempty
@[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
- module.Baer.extension_of.inhabited i f = {default := {to_linear_pmap := {domain := linear_map.range i, to_fun := {to_fun := λ (x : ↥(linear_map.range i)), ⇑f (Exists.some _), map_add' := _, map_smul' := _}}, le := _, is_extension := _}}
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
theorem
module.Baer.extension_of_max_is_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)]
(a : module.Baer.extension_of i f) :
module.Baer.extension_of_max i f ≤ a → a = module.Baer.extension_of_max i f
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
theorem
module.Baer.extension_of_max_adjoin.eqn
{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})) :
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) :
ideal R
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) :
↥(module.Baer.extension_of_max_adjoin.ideal i f y) →ₗ[R] Q
A linear map I ⟶ Q by x ↦ f' (x • y) where f' is the maximal extension
Equations
- module.Baer.extension_of_max_adjoin.ideal_to i f y = {to_fun := λ (z : ↥(module.Baer.extension_of_max_adjoin.ideal i f y)), ⇑((module.Baer.extension_of_max i f).to_linear_pmap) ⟨↑z • y, _⟩, map_add' := _, map_smul' := _}
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_is_extension
{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)
(x : R)
(mem : x ∈ module.Baer.extension_of_max_adjoin.ideal i f y) :
⇑(module.Baer.extension_of_max_adjoin.extend_ideal_to i f h y) x = ⇑(module.Baer.extension_of_max_adjoin.ideal_to i f y) ⟨x, mem⟩
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) :
⇑(module.Baer.extension_of_max_adjoin.extend_ideal_to i f h y) r = 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) :
⇑(module.Baer.extension_of_max_adjoin.extend_ideal_to i f h y) r = ⇑(module.Baer.extension_of_max_adjoin.extend_ideal_to i f h y) r'
theorem
module.Baer.extension_of_max_adjoin.extend_ideal_to_eq
{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)
(hr : r • y ∈ (module.Baer.extension_of_max i f).to_linear_pmap.domain) :
⇑(module.Baer.extension_of_max_adjoin.extend_ideal_to i f h y) r = ⇑((module.Baer.extension_of_max i f).to_linear_pmap) ⟨r • y, hr⟩
noncomputable
def
module.Baer.extension_of_max_adjoin.extension_to_fun
{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} :
↥((module.Baer.extension_of_max i f).to_linear_pmap.domain ⊔ submodule.span R {y}) → Q
We can finally define a linear map M ⊔ ⟨y⟩ ⟶ Q by x + r • y ↦ f x + φ r
Equations
- module.Baer.extension_of_max_adjoin.extension_to_fun i f h = λ (x : ↥((module.Baer.extension_of_max i f).to_linear_pmap.domain ⊔ submodule.span R {y})), ⇑((module.Baer.extension_of_max i f).to_linear_pmap) (module.Baer.extension_of_max_adjoin.fst i x) + ⇑(module.Baer.extension_of_max_adjoin.extend_ideal_to i f h y) (module.Baer.extension_of_max_adjoin.snd i x)
theorem
module.Baer.extension_of_max_adjoin.extension_to_fun_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}
(x : ↥((module.Baer.extension_of_max i f).to_linear_pmap.domain ⊔ submodule.span R {y}))
(a : ↥((module.Baer.extension_of_max i f).to_linear_pmap.domain))
(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)}
[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
- module.Baer.extension_of_max_adjoin i f h y = {to_linear_pmap := {domain := (module.Baer.extension_of_max i f).to_linear_pmap.domain ⊔ submodule.span R {y}, to_fun := {to_fun := module.Baer.extension_of_max_adjoin.extension_to_fun i f h y, map_add' := _, map_smul' := _}}, le := _, is_extension := _}
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} :
theorem
module.Baer.extension_of_max_to_submodule_eq_top
{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) :
@[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) :
module.injective 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.