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

    Instances For
      source
      šŸ“ coverage
      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
      theorem Module.Baer.iff_surjective {M : Type u_1} [AddCommGroup M] {R : Type u} [CommRing R] [Module R M] :
      Baer R M ā†” āˆ€ (I : Ideal R), Function.Surjective ā‡‘(LinearMap.lcomp R M (Submodule.subtype I))
      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
        @[implicit_reducible]
        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)
        source
        šŸ”ø coverage
        @[implicit_reducible]
        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)
        source
        šŸ”ø coverage
        @[implicit_reducible]
        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)
        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
        noncomputable 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.

        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
          @[implicit_reducible]
          noncomputable 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)
          source
          šŸ”ø coverage
          noncomputable 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.

          Instances For
            source
            šŸ“ coverage
            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]
            noncomputable 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
            Instances For
              source
              šŸ”ø coverage
              noncomputable 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.

              Instances For
                source
                šŸ”ø coverage
                noncomputable 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.

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

                  Instances For
                    source
                    šŸ”ø coverage
                    noncomputable 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

                    Instances For
                      source
                      šŸ”ø coverage
                      noncomputable 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 Ļ†

                      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
                        noncomputable 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

                        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
                          noncomputable 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

                          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)
                            source
                            šŸ“ coverage
                            theorem Module.Injective.of_ringEquiv {R : Type u} [Ring R] [Small.{v, u} R] {S : Type u'} [Ring S] {M : Type v} {N : Type v'} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module S N] (eā‚ : R ā‰ƒ+* S) (eā‚‚ : M ā‰ƒā‚›ā‚—[ā†‘eā‚] N) [inj : Injective R M] :
                            Injective S N