Injective modules

Main definitions

• Module.Injective: 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
  

• Module.Baer: 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

Main statements

• Module.Baer.injective: an R-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

class Module.Injective (R : Type u) [Ring R] (Q : Type v) [AddCommGroup Q] [Module R Q] : Prop

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

theorem Module.Injective.out {R : Type u} : ∀ {inst : Ring R} {Q : Type v} {inst_1 : AddCommGroup Q} {inst_2 : Module R Q} [self : Module.Injective R Q] ⦃X Y : Type v⦄ [inst_3 : AddCommGroup X] [inst_4 : AddCommGroup Y] [inst_5 : Module R X] [inst_6 : 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

def Module.Baer (R : Type u) [Ring R] (Q : Type v) [AddCommGroup Q] [Module R Q] : Prop

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

• Module.Baer R Q = ∀ (I : Ideal R) (g : ↥I →ₗ[R] Q), ∃ (g' : R →ₗ[R] Q), ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

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
• toFun : ↥self.domain →ₗ[R] Q
• le : LinearMap.range i ≤ self.domain
• is_extension : ∀ (m : M), f m = ↑self.toLinearPMap ⟨i m, ⋯⟩

theorem Module.Baer.ExtensionOf.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} (self : Module.Baer.ExtensionOf i f) : LinearMap.range i ≤ self.domain

theorem Module.Baer.ExtensionOf.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} (self : Module.Baer.ExtensionOf i f) (m : M) : f m = ↑self.toLinearPMap ⟨i m, ⋯⟩

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} : a = b ↔ ∃ (_ : a.domain = b.domain), ∀ ⦃x : ↥a.domain⦄ ⦃y : ↥b.domain⦄, ↑x = ↑y → ↑a.toLinearPMap x = ↑b.toLinearPMap y

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) : SemilatticeInf (Module.Baer.ExtensionOf i f)

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 (x1 x2 : Module.Baer.ExtensionOf i f) => x1 ≤ x2) c) : IsChain (fun (x1 x2 : N →ₗ.[R] Q) => x1 ≤ x2) ((fun (x : Module.Baer.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 (Module.Baer.ExtensionOf i f)} (hchain : IsChain (fun (x1 x2 : Module.Baer.ExtensionOf i f) => x1 ≤ x2) c) (hnonempty : c.Nonempty) : Module.Baer.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 := ⋯ }

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 (x1 x2 : Module.Baer.ExtensionOf i f) => x1 ≤ x2) c) (hnonempty : c.Nonempty) (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)] : Inhabited (Module.Baer.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)] : Module.Baer.ExtensionOf i f

Since every nonempty chain has a maximal element, by Zorn's lemma, there is a maximal extension_of i f.

Equations

• Module.Baer.extensionOfMax i f = ⋯.choose

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, 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}

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

• Module.Baer.ExtensionOfMaxAdjoin.fst i x = ⋯.choose

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

• Module.Baer.ExtensionOfMaxAdjoin.snd i x = ⋯.choose

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.id.smulRight y) (Module.Baer.extensionOfMax i f).domain

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.

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) : R →ₗ[R] Q

Since we assumed Q being Baer, the linear map x ↦ f' (x • y) : I ⟶ Q extends to R ⟶ Q, call this extended map φ

Equations

• Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y = ⋯.choose

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) ⟨x, 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 ⟨r • y, 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.

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) : Module.Baer.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.

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} : Module.Baer.extensionOfMax i f ≤ Module.Baer.extensionOfMaxAdjoin i f h y

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) : ∃ (h : N →ₗ[R] Q), h ∘ₗ f = g

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), h.comp 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) : Module.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 : 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)

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) : ∃ (h : P' →ₗ[R] M), h ∘ₗ f = g