Documentation

Mathlib.LinearAlgebra.Prod

Products of modules #

This file defines constructors for linear maps whose domains or codomains are products.

It contains theorems relating these to each other, as well as to Submodule.prod, Submodule.map, Submodule.comap, LinearMap.range, and LinearMap.ker.

Main definitions #

def LinearMap.fst (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
M × M₂ →ₗ[R] M

The first projection of a product is a linear map.

Equations
  • LinearMap.fst R M M₂ = { toAddHom := { toFun := Prod.fst, map_add' := }, map_smul' := }
Instances For
    def LinearMap.snd (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
    M × M₂ →ₗ[R] M₂

    The second projection of a product is a linear map.

    Equations
    • LinearMap.snd R M M₂ = { toAddHom := { toFun := Prod.snd, map_add' := }, map_smul' := }
    Instances For
      @[simp]
      theorem LinearMap.fst_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (x : M × M₂) :
      (LinearMap.fst R M M₂) x = x.1
      @[simp]
      theorem LinearMap.snd_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (x : M × M₂) :
      (LinearMap.snd R M M₂) x = x.2
      theorem LinearMap.fst_surjective {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
      theorem LinearMap.snd_surjective {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
      @[simp]
      theorem LinearMap.prod_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (i : M) :
      (LinearMap.prod f g) i = Pi.prod (f) (g) i
      def LinearMap.prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
      M →ₗ[R] M₂ × M₃

      The prod of two linear maps is a linear map.

      Equations
      Instances For
        theorem LinearMap.coe_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
        (LinearMap.prod f g) = Pi.prod f g
        @[simp]
        theorem LinearMap.fst_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
        LinearMap.fst R M₂ M₃ ∘ₗ LinearMap.prod f g = f
        @[simp]
        theorem LinearMap.snd_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
        LinearMap.snd R M₂ M₃ ∘ₗ LinearMap.prod f g = g
        @[simp]
        theorem LinearMap.pair_fst_snd {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
        LinearMap.prod (LinearMap.fst R M M₂) (LinearMap.snd R M M₂) = LinearMap.id
        theorem LinearMap.prod_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M₂ →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (h : M →ₗ[R] M₂) :
        LinearMap.prod f g ∘ₗ h = LinearMap.prod (f ∘ₗ h) (g ∘ₗ h)
        @[simp]
        theorem LinearMap.prodEquiv_symm_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃] (f : M →ₗ[R] M₂ × M₃) :
        @[simp]
        theorem LinearMap.prodEquiv_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃] (f : (M →ₗ[R] M₂) × (M →ₗ[R] M₃)) :
        def LinearMap.prodEquiv {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃] :
        ((M →ₗ[R] M₂) × (M →ₗ[R] M₃)) ≃ₗ[S] M →ₗ[R] M₂ × M₃

        Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.

        See note [bundled maps over different rings] for why separate R and S semirings are used.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def LinearMap.inl (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
          M →ₗ[R] M × M₂

          The left injection into a product is a linear map.

          Equations
          Instances For
            def LinearMap.inr (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
            M₂ →ₗ[R] M × M₂

            The right injection into a product is a linear map.

            Equations
            Instances For
              theorem LinearMap.range_inl (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              theorem LinearMap.ker_snd (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              theorem LinearMap.range_inr (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              theorem LinearMap.ker_fst (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              @[simp]
              theorem LinearMap.fst_comp_inl (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂ = LinearMap.id
              @[simp]
              theorem LinearMap.snd_comp_inl (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂ = 0
              @[simp]
              theorem LinearMap.fst_comp_inr (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              LinearMap.fst R M M₂ ∘ₗ LinearMap.inr R M M₂ = 0
              @[simp]
              theorem LinearMap.snd_comp_inr (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              LinearMap.snd R M M₂ ∘ₗ LinearMap.inr R M M₂ = LinearMap.id
              @[simp]
              theorem LinearMap.coe_inl {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              (LinearMap.inl R M M₂) = fun (x : M) => (x, 0)
              theorem LinearMap.inl_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (x : M) :
              (LinearMap.inl R M M₂) x = (x, 0)
              @[simp]
              theorem LinearMap.coe_inr {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              (LinearMap.inr R M M₂) = Prod.mk 0
              theorem LinearMap.inr_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (x : M₂) :
              (LinearMap.inr R M M₂) x = (0, x)
              theorem LinearMap.inl_eq_prod {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              LinearMap.inl R M M₂ = LinearMap.prod LinearMap.id 0
              theorem LinearMap.inr_eq_prod {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              LinearMap.inr R M M₂ = LinearMap.prod 0 LinearMap.id
              theorem LinearMap.inl_injective {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              theorem LinearMap.inr_injective {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
              def LinearMap.coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
              M × M₂ →ₗ[R] M₃

              The coprod function x : M × M₂ ↦ f x.1 + g x.2 is a linear map.

              Equations
              Instances For
                @[simp]
                theorem LinearMap.coprod_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (x : M × M₂) :
                (LinearMap.coprod f g) x = f x.1 + g x.2
                @[simp]
                theorem LinearMap.coprod_inl {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
                LinearMap.coprod f g ∘ₗ LinearMap.inl R M M₂ = f
                @[simp]
                theorem LinearMap.coprod_inr {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
                LinearMap.coprod f g ∘ₗ LinearMap.inr R M M₂ = g
                @[simp]
                theorem LinearMap.coprod_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                LinearMap.coprod (LinearMap.inl R M M₂) (LinearMap.inr R M M₂) = LinearMap.id
                theorem LinearMap.coprod_zero_left {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) :
                LinearMap.coprod 0 g = g ∘ₗ LinearMap.snd R M M₂
                theorem LinearMap.coprod_zero_right {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) :
                LinearMap.coprod f 0 = f ∘ₗ LinearMap.fst R M M₂
                theorem LinearMap.comp_coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M₃ →ₗ[R] M₄) (g₁ : M →ₗ[R] M₃) (g₂ : M₂ →ₗ[R] M₃) :
                f ∘ₗ LinearMap.coprod g₁ g₂ = LinearMap.coprod (f ∘ₗ g₁) (f ∘ₗ g₂)
                theorem LinearMap.fst_eq_coprod {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                LinearMap.fst R M M₂ = LinearMap.coprod LinearMap.id 0
                theorem LinearMap.snd_eq_coprod {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                LinearMap.snd R M M₂ = LinearMap.coprod 0 LinearMap.id
                @[simp]
                theorem LinearMap.coprod_comp_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M₂ →ₗ[R] M₄) (g : M₃ →ₗ[R] M₄) (f' : M →ₗ[R] M₂) (g' : M →ₗ[R] M₃) :
                LinearMap.coprod f g ∘ₗ LinearMap.prod f' g' = f ∘ₗ f' + g ∘ₗ g'
                @[simp]
                theorem LinearMap.coprod_map_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Submodule R M) (S' : Submodule R M₂) :
                @[simp]
                theorem LinearMap.coprodEquiv_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] (f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) :
                @[simp]
                theorem LinearMap.coprodEquiv_symm_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] (f : M × M₂ →ₗ[R] M₃) :
                def LinearMap.coprodEquiv {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] :
                ((M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) ≃ₗ[S] M × M₂ →ₗ[R] M₃

                Taking the product of two maps with the same codomain is equivalent to taking the product of their domains.

                See note [bundled maps over different rings] for why separate R and S semirings are used.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem LinearMap.prod_ext_iff {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] {f : M × M₂ →ₗ[R] M₃} {g : M × M₂ →ₗ[R] M₃} :
                  f = g f ∘ₗ LinearMap.inl R M M₂ = g ∘ₗ LinearMap.inl R M M₂ f ∘ₗ LinearMap.inr R M M₂ = g ∘ₗ LinearMap.inr R M M₂
                  theorem LinearMap.prod_ext {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] {f : M × M₂ →ₗ[R] M₃} {g : M × M₂ →ₗ[R] M₃} (hl : f ∘ₗ LinearMap.inl R M M₂ = g ∘ₗ LinearMap.inl R M M₂) (hr : f ∘ₗ LinearMap.inr R M M₂ = g ∘ₗ LinearMap.inr R M M₂) :
                  f = g

                  Split equality of linear maps from a product into linear maps over each component, to allow ext to apply lemmas specific to M →ₗ M₃ and M₂ →ₗ M₃.

                  See note [partially-applied ext lemmas].

                  def LinearMap.prodMap {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) :
                  M × M₂ →ₗ[R] M₃ × M₄

                  prod.map of two linear maps.

                  Equations
                  Instances For
                    theorem LinearMap.coe_prodMap {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) :
                    (LinearMap.prodMap f g) = Prod.map f g
                    @[simp]
                    theorem LinearMap.prodMap_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (x : M × M₂) :
                    (LinearMap.prodMap f g) x = (f x.1, g x.2)
                    theorem LinearMap.prodMap_comap_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) (S : Submodule R M₂) (S' : Submodule R M₄) :
                    theorem LinearMap.ker_prodMap {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) :
                    @[simp]
                    theorem LinearMap.prodMap_id {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                    LinearMap.prodMap LinearMap.id LinearMap.id = LinearMap.id
                    @[simp]
                    theorem LinearMap.prodMap_one {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                    theorem LinearMap.prodMap_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} {M₅ : Type u_1} {M₆ : Type u_2} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [AddCommMonoid M₅] [AddCommMonoid M₆] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [Module R M₅] [Module R M₆] (f₁₂ : M →ₗ[R] M₂) (f₂₃ : M₂ →ₗ[R] M₃) (g₁₂ : M₄ →ₗ[R] M₅) (g₂₃ : M₅ →ₗ[R] M₆) :
                    LinearMap.prodMap f₂₃ g₂₃ ∘ₗ LinearMap.prodMap f₁₂ g₁₂ = LinearMap.prodMap (f₂₃ ∘ₗ f₁₂) (g₂₃ ∘ₗ g₁₂)
                    theorem LinearMap.prodMap_mul {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f₁₂ : M →ₗ[R] M) (f₂₃ : M →ₗ[R] M) (g₁₂ : M₂ →ₗ[R] M₂) (g₂₃ : M₂ →ₗ[R] M₂) :
                    LinearMap.prodMap f₂₃ g₂₃ * LinearMap.prodMap f₁₂ g₁₂ = LinearMap.prodMap (f₂₃ * f₁₂) (g₂₃ * g₁₂)
                    theorem LinearMap.prodMap_add {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f₁ : M →ₗ[R] M₃) (f₂ : M →ₗ[R] M₃) (g₁ : M₂ →ₗ[R] M₄) (g₂ : M₂ →ₗ[R] M₄) :
                    LinearMap.prodMap (f₁ + f₂) (g₁ + g₂) = LinearMap.prodMap f₁ g₁ + LinearMap.prodMap f₂ g₂
                    @[simp]
                    theorem LinearMap.prodMap_zero {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] :
                    @[simp]
                    theorem LinearMap.prodMap_smul {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} (S : Type u_3) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [Module S M₃] [Module S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] (s : S) (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) :
                    @[simp]
                    theorem LinearMap.prodMapLinear_apply (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) (S : Type u_3) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [Module S M₃] [Module S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] (f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄)) :
                    (LinearMap.prodMapLinear R M M₂ M₃ M₄ S) f = LinearMap.prodMap f.1 f.2
                    def LinearMap.prodMapLinear (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) (S : Type u_3) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [Module S M₃] [Module S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] :
                    (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄) →ₗ[S] M × M₂ →ₗ[R] M₃ × M₄

                    LinearMap.prodMap as a LinearMap

                    Equations
                    Instances For
                      @[simp]
                      theorem LinearMap.prodMapRingHom_apply (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) :
                      def LinearMap.prodMapRingHom (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                      (M →ₗ[R] M) × (M₂ →ₗ[R] M₂) →+* M × M₂ →ₗ[R] M × M₂

                      LinearMap.prodMap as a RingHom

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem LinearMap.inl_map_mul {R : Type u} [Semiring R] {A : Type u_4} [NonUnitalNonAssocSemiring A] [Module R A] {B : Type u_5} [NonUnitalNonAssocSemiring B] [Module R B] (a₁ : A) (a₂ : A) :
                        (LinearMap.inl R A B) (a₁ * a₂) = (LinearMap.inl R A B) a₁ * (LinearMap.inl R A B) a₂
                        theorem LinearMap.inr_map_mul {R : Type u} [Semiring R] {A : Type u_4} [NonUnitalNonAssocSemiring A] [Module R A] {B : Type u_5} [NonUnitalNonAssocSemiring B] [Module R B] (b₁ : B) (b₂ : B) :
                        (LinearMap.inr R A B) (b₁ * b₂) = (LinearMap.inr R A B) b₁ * (LinearMap.inr R A B) b₂
                        @[simp]
                        theorem LinearMap.prodMapAlgHom_apply_apply (R : Type u) (M : Type v) (M₂ : Type w) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) (i : M × M₂) :
                        ((LinearMap.prodMapAlgHom R M M₂) f) i = (f.1 i.1, f.2 i.2)
                        def LinearMap.prodMapAlgHom (R : Type u) (M : Type v) (M₂ : Type w) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                        Module.End R M × Module.End R M₂ →ₐ[R] Module.End R (M × M₂)

                        LinearMap.prodMap as an AlgHom

                        Equations
                        Instances For
                          theorem LinearMap.range_coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
                          theorem LinearMap.sup_range_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                          theorem LinearMap.disjoint_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                          theorem LinearMap.map_coprod_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : Submodule R M) (q : Submodule R M₂) :
                          theorem LinearMap.comap_prod_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (p : Submodule R M₂) (q : Submodule R M₃) :
                          theorem LinearMap.prod_eq_inf_comap {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) :
                          theorem LinearMap.prod_eq_sup_map {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) :
                          theorem LinearMap.span_inl_union_inr {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {s : Set M} {t : Set M₂} :
                          @[simp]
                          theorem LinearMap.ker_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
                          theorem LinearMap.range_prod_le {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
                          theorem LinearMap.ker_prod_ker_le_ker_coprod {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] {M₃ : Type u_4} [AddCommGroup M₃] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
                          theorem LinearMap.ker_coprod_of_disjoint_range {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] {M₃ : Type u_4} [AddCommGroup M₃] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (hd : Disjoint (LinearMap.range f) (LinearMap.range g)) :
                          @[simp]
                          theorem Submodule.map_inl {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) :
                          @[simp]
                          theorem Submodule.map_inr {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (q : Submodule R M₂) :
                          @[simp]
                          theorem Submodule.comap_fst {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) :
                          @[simp]
                          theorem Submodule.comap_snd {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (q : Submodule R M₂) :
                          @[simp]
                          theorem Submodule.prod_comap_inl {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) :
                          @[simp]
                          theorem Submodule.prod_comap_inr {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) :
                          @[simp]
                          theorem Submodule.prod_map_fst {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) :
                          @[simp]
                          theorem Submodule.prod_map_snd {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) :
                          @[simp]
                          theorem Submodule.ker_inl {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                          @[simp]
                          theorem Submodule.ker_inr {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                          @[simp]
                          theorem Submodule.range_fst {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                          @[simp]
                          theorem Submodule.range_snd {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                          def Submodule.fst (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                          Submodule R (M × M₂)

                          M as a submodule of M × N.

                          Equations
                          Instances For
                            @[simp]
                            theorem Submodule.fstEquiv_apply (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (x : (Submodule.fst R M M₂)) :
                            (Submodule.fstEquiv R M M₂) x = (x).1
                            @[simp]
                            theorem Submodule.fstEquiv_symm_apply_coe (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (m : M) :
                            ((LinearEquiv.symm (Submodule.fstEquiv R M M₂)) m) = (m, 0)
                            def Submodule.fstEquiv (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                            (Submodule.fst R M M₂) ≃ₗ[R] M

                            M as a submodule of M × N is isomorphic to M.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem Submodule.fst_map_fst (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                              theorem Submodule.fst_map_snd (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                              def Submodule.snd (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                              Submodule R (M × M₂)

                              N as a submodule of M × N.

                              Equations
                              Instances For
                                @[simp]
                                theorem Submodule.sndEquiv_apply (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (x : (Submodule.snd R M M₂)) :
                                (Submodule.sndEquiv R M M₂) x = (x).2
                                @[simp]
                                theorem Submodule.sndEquiv_symm_apply_coe (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (n : M₂) :
                                ((LinearEquiv.symm (Submodule.sndEquiv R M M₂)) n) = (0, n)
                                def Submodule.sndEquiv (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                (Submodule.snd R M M₂) ≃ₗ[R] M₂

                                N as a submodule of M × N is isomorphic to N.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem Submodule.snd_map_fst (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                  theorem Submodule.snd_map_snd (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                  theorem Submodule.fst_sup_snd (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                  Submodule.fst R M M₂ Submodule.snd R M M₂ =
                                  theorem Submodule.fst_inf_snd (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                  Submodule.fst R M M₂ Submodule.snd R M M₂ =
                                  theorem Submodule.le_prod_iff (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} :
                                  q Submodule.prod p₁ p₂ Submodule.map (LinearMap.fst R M M₂) q p₁ Submodule.map (LinearMap.snd R M M₂) q p₂
                                  theorem Submodule.prod_le_iff (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} :
                                  Submodule.prod p₁ p₂ q Submodule.map (LinearMap.inl R M M₂) p₁ q Submodule.map (LinearMap.inr R M M₂) p₂ q
                                  theorem Submodule.prod_eq_bot_iff (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂} :
                                  Submodule.prod p₁ p₂ = p₁ = p₂ =
                                  theorem Submodule.prod_eq_top_iff (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂} :
                                  Submodule.prod p₁ p₂ = p₁ = p₂ =
                                  @[simp]
                                  theorem LinearEquiv.prodComm_apply (R : Type u_3) (M : Type u_4) (N : Type u_5) [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                                  ∀ (a : M × N), (LinearEquiv.prodComm R M N) a = Prod.swap a
                                  def LinearEquiv.prodComm (R : Type u_3) (M : Type u_4) (N : Type u_5) [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                                  (M × N) ≃ₗ[R] N × M

                                  Product of modules is commutative up to linear isomorphism.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem LinearEquiv.fst_comp_prodComm {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                    LinearMap.fst R M₂ M ∘ₗ (LinearEquiv.prodComm R M M₂) = LinearMap.snd R M M₂
                                    theorem LinearEquiv.snd_comp_prodComm {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                    LinearMap.snd R M₂ M ∘ₗ (LinearEquiv.prodComm R M M₂) = LinearMap.fst R M M₂
                                    @[simp]
                                    theorem LinearEquiv.prodProdProdComm_apply (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (mnmn : (M × M₂) × M₃ × M₄) :
                                    (LinearEquiv.prodProdProdComm R M M₂ M₃ M₄) mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
                                    def LinearEquiv.prodProdProdComm (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] :
                                    ((M × M₂) × M₃ × M₄) ≃ₗ[R] (M × M₃) × M₂ × M₄

                                    Four-way commutativity of prod. The name matches mul_mul_mul_comm.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem LinearEquiv.prodProdProdComm_symm (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] :
                                      @[simp]
                                      theorem LinearEquiv.prodProdProdComm_toAddEquiv (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] :
                                      (LinearEquiv.prodProdProdComm R M M₂ M₃ M₄) = AddEquiv.prodProdProdComm M M₂ M₃ M₄
                                      def LinearEquiv.prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] {module_M : Module R M} {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄) :
                                      (M × M₃) ≃ₗ[R] M₂ × M₄

                                      Product of linear equivalences; the maps come from Equiv.prodCongr.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem LinearEquiv.prod_symm {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] {module_M : Module R M} {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄) :
                                        @[simp]
                                        theorem LinearEquiv.prod_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] {module_M : Module R M} {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄) (p : M × M₃) :
                                        (LinearEquiv.prod e₁ e₂) p = (e₁ p.1, e₂ p.2)
                                        @[simp]
                                        theorem LinearEquiv.coe_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] {module_M : Module R M} {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄) :
                                        (LinearEquiv.prod e₁ e₂) = LinearMap.prodMap e₁ e₂
                                        def LinearEquiv.skewProd {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommGroup M₄] {module_M : Module R M} {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄) (f : M →ₗ[R] M₄) :
                                        (M × M₃) ≃ₗ[R] M₂ × M₄

                                        Equivalence given by a block lower diagonal matrix. e₁ and e₂ are diagonal square blocks, and f is a rectangular block below the diagonal.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem LinearEquiv.skewProd_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommGroup M₄] {module_M : Module R M} {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄) (f : M →ₗ[R] M₄) (x : M × M₃) :
                                          (LinearEquiv.skewProd e₁ e₂ f) x = (e₁ x.1, e₂ x.2 + f x.1)
                                          @[simp]
                                          theorem LinearEquiv.skewProd_symm_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommGroup M₄] {module_M : Module R M} {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄) (f : M →ₗ[R] M₄) (x : M₂ × M₄) :
                                          (LinearEquiv.symm (LinearEquiv.skewProd e₁ e₂ f)) x = ((LinearEquiv.symm e₁) x.1, (LinearEquiv.symm e₂) (x.2 - f ((LinearEquiv.symm e₁) x.1)))
                                          theorem LinearMap.range_prod_eq {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : LinearMap.ker f LinearMap.ker g = ) :

                                          If the union of the kernels ker f and ker g spans the domain, then the range of Prod f g is equal to the product of range f and range g.

                                          Tunnels and tailings #

                                          Some preliminary work for establishing the strong rank condition for noetherian rings.

                                          Given a morphism f : M × N →ₗ[R] M which is i : Injective f, we can find an infinite decreasing tunnel f i n of copies of M inside M, and sitting beside these, an infinite sequence of copies of N.

                                          We picturesquely name these as tailing f i n for each individual copy of N, and tailings f i n for the supremum of the first n+1 copies: they are the pieces left behind, sitting inside the tunnel.

                                          By construction, each tailing f i (n+1) is disjoint from tailings f i n; later, when we assume M is noetherian, this implies that N must be trivial, and establishes the strong rank condition for any left-noetherian ring.

                                          def LinearMap.tunnelAux {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (Kφ : (K : Submodule R M) × K ≃ₗ[R] M) :
                                          M × N →ₗ[R] M

                                          An auxiliary construction for tunnel. The composition of f, followed by the isomorphism back to K, followed by the inclusion of this submodule back into M.

                                          Equations
                                          Instances For
                                            theorem LinearMap.tunnelAux_injective {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) (Kφ : (K : Submodule R M) × K ≃ₗ[R] M) :
                                            def LinearMap.tunnel' {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) :
                                            (K : Submodule R M) × K ≃ₗ[R] M

                                            Auxiliary definition for tunnel.

                                            Equations
                                            Instances For
                                              def LinearMap.tunnel {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) :

                                              Give an injective map f : M × N →ₗ[R] M we can find a nested sequence of submodules all isomorphic to M.

                                              Equations
                                              Instances For
                                                def LinearMap.tailing {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) (n : ) :

                                                Give an injective map f : M × N →ₗ[R] M we can find a sequence of submodules all isomorphic to N.

                                                Equations
                                                Instances For
                                                  def LinearMap.tailingLinearEquiv {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) (n : ) :

                                                  Each tailing f i n is a copy of N.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    theorem LinearMap.tailing_le_tunnel {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) (n : ) :
                                                    LinearMap.tailing f i n OrderDual.ofDual ((LinearMap.tunnel f i) n)
                                                    theorem LinearMap.tailing_disjoint_tunnel_succ {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) (n : ) :
                                                    Disjoint (LinearMap.tailing f i n) (OrderDual.ofDual ((LinearMap.tunnel f i) (n + 1)))
                                                    theorem LinearMap.tailing_sup_tunnel_succ_le_tunnel {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) (n : ) :
                                                    LinearMap.tailing f i n OrderDual.ofDual ((LinearMap.tunnel f i) (n + 1)) OrderDual.ofDual ((LinearMap.tunnel f i) n)
                                                    def LinearMap.tailings {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) :
                                                    Submodule R M

                                                    The supremum of all the copies of N found inside the tunnel.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem LinearMap.tailings_zero {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) :
                                                      @[simp]
                                                      theorem LinearMap.tailings_succ {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) (n : ) :
                                                      theorem LinearMap.tailings_disjoint_tunnel {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) (n : ) :
                                                      Disjoint (LinearMap.tailings f i n) (OrderDual.ofDual ((LinearMap.tunnel f i) (n + 1)))
                                                      theorem LinearMap.tailings_disjoint_tailing {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M × N →ₗ[R] M) (i : Function.Injective f) (n : ) :
                                                      def LinearMap.graph {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :
                                                      Submodule R (M × M₂)

                                                      Graph of a linear map.

                                                      Equations
                                                      • LinearMap.graph f = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {p : M × M₂ | p.2 = f p.1}, add_mem' := }, zero_mem' := }, smul_mem' := }
                                                      Instances For
                                                        @[simp]
                                                        theorem LinearMap.mem_graph_iff {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (x : M × M₂) :
                                                        x LinearMap.graph f x.2 = f x.1
                                                        theorem LinearMap.graph_eq_ker_coprod {R : Type u} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₃] [Module R M₄] (g : M₃ →ₗ[R] M₄) :
                                                        theorem LinearMap.graph_eq_range_prod {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :