Documentation

Mathlib.Algebra.Module.Injective

Injective modules #

Main definitions #

Main statements #

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

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
    def Module.Baer (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
      • toFun : { x // x s.domain } →ₗ[R] Q
      • le : LinearMap.range i s.domain
      • is_extension : ∀ (m : M), f m = s.toLinearPMap { val := i m, property := (_ : i m 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 = ya.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} :
        a = b x, ∀ ⦃x : { x // x a.domain }⦄ ⦃y : { x // x b.domain }⦄, x = ya.toLinearPMap x = b.toLinearPMap y
        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) :
        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) :
        IsChain (fun x x_1 => x x_1) ((fun x => x.toLinearPMap) '' 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) :
            @[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) :
            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 }) :
                  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) :

                  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) :

                    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) :
                        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) :
                        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} :

                        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) :
                          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) :

                            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.