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.
theorem
Module.injective_iff
(R : Type u)
[Ring R]
(Q : Type v)
[AddCommGroup Q]
[Module R Q]
:
Module.Injective R Q ↔ ∀ ⦃X Y : Type v⦄ [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 : 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
- out : ∀ ⦃X Y : Type v⦄ [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 : Y →ₗ[R] Q), ∀ (x : X), h (f x) = g x
Instances
theorem
Module.injective_object_of_injective_module
(R : Type u)
[Ring R]
(Q : Type v)
[AddCommGroup Q]
[Module R Q]
[inj : Module.Injective R Q]
:
theorem
Module.injective_module_of_injective_object
(R : Type u)
[Ring R]
(Q : Type v)
[AddCommGroup Q]
[Module R Q]
[inj : CategoryTheory.Injective (ModuleCat.of R Q)]
:
Module.Injective R Q
theorem
Module.injective_iff_injective_object
(R : Type u)
[Ring R]
(Q : Type v)
[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
Equations
Instances For
structure
Module.Baer.ExtensionOf
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
extends
LinearPMap
:
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 : Submodule R N
- le : LinearMap.range i ≤ self.domain
- is_extension : ∀ (m : M), f m = ↑self.toLinearPMap { val := i m, property := ⋯ }
Instances For
theorem
Module.Baer.ExtensionOf.ext
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : ↥a.domain⦄ ⦃y : ↥b.domain⦄, ↑x = ↑y → ↑a.toLinearPMap x = ↑b.toLinearPMap y)
:
a = b
theorem
Module.Baer.ExtensionOf.ext_iff
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
:
Inf (Module.Baer.ExtensionOf i f)
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}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
:
Equations
- Module.Baer.instSemilatticeInfExtensionOf i f = Function.Injective.semilatticeInf Module.Baer.ExtensionOf.toLinearPMap ⋯ ⋯
theorem
Module.Baer.chain_linearPMap_of_chain_extensionOf
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : Module.Baer.ExtensionOf i f) => x ≤ x_1) c)
:
def
Module.Baer.ExtensionOf.max
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : Module.Baer.ExtensionOf i f) => x ≤ x_1) c)
(hnonempty : Set.Nonempty c)
:
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}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : Module.Baer.ExtensionOf i f) => 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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
[Fact (Function.Injective ⇑i)]
:
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}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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.
Equations
Instances For
theorem
Module.Baer.extensionOfMax_is_max
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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
Equations
- Module.Baer.supExtensionOfMaxSingleton i f y = (Module.Baer.extensionOfMax i f).domain ⊔ Submodule.span R {y}
Instances For
def
Module.Baer.ExtensionOfMaxAdjoin.fst
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : ↥(Module.Baer.supExtensionOfMaxSingleton i f y))
:
↥(Module.Baer.extensionOfMax i f).domain
If x ∈ M ⊔ ⟨y⟩, then x = m + r • y, fst pick an arbitrary such m.
Equations
Instances For
def
Module.Baer.ExtensionOfMaxAdjoin.snd
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : ↥(Module.Baer.supExtensionOfMaxSingleton i f y))
:
R
If x ∈ M ⊔ ⟨y⟩, then x = m + r • y, snd pick an arbitrary such r.
Equations
Instances For
theorem
Module.Baer.ExtensionOfMaxAdjoin.eqn
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : ↥(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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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}
Equations
- Module.Baer.ExtensionOfMaxAdjoin.ideal i f y = Submodule.comap (LinearMap.smulRight LinearMap.id y) (Module.Baer.extensionOfMax i f).domain
Instances For
def
Module.Baer.ExtensionOfMaxAdjoin.idealTo
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(i : M →ₗ[R] N)
(f : M →ₗ[R] Q)
[Fact (Function.Injective ⇑i)]
(y : N)
:
↥(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
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}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 φ
Equations
Instances For
theorem
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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).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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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}
:
↥(Module.Baer.supExtensionOfMaxSingleton i f y) → 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}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : ↥(Module.Baer.supExtensionOfMaxSingleton i f y))
(a : ↥(Module.Baer.extensionOfMax i f).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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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
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}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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 : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[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).domain = ⊤
theorem
Module.Baer.extension_property
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(h : Module.Baer R Q)
(f : M →ₗ[R] N)
(hf : Function.Injective ⇑f)
(g : M →ₗ[R] Q)
:
theorem
Module.Baer.extension_property_addMonoidHom
{Q : Type v}
[AddCommGroup Q]
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[AddCommGroup N]
(h : Module.Baer ℤ Q)
(f : M →+ N)
(hf : Function.Injective ⇑f)
(g : M →+ Q)
:
∃ (h : N →+ Q), AddMonoidHom.comp h f = g
theorem
Module.Baer.injective
{R : Type u}
[Ring R]
{Q : Type v}
[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.
theorem
Module.Baer.of_injective
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
[Small.{v, u} R]
(inj : Module.Injective R Q)
:
Module.Baer R Q
theorem
Module.Baer.iff_injective
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
[Small.{v, u} R]
:
Module.Baer R Q ↔ Module.Injective R Q
theorem
Module.ulift_injective_of_injective
(R : Type u)
[Ring R]
{M : Type v}
[AddCommGroup M]
[Module R M]
[Small.{v, u} R]
(inj : Module.Injective R M)
:
theorem
Module.injective_of_ulift_injective
(R : Type u)
[Ring R]
{M : Type v}
[AddCommGroup M]
[Module R M]
(inj : Module.Injective R (ULift.{v', v} M))
:
Module.Injective R M
theorem
Module.injective_iff_ulift_injective
(R : Type u)
[Ring R]
(M : Type v)
[AddCommGroup M]
[Module R M]
[Small.{v, u} R]
:
Module.Injective R M ↔ Module.Injective R (ULift.{v', v} M)
instance
ModuleCat.ulift_injective_of_injective
(R : Type u)
[Ring R]
(M : Type v)
[AddCommGroup M]
[Module R M]
[Small.{v, u} R]
[inj : CategoryTheory.Injective (ModuleCat.of R M)]
:
Equations
- ⋯ = ⋯
theorem
Module.Injective.extension_property
(R : Type uR)
[Ring R]
[Small.{uM, uR} R]
(M : Type uM)
[AddCommGroup M]
[Module R M]
[inj : Module.Injective R M]
(P : Type uP)
[AddCommGroup P]
[Module R P]
(P' : Type uP')
[AddCommGroup P']
[Module R P']
(f : P →ₗ[R] P')
(hf : Function.Injective ⇑f)
(g : P →ₗ[R] M)
: