Injective modules #
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.injective: anR-module is injective if it is Baer.
- out : ∀ (X Y : TypeMax) [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y] (f : X →ₗ[R] Y), Function.Injective ↑f → ∀ (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
theorem
Module.injective_object_of_injective_module
(R : Type u)
[Ring R]
(Q : TypeMax)
[AddCommGroup Q]
[Module R Q]
[Module.Injective R Q]
:
theorem
Module.injective_module_of_injective_object
(R : Type u)
[Ring R]
(Q : TypeMax)
[AddCommGroup Q]
[Module R Q]
[CategoryTheory.Injective (ModuleCat.mk Q)]
:
Module.Injective R Q
theorem
Module.injective_iff_injective_object
(R : Type u)
[Ring R]
(Q : TypeMax)
[AddCommGroup 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
Instances For
structure
Module.Baer.ExtensionOf
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
extends
LinearPMap
:
Type (max u v)
- domain : Submodule R N
- le : LinearMap.range i ≤ 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}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
{i : M →ₗ[R] N}
{f : M →ₗ[R] Q}
{a : Module.Baer.ExtensionOf i f}
{b : Module.Baer.ExtensionOf i f}
(domain_eq : a.domain = b.domain)
(to_fun_eq : ∀ ⦃x : { x // x ∈ a.domain }⦄ ⦃y : { x // x ∈ b.domain }⦄, ↑x = ↑y → ↑a.toLinearPMap x = ↑b.toLinearPMap y)
:
a = b
theorem
Module.Baer.ExtensionOf.ext_iff
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
{i : M →ₗ[R] N}
{f : M →ₗ[R] Q}
{a : Module.Baer.ExtensionOf i f}
{b : Module.Baer.ExtensionOf i f}
:
instance
Module.Baer.instInfExtensionOf
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
:
Inf (Module.Baer.ExtensionOf i f)
instance
Module.Baer.instSemilatticeInfExtensionOf
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[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}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
{i : M →ₗ[R] N}
{f : M →ₗ[R] Q}
{c : Set (Module.Baer.ExtensionOf i f)}
(hchain : IsChain (fun x x_1 => x ≤ x_1) c)
:
def
Module.Baer.ExtensionOf.max
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
{i : M →ₗ[R] N}
{f : M →ₗ[R] Q}
{c : Set (Module.Baer.ExtensionOf i f)}
(hchain : IsChain (fun x x_1 => x ≤ x_1) c)
(hnonempty : Set.Nonempty c)
:
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}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
{i : M →ₗ[R] N}
{f : M →ₗ[R] Q}
{c : Set (Module.Baer.ExtensionOf i f)}
(hchain : IsChain (fun x x_1 => x ≤ x_1) c)
(hnonempty : Set.Nonempty c)
(a : Module.Baer.ExtensionOf i f)
(ha : a ∈ c)
:
a ≤ Module.Baer.ExtensionOf.max hchain hnonempty
instance
Module.Baer.ExtensionOf.inhabited
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
[Fact (Function.Injective ↑i)]
:
def
Module.Baer.extensionOfMax
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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.
Instances For
theorem
Module.Baer.extensionOfMax_is_max
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
[Fact (Function.Injective ↑i)]
(a : Module.Baer.ExtensionOf i f)
:
Module.Baer.extensionOfMax i f ≤ a → a = Module.Baer.extensionOfMax i f
@[reducible]
def
Module.Baer.supExtensionOfMaxSingleton
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
[Fact (Function.Injective ↑i)]
(y : N)
:
Submodule R N
Instances For
def
Module.Baer.ExtensionOfMaxAdjoin.fst
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
{f : M →ₗ[R] Q}
[Fact (Function.Injective ↑i)]
{y : N}
(x : { x // x ∈ Module.Baer.supExtensionOfMaxSingleton i f y })
:
{ x // x ∈ (Module.Baer.extensionOfMax i f).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}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
{f : M →ₗ[R] Q}
[Fact (Function.Injective ↑i)]
{y : N}
(x : { x // x ∈ Module.Baer.supExtensionOfMaxSingleton i f y })
:
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}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
{f : M →ₗ[R] Q}
[Fact (Function.Injective ↑i)]
{y : N}
(x : { x // x ∈ Module.Baer.supExtensionOfMaxSingleton i f y })
:
↑x = ↑(Module.Baer.ExtensionOfMaxAdjoin.fst i x) + Module.Baer.ExtensionOfMaxAdjoin.snd i x • y
def
Module.Baer.ExtensionOfMaxAdjoin.ideal
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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}
Instances For
def
Module.Baer.ExtensionOfMaxAdjoin.idealTo
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
[Fact (Function.Injective ↑i)]
(y : N)
:
{ x // x ∈ Module.Baer.ExtensionOfMaxAdjoin.ideal i f y } →ₗ[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}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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 φ
Instances For
theorem
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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.ExtensionOfMaxAdjoin.ideal i f y)
:
↑(Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) x = ↑(Module.Baer.ExtensionOfMaxAdjoin.idealTo i f y) { val := x, property := mem }
theorem
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd'
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r = 0
theorem
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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' : R)
(eq1 : r • y = r' • y)
:
↑(Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r = ↑(Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r'
theorem
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_eq
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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.extensionOfMax i f).toLinearPMap.domain)
:
↑(Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r = ↑(Module.Baer.extensionOfMax i f).toLinearPMap { val := r • y, property := hr }
def
Module.Baer.ExtensionOfMaxAdjoin.extensionToFun
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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 // x ∈ Module.Baer.supExtensionOfMaxSingleton i f y } → 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}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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 : { x // x ∈ Module.Baer.supExtensionOfMaxSingleton i f y })
(a : { x // x ∈ (Module.Baer.extensionOfMax i f).toLinearPMap.domain })
(r : R)
(eq1 : ↑x = ↑a + r • y)
:
Module.Baer.ExtensionOfMaxAdjoin.extensionToFun i f h x = ↑(Module.Baer.extensionOfMax i f).toLinearPMap a + ↑(Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r
def
Module.Baer.extensionOfMaxAdjoin
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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
Instances For
theorem
Module.Baer.extensionOfMax_le
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup 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.extensionOfMax_to_submodule_eq_top
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup Q]
[Module R Q]
{M : Type (max u v)}
{N : Type (max u v)}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
[Fact (Function.Injective ↑i)]
(h : Module.Baer R Q)
:
(Module.Baer.extensionOfMax i f).toLinearPMap.domain = ⊤
theorem
Module.Baer.injective
{R : Type u}
[Ring R]
{Q : TypeMax}
[AddCommGroup 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.