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
  • One or more equations did not get rendered due to their size.
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) :
      @[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) :
      ↑(LinearEquiv.symm (LinearMap.quotKerEquivRange f)) { val := f x, property := h } = ↑(Submodule.mkQ (LinearMap.ker f)) x
      @[reducible]
      def 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) :
      { x // x p } →ₗ[R] { x // x p p' } Submodule.comap (Submodule.subtype (p p')) 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) :
        { x // x p } Submodule.comap (Submodule.subtype p) (p p') →ₗ[R] { x // x p p' } Submodule.comap (Submodule.subtype (p p')) 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
        • One or more equations did not get rendered due to their size.
        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) :
          ({ x // x p } Submodule.comap (Submodule.subtype p) (p p')) ≃ₗ[R] { x // x p p' } Submodule.comap (Submodule.subtype (p p')) p'

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem LinearMap.quotientInfEquivSupQuotient_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) (x : { x // x p }) :
            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 : { x // 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 : { x // 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) :

            The map from the 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
              @[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) :
              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) :

              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
                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) [DecidablePred fun x => x Submodule.map (Submodule.mkQ T) S] [Fintype (M S)] [Fintype (M T)] :

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