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.
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⦄ [AddCommGroup X] [AddCommGroup Y] [Module R X] [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_iff
(R : Type u)
[Ring R]
(Q : Type v)
[AddCommGroup Q]
[Module R Q]
:
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 satisfies Baer's criterion if any R-linear map from an Ideal R extends to
an R-linear map R ⟶ Q
Equations
Instances For
theorem
Module.Baer.of_equiv
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
[AddCommGroup M]
[Module R M]
(e : Q ≃ₗ[R] M)
(h : Baer R Q)
:
Baer R M
theorem
Module.Baer.congr
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
{M : Type u_1}
[AddCommGroup M]
[Module R M]
(e : Q ≃ₗ[R] M)
:
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 N →ₗ.[R] Q :
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.
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 b : ExtensionOf i f}
(domain_eq : a.domain = b.domain)
(to_fun_eq : ∀ ⦃x : N⦄ ⦃ha : x ∈ a.domain⦄ ⦃hb : x ∈ b.domain⦄, ↑a.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩)
:
theorem
Module.Baer.ExtensionOf.dExt
{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 b : 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 dependent version of ExtensionOf.ext
theorem
Module.Baer.ExtensionOf.dExt_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 b : ExtensionOf i f}
:
instance
Module.Baer.instMinExtensionOf
{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)
:
Min (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)
:
SemilatticeInf (ExtensionOf i f)
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 (ExtensionOf i f)}
(hchain : IsChain (fun (x1 x2 : ExtensionOf i f) => x1 ≤ x2) c)
:
IsChain (fun (x1 x2 : N →ₗ.[R] Q) => x1 ≤ x2) ((fun (x : ExtensionOf i f) => x.toLinearPMap) '' 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 (ExtensionOf i f)}
(hchain : IsChain (fun (x1 x2 : ExtensionOf i f) => x1 ≤ x2) c)
(hnonempty : c.Nonempty)
:
ExtensionOf i f
The maximal element of every nonempty chain of extension_of i f.
Equations
- Module.Baer.ExtensionOf.max hchain hnonempty = { toLinearPMap := LinearPMap.sSup ((fun (x : Module.Baer.ExtensionOf i f) => x.toLinearPMap) '' c) ⋯, le := ⋯, is_extension := ⋯ }
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 (ExtensionOf i f)}
(hchain : IsChain (fun (x1 x2 : ExtensionOf i f) => x1 ≤ x2) c)
(hnonempty : c.Nonempty)
(a : ExtensionOf i f)
(ha : a ∈ c)
:
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)]
:
Inhabited (ExtensionOf i f)
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)]
:
ExtensionOf i f
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 : ExtensionOf i f)
:
extensionOfMax i f ≤ a → a = extensionOfMax i f
@[reducible, inline]
abbrev
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 : ↥(supExtensionOfMaxSingleton i f y))
:
↥(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 : ↥(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 : ↥(supExtensionOfMaxSingleton i f 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
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)
:
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 : 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 : Baer R Q)
(y : N)
(x : R)
(mem : x ∈ ideal i f y)
:
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 : Baer R Q)
{y : N}
(r : R)
(eq1 : r • y = 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 : Baer R Q)
{y : N}
(r r' : R)
(eq1 : r • y = r' • y)
:
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 : Baer R Q)
{y : N}
(r : R)
(hr : r • y ∈ (extensionOfMax i f).domain)
:
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 : Baer R Q)
{y : N}
:
↥(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 : Baer R Q)
{y : N}
(x : ↥(supExtensionOfMaxSingleton i f y))
(a : ↥(extensionOfMax i f).domain)
(r : R)
(eq1 : ↑x = ↑a + r • y)
:
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 : Baer R Q)
(y : N)
:
ExtensionOf i f
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 : 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 : Baer R Q)
:
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 : 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 : Baer ℤ Q)
(f : M →+ N)
(hf : Function.Injective ⇑f)
(g : M →+ Q)
:
theorem
Module.Baer.injective
{R : Type u}
[Ring R]
{Q : Type v}
[AddCommGroup Q]
[Module R Q]
(h : Baer R Q)
:
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 : Injective R Q)
:
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]
:
theorem
Module.ulift_injective_of_injective
(R : Type u)
[Ring R]
{M : Type v}
[AddCommGroup M]
[Module R M]
[Small.{v, u} R]
(inj : Injective R M)
:
Injective R (ULift.{v', v} M)
theorem
Module.injective_of_ulift_injective
(R : Type u)
[Ring R]
{M : Type v}
[AddCommGroup M]
[Module R M]
(inj : Injective R (ULift.{v', v} M))
:
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]
:
theorem
Module.Injective.extension_property
(R : Type uR)
[Ring R]
[Small.{uM, uR} R]
(M : Type uM)
[AddCommGroup M]
[Module R M]
[inj : 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)
: