Documentation

Mathlib.LinearAlgebra.Isomorphisms

Isomorphism theorems for modules. #

The first and second isomorphism theorems for modules.

noncomputable def LinearMap.quotKerEquivRange {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :

The first isomorphism law for modules. The quotient of M by the kernel of f is linearly equivalent to the range of f.

Equations
Instances For
    noncomputable def LinearMap.quotKerEquivOfSurjective {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (hf : Function.Surjective f) :

    The first isomorphism theorem for surjective linear maps.

    Equations
    Instances For
      @[simp]
      theorem LinearMap.quotKerEquivRange_apply_mk {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (x : M) :
      (f.quotKerEquivRange (Submodule.Quotient.mk x)) = f x
      @[simp]
      theorem LinearMap.quotKerEquivRange_symm_apply_image {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (x : M) (h : f x LinearMap.range f) :
      f.quotKerEquivRange.symm f x, h = (LinearMap.ker f).mkQ x
      @[reducible, inline]
      abbrev LinearMap.subToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) :
      p →ₗ[R] (p p') Submodule.comap (p p').subtype p'

      Linear map from p to p+p'/p' where p p' are submodules of R

      Equations
      Instances For
        def LinearMap.quotientInfToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) :
        p Submodule.comap p.subtype (p p') →ₗ[R] (p p') Submodule.comap (p p').subtype p'

        Canonical linear map from the quotient p/(p ∩ p') to (p+p')/p', mapping x + (p ∩ p') to x + p', where p and p' are submodules of an ambient module.

        Equations
        Instances For
          noncomputable def LinearMap.quotientInfEquivSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) :
          (p Submodule.comap p.subtype (p p')) ≃ₗ[R] (p p') Submodule.comap (p p').subtype p'

          Second Isomorphism Law : the canonical map from p/(p ∩ p') to (p+p')/p' as a linear isomorphism.

          Equations
          Instances For
            theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_left {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) (x : (p p')) (hx : x p) :
            theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_right {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) {x : (p p')} (hx : x p') :

            The third isomorphism theorem for modules.

            def Submodule.quotientQuotientEquivQuotientAux {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) (h : S T) :
            (M S) Submodule.map S.mkQ T →ₗ[R] M T

            The map from the third isomorphism theorem for modules: (M / S) / (T / S) → M / T.

            Equations
            • S.quotientQuotientEquivQuotientAux T h = (Submodule.map S.mkQ T).liftQ (S.mapQ T LinearMap.id h)
            Instances For
              @[simp]
              theorem Submodule.quotientQuotientEquivQuotientAux_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) (h : S T) (x : M S) :
              (S.quotientQuotientEquivQuotientAux T h) (Submodule.Quotient.mk x) = (S.mapQ T LinearMap.id h) x
              theorem Submodule.quotientQuotientEquivQuotientAux_mk_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) (h : S T) (x : M) :
              (S.quotientQuotientEquivQuotientAux T h) (Submodule.Quotient.mk (Submodule.Quotient.mk x)) = Submodule.Quotient.mk x
              def Submodule.quotientQuotientEquivQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) (h : S T) :
              ((M S) Submodule.map S.mkQ T) ≃ₗ[R] M T

              Noether's third isomorphism theorem for modules: (M / S) / (T / S) ≃ M / T.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Submodule.quotientQuotientEquivQuotientSup {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) :
                ((M S) Submodule.map S.mkQ T) ≃ₗ[R] M S T

                Essentially the same equivalence as in the third isomorphism theorem, except restated in terms of suprema/addition of submodules instead of .

                Equations
                • S.quotientQuotientEquivQuotientSup T = ((Submodule.map S.mkQ T).quotEquivOfEq (Submodule.map S.mkQ (S T)) ).trans (S.quotientQuotientEquivQuotient (S T) )
                Instances For
                  theorem Submodule.card_quotient_mul_card_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) (hST : T S) :
                  Nat.card (Submodule.map T.mkQ S) * Nat.card (M S) = Nat.card (M T)

                  Corollary of the third isomorphism theorem: [S : T] [M : S] = [M : T]