Documentation

Mathlib.Algebra.Module.Injective

Injective modules #

Main definitions #

Main statements #

source
šŸ”¶ coverage
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
Instances
    source
    šŸ“ coverage
    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
    source
    šŸ”¹ coverage
    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
      Instances For
        source
        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
        source
        šŸ“ coverage
        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) :
        Baer R Q ā†” Baer R M
        source
        šŸ”¶ coverage
        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
          source
          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āŸ©) :
          a = b
          source
          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 = b

          A dependent version of ExtensionOf.ext

          source
          šŸ“ coverage
          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} :
          a = b ā†” āˆƒ (_ : a.domain = b.domain), āˆ€ ā¦ƒx : ā†„a.domainā¦„ ā¦ƒy : ā†„b.domainā¦„, ā†‘x = ā†‘y ā†’ ā†‘a.toLinearPMap x = ā†‘b.toLinearPMap y
          source
          šŸ“ coverage
          theorem Module.Baer.ExtensionOf.toLinearPMap_injective {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} :
          Function.Injective toLinearPMap
          source
          šŸ”ø coverage
          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
            source
            šŸ”ø coverage
            instance Module.Baer.instPartialOrderExtensionOf {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) :
            PartialOrder (ExtensionOf i f)
            Equations
              source
              šŸ”ø coverage
              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)
              Equations
                source
                šŸ“ coverage
                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)
                source
                šŸ”ø coverage
                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
                  Instances For
                    source
                    šŸ“ coverage
                    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) :
                    a ā‰¤ max hchain hnonempty
                    source
                    šŸ”ø coverage
                    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
                      source
                      šŸ”ø coverage
                      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
                          source
                          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
                          source
                          šŸ”ø coverage
                          @[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
                            Instances For
                              source
                              šŸ”ø coverage
                              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
                                  source
                                  šŸ”ø coverage
                                  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
                                      source
                                      šŸ“ coverage
                                      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)) :
                                      ā†‘x = ā†‘(fst i x) + snd i x ā€¢ y
                                      source
                                      šŸ”ø coverage
                                      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
                                          source
                                          šŸ”ø coverage
                                          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) :
                                          ā†„(ideal i f y) ā†’ā‚—[R] Q

                                          A linear map I āŸ¶ Q by x ā†¦ f' (x ā€¢ y) where f' is the maximal extension

                                          Equations
                                            Instances For
                                              source
                                              šŸ”ø coverage
                                              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) :
                                              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
                                                Instances For
                                                  source
                                                  šŸ“ coverage
                                                  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) :
                                                  (extendIdealTo i f h y) x = (idealTo i f y) āŸØx, memāŸ©
                                                  source
                                                  šŸ“ coverage
                                                  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) :
                                                  (extendIdealTo i f h y) r = 0
                                                  source
                                                  šŸ“ coverage
                                                  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) :
                                                  (extendIdealTo i f h y) r = (extendIdealTo i f h y) r'
                                                  source
                                                  šŸ“ coverage
                                                  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) :
                                                  (extendIdealTo i f h y) r = ā†‘(extensionOfMax i f).toLinearPMap āŸØr ā€¢ y, hrāŸ©
                                                  source
                                                  šŸ”ø coverage
                                                  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
                                                    Instances For
                                                      source
                                                      šŸ“ coverage
                                                      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) :
                                                      extensionToFun i f h x = ā†‘(extensionOfMax i f).toLinearPMap a + (extendIdealTo i f h y) r
                                                      source
                                                      šŸ”ø coverage
                                                      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
                                                        Instances For
                                                          source
                                                          šŸ“ coverage
                                                          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} :
                                                          extensionOfMax i f ā‰¤ extensionOfMaxAdjoin i f h y
                                                          source
                                                          šŸ“ coverage
                                                          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) :
                                                          (extensionOfMax i f).domain = āŠ¤
                                                          source
                                                          šŸ“ coverage
                                                          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) :
                                                          āˆƒ (h : N ā†’ā‚—[R] Q), h āˆ˜ā‚— f = g
                                                          source
                                                          šŸ“ coverage
                                                          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) :
                                                          āˆƒ (h : N ā†’+ Q), h.comp f = g
                                                          source
                                                          šŸ“ coverage
                                                          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.

                                                          source
                                                          šŸ“ coverage
                                                          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
                                                          source
                                                          šŸ“ coverage
                                                          theorem Module.Baer.iff_injective {R : Type u} [Ring R] {Q : Type v} [AddCommGroup Q] [Module R Q] [Small.{v, u} R] :
                                                          Baer R Q ā†” Injective R Q
                                                          source
                                                          šŸ“ coverage
                                                          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)
                                                          source
                                                          šŸ“ coverage
                                                          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
                                                          source
                                                          šŸ“ coverage
                                                          theorem Module.injective_iff_ulift_injective (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [Small.{v, u} R] :
                                                          Injective R M ā†” Injective R (ULift.{v', v} M)
                                                          source
                                                          šŸ“ coverage
                                                          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) :
                                                          āˆƒ (h : P' ā†’ā‚—[R] M), h āˆ˜ā‚— f = g
                                                          source
                                                          šŸ“ coverage
                                                          instance Module.Injective.pi (R : Type u) [Ring R] {Ī¹ : Type w} (M : Ī¹ ā†’ Type v) [Small.{v, u} R] [(i : Ī¹) ā†’ AddCommGroup (M i)] [(i : Ī¹) ā†’ Module R (M i)] [āˆ€ (i : Ī¹), Injective R (M i)] :
                                                          Injective R ((i : Ī¹) ā†’ M i)