Module.injective_object_of_injective_module
theorem Module.injective_object_of_injective_module :
∀ (R : Type u) [inst : Ring R] (Q : Type v) [inst_1 : AddCommGroup Q] [inst_2 : Module R Q]
[inj : Module.Injective R Q], CategoryTheory.Injective (ModuleCat.of R Q)
This theorem, referred to as `Module.injective_object_of_injective_module`, states that for any ring `R` and any `R-module` `Q` with the additive commutative group structure and the module structure, if `Q` is an injective `R-module`, then the object of the category of `R-modules` associated to `Q` is also injective. In other words, the association of `R-modules` to objects in the category of `R-modules` preserves the property of injectivity.
More concisely: If `Q` is an injective `R-module` in the category of `R-modules`, then the object associated to `Q` in this category is also an injective object.
|
Module.Baer.injective
theorem Module.Baer.injective :
∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q],
Module.Baer R Q → Module.Injective R Q
**Baer's Criterion for Injective Modules**: This theorem states that, for any ring `R`, additive commutative group `Q`, and `Q` is a module over `R`, if `Q` satisfies Baer's criterion - meaning for every `R`-linear map from an ideal of `R` there exists an extension to an `R`-linear map from `R` to `Q` - then `Q` is an injective module over `R`. In other words, a module that satisfies Baer's criterion is an injective module.
More concisely: A module over a ring is injective if and only if it satisfies Baer's criterion.
|
Module.Baer.chain_linearPMap_of_chain_extensionOf
theorem Module.Baer.chain_linearPMap_of_chain_extensionOf :
∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
{N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
{i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : Set (Module.Baer.ExtensionOf i f)},
IsChain (fun x x_1 => x ≤ x_1) c → IsChain (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) '' c)
This theorem, called `Module.Baer.chain_linearPMap_of_chain_extensionOf`, states that for any ring `R`, additively commutative groups `Q`, `M`, and `N`, and modules `Q`, `M`, and `N` over `R`, given a linear map `i` from `M` to `N`, a linear map `f` from `M` to `Q`, and a set `c` of extensions of `i` to `f`, if `c` is a chain with respect to the less than or equal to relation, then the set of linear P-maps corresponding to elements of `c` is also a chain with respect to the less than or equal to relation. Here a chain is a set where for any two elements `x` and `y`, either `x` is less than or equal to `y`, `y` is less than or equal to `x`, or `x` and `y` are equal.
More concisely: Given a ring `R`, additively commutative groups `Q`, `M`, and `N`, and modules `Q`, `M`, and `N` over `R`, if `i` is a linear map from `M` to `N`, `f` is a linear map from `M` to `Q`, and `c` is a chain of extensions of `i` to `f`, then the set of linear `Q`-maps corresponding to elements of `c` forms a chain.
|