Injective modules #
Main definitions #
module.injective
: anR
-moduleQ
is injective if and only if every injectiveR
-linear map descends to a linear map toQ
, i.e. in the following diagram, iff
is injective then there is anR
-linear maph : Y ⟶ Q
such thatg = h ∘ f
X --- f ---> Y | | g v Q
module.Baer
: anR
-moduleQ
satisfies Baer's criterion if anyR
-linear map from anideal R
extends to anR
-linear mapR ⟶ Q
Main statements #
module.Baer.criterion
: anR
-module is injective if it is Baer.
- 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
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
- 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
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 := _}}
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 := _}
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 := _}}
Since every nonempty chain has a maximal element, by Zorn's lemma, there is a maximal
extension_of i f
.
Equations
If x ∈ M ⊔ ⟨y⟩
, then x = m + r • y
, fst
pick an arbitrary such m
.
Equations
If x ∈ M ⊔ ⟨y⟩
, then x = m + r • y
, snd
pick an arbitrary such r
.
Equations
the ideal I = {r | r • y ∈ N}
Equations
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' := _}
Since we assumed Q
being Baer, the linear map x ↦ f' (x • y) : I ⟶ Q
extends to R ⟶ Q
,
call this extended map φ
Equations
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)
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 := _}
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.