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
    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
        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₂) :
          (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₂) :
          (snd R M M₂) x = x.2
          @[simp]
          theorem LinearMap.coe_fst {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
          (fst R M M₂) = Prod.fst
          @[simp]
          theorem LinearMap.coe_snd {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
          (snd R M M₂) = Prod.snd
          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₂] :
          Function.Surjective (fst R M 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₂] :
          Function.Surjective (snd R M M₂)
          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
              @[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) :
              (f.prod g) i = Pi.prod (⇑f) (⇑g) i
              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₃) :
              (f.prod 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₃) :
              fst R M₂ M₃ ∘ₗ f.prod 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₃) :
              snd R M₂ M₃ ∘ₗ f.prod 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₂] :
              (fst R M M₂).prod (snd R M M₂) = 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₂) :
              f.prod g ∘ₗ h = (f ∘ₗ h).prod (g ∘ₗ h)
              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
                Instances For
                  @[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₃)) :
                  (prodEquiv S) f = f.1.prod f.2
                  @[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₃) :
                  (prodEquiv S).symm f = (fst R M₂ M₃ ∘ₗ f, snd R M₂ M₃ ∘ₗ f)
                  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₂] :
                          range (inl R M M₂) = ker (snd R M 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₂] :
                          ker (snd R M M₂) = range (inl R M 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₂] :
                          range (inr R M M₂) = ker (fst R M 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₂] :
                          ker (fst R M M₂) = range (inr R M 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₂] :
                          fst R M M₂ ∘ₗ inl R M M₂ = 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₂] :
                          snd R M M₂ ∘ₗ 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₂] :
                          fst R M M₂ ∘ₗ 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₂] :
                          snd R M M₂ ∘ₗ inr R M M₂ = 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₂] :
                          (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) :
                          (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₂] :
                          (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₂) :
                          (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₂] :
                          inl R M M₂ = id.prod 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₂] :
                          inr R M M₂ = prod 0 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₂] :
                          Function.Injective (inl R M 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₂] :
                          Function.Injective (inr R M 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₂) :
                              (f.coprod 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₃) :
                              f.coprod g ∘ₗ 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₃) :
                              f.coprod g ∘ₗ 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₂] :
                              (inl R M M₂).coprod (inr R M M₂) = 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₃) :
                              coprod 0 g = g ∘ₗ 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₃) :
                              f.coprod 0 = f ∘ₗ 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 ∘ₗ g₁.coprod g₂ = (f ∘ₗ g₁).coprod (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₂] :
                              fst R M M₂ = id.coprod 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₂] :
                              snd R M M₂ = coprod 0 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₃) :
                              f.coprod g ∘ₗ f'.prod 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.coprod_comp_inl_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 × M₂ →ₗ[R] M₃) :
                              (f ∘ₗ inl R M M₂).coprod (f ∘ₗ inr R M M₂) = f
                              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
                                Instances For
                                  @[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₃) :
                                  (coprodEquiv S).symm f = (f ∘ₗ inl R M M₂, f ∘ₗ inr R M 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₃)) :
                                  (coprodEquiv S) f = f.1.coprod f.2
                                  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 g : M × M₂ →ₗ[R] M₃} :
                                  f = g f ∘ₗ inl R M M₂ = g ∘ₗ inl R M M₂ f ∘ₗ inr R M M₂ = g ∘ₗ 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 g : M × M₂ →ₗ[R] M₃} (hl : f ∘ₗ inl R M M₂ = g ∘ₗ inl R M M₂) (hr : f ∘ₗ inr R M M₂ = g ∘ₗ 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₄) :
                                      (f.prodMap 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₂) :
                                      (f.prodMap 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₄) :
                                      ker (f.prodMap g) = (ker f).prod (ker g)
                                      @[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₂] :
                                      @[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₂] :
                                      prodMap 1 1 = 1
                                      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₆) :
                                      f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (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₁₂ f₂₃ : M →ₗ[R] M) (g₁₂ g₂₃ : M₂ →ₗ[R] M₂) :
                                      f₂₃.prodMap g₂₃ * f₁₂.prodMap g₁₂ = (f₂₃ * f₁₂).prodMap (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₁ f₂ : M →ₗ[R] M₃) (g₁ g₂ : M₂ →ₗ[R] M₄) :
                                      (f₁ + f₂).prodMap (g₁ + g₂) = f₁.prodMap g₁ + f₂.prodMap 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₄] :
                                      prodMap 0 0 = 0
                                      @[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₄] [DistribMulAction S M₃] [DistribMulAction S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] (s : S) (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) :
                                      (s f).prodMap (s g) = s f.prodMap g
                                      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.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₄)) :
                                          (prodMapLinear R M M₂ M₃ M₄ S) f = f.1.prodMap f.2
                                          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
                                            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₂)) :
                                              (prodMapRingHom R M M₂) f = f.1.prodMap f.2
                                              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) :
                                              (inl R A B) (a₁ * a₂) = (inl R A B) a₁ * (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) :
                                              (inr R A B) (b₁ * b₂) = (inr R A B) b₁ * (inr R A B) b₂
                                              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
                                                  @[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₂) :
                                                  ((prodMapAlgHom R M M₂) f) i = (f.1 i.1, f.2 i.2)
                                                  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₃) :
                                                  range (f.coprod g) = range frange g
                                                  theorem LinearMap.isCompl_range_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                                  IsCompl (range (inl R M M₂)) (range (inr R M 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₂] :
                                                  range (inl R M M₂)range (inr R M 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₂] :
                                                  Disjoint (range (inl R M M₂)) (range (inr R M 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₂) :
                                                  p.prod q = Submodule.comap (fst R M M₂) pSubmodule.comap (snd R M M₂) q
                                                  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₂) :
                                                  p.prod q = Submodule.map (inl R M M₂) pSubmodule.map (inr R M M₂) q
                                                  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₂} :
                                                  Submodule.span R ((inl R M M₂) '' s (inr R M M₂) '' t) = (Submodule.span R s).prod (Submodule.span R t)
                                                  @[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₃) :
                                                  ker (f.prod g) = ker fker g
                                                  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₃) :
                                                  range (f.prod g) (range f).prod (range g)
                                                  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} [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [AddCommMonoid M₃] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
                                                  (ker f).prod (ker g) ker (f.coprod g)
                                                  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 (range f) (range g)) :
                                                  ker (f.coprod g) = (ker f).prod (ker g)
                                                  theorem Submodule.sup_eq_range {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p q : Submodule R M) :
                                                  @[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) :
                                                  map (LinearMap.inl R M M₂) p = p.prod
                                                  @[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₂) :
                                                  map (LinearMap.inr R M M₂) q = .prod q
                                                  @[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) :
                                                  comap (LinearMap.fst R M M₂) p = p.prod
                                                  @[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₂) :
                                                  comap (LinearMap.snd R M M₂) q = .prod q
                                                  @[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₂) :
                                                  comap (LinearMap.inl R M M₂) (p.prod q) = p
                                                  @[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₂) :
                                                  comap (LinearMap.inr R M M₂) (p.prod q) = q
                                                  @[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₂) :
                                                  map (LinearMap.fst R M M₂) (p.prod q) = p
                                                  @[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₂) :
                                                  map (LinearMap.snd R M M₂) (p.prod q) = q
                                                  @[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
                                                      def Submodule.fstEquiv (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                                      (fst R M M₂) ≃ₗ[R] M

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

                                                      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 : (fst R M M₂)) :
                                                          (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) :
                                                          ((fstEquiv R M M₂).symm m) = (m, 0)
                                                          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₂] :
                                                          map (LinearMap.fst R M M₂) (fst R M 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₂] :
                                                          map (LinearMap.snd R M M₂) (fst R M 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
                                                              def Submodule.sndEquiv (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                                                              (snd R M M₂) ≃ₗ[R] M₂

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

                                                              Equations
                                                                Instances For
                                                                  @[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₂) :
                                                                  ((sndEquiv R M M₂).symm n) = (0, n)
                                                                  @[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 : (snd R M M₂)) :
                                                                  (sndEquiv R M M₂) x = (↑x).2
                                                                  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₂] :
                                                                  map (LinearMap.fst R M M₂) (snd R M 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₂] :
                                                                  map (LinearMap.snd R M M₂) (snd R M 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₂] :
                                                                  fst R M M₂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₂] :
                                                                  fst R M M₂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 p₁.prod p₂ map (LinearMap.fst R M M₂) q p₁ 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₂)} :
                                                                  p₁.prod p₂ q map (LinearMap.inl R M M₂) p₁ q 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₂} :
                                                                  p₁.prod 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₂} :
                                                                  p₁.prod p₂ = p₁ = p₂ =
                                                                  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
                                                                    Instances For
                                                                      @[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) :
                                                                      (prodComm R M N) a✝ = a✝.swap
                                                                      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 ∘ₗ (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 ∘ₗ (prodComm R M M₂) = LinearMap.fst R M M₂
                                                                      def LinearEquiv.prodAssoc (R : Type u_3) (M₁ : Type u_4) (M₂ : Type u_5) (M₃ : Type u_6) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] :
                                                                      ((M₁ × M₂) × M₃) ≃ₗ[R] M₁ × M₂ × M₃

                                                                      Product of modules is associative up to linear isomorphism.

                                                                      Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem LinearEquiv.prodAssoc_apply (R : Type u_3) (M₁ : Type u_4) (M₂ : Type u_5) (M₃ : Type u_6) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] (a✝ : (M₁ × M₂) × M₃) :
                                                                          (prodAssoc R M₁ M₂ M₃) a✝ = AddEquiv.prodAssoc.toFun a✝
                                                                          theorem LinearEquiv.fst_comp_prodAssoc {R : Type u} {M₂ : Type w} {M₃ : Type y} {M₁ : Type u_3} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] :
                                                                          LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (prodAssoc R M₁ M₂ M₃) = LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃
                                                                          theorem LinearEquiv.snd_comp_prodAssoc {R : Type u} {M₂ : Type w} {M₃ : Type y} {M₁ : Type u_3} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] :
                                                                          LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (prodAssoc R M₁ M₂ M₃) = (LinearMap.snd R M₁ M₂).prodMap LinearMap.id
                                                                          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
                                                                            Instances For
                                                                              @[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₄) :
                                                                              (prodProdProdComm R M M₂ M₃ M₄) mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
                                                                              @[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₄] :
                                                                              (prodProdProdComm R M M₂ M₃ M₄).symm = prodProdProdComm R M M₃ M₂ 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₄] :
                                                                              (prodProdProdComm R M M₂ M₃ M₄) = AddEquiv.prodProdProdComm M M₂ M₃ M₄
                                                                              def LinearEquiv.prodCongr {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
                                                                                Instances For
                                                                                  @[deprecated LinearEquiv.prodCongr (since := "2025-04-17")]
                                                                                  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₄

                                                                                  Alias of LinearEquiv.prodCongr.


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

                                                                                  Equations
                                                                                    Instances For
                                                                                      theorem LinearEquiv.prodCongr_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₄) :
                                                                                      (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm
                                                                                      @[deprecated LinearEquiv.prodCongr_symm (since := "2025-04-17")]
                                                                                      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₄) :
                                                                                      (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm

                                                                                      Alias of LinearEquiv.prodCongr_symm.

                                                                                      @[simp]
                                                                                      theorem LinearEquiv.prodCongr_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₃) :
                                                                                      (e₁.prodCongr e₂) p = (e₁ p.1, e₂ p.2)
                                                                                      @[deprecated LinearEquiv.prodCongr_apply (since := "2025-04-17")]
                                                                                      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₃) :
                                                                                      (e₁.prodCongr e₂) p = (e₁ p.1, e₂ p.2)

                                                                                      Alias of LinearEquiv.prodCongr_apply.

                                                                                      @[simp]
                                                                                      theorem LinearEquiv.coe_prodCongr {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₄) :
                                                                                      (e₁.prodCongr e₂) = (↑e₁).prodMap e₂
                                                                                      @[deprecated LinearEquiv.coe_prodCongr (since := "2025-04-17")]
                                                                                      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₄) :
                                                                                      (e₁.prodCongr e₂) = (↑e₁).prodMap e₂

                                                                                      Alias of LinearEquiv.coe_prodCongr.

                                                                                      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
                                                                                        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₃) :
                                                                                          (e₁.skewProd 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₄) :
                                                                                          (e₁.skewProd e₂ f).symm x = (e₁.symm x.1, e₂.symm (x.2 - f (e₁.symm x.1)))
                                                                                          def LinearEquiv.uniqueProd {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Unique M₂] :
                                                                                          (M₂ × M) ≃ₗ[R] M

                                                                                          Multiplying by the trivial module from the left does not change the structure. This is the LinearEquiv version of AddEquiv.uniqueProd.

                                                                                          Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem LinearEquiv.uniqueProd_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Unique M₂] (a✝ : M₂ × M) :
                                                                                              @[simp]
                                                                                              theorem LinearEquiv.uniqueProd_symm_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Unique M₂] (a✝ : M) :
                                                                                              def LinearEquiv.prodUnique {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Unique M₂] :
                                                                                              (M × M₂) ≃ₗ[R] M

                                                                                              Multiplying by the trivial module from the right does not change the structure. This is the LinearEquiv version of AddEquiv.prodUnique.

                                                                                              Equations
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem LinearEquiv.prodUnique_symm_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Unique M₂] (a✝ : M) :
                                                                                                  @[simp]
                                                                                                  theorem LinearEquiv.prodUnique_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Unique M₂] (a✝ : M × M₂) :
                                                                                                  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 : ker fker g = ) :
                                                                                                  range (f.prod g) = (range f).prod (range 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 #

                                                                                                  NOTE: The proof of strong rank condition for noetherian rings is changed. LinearMap.tunnel and LinearMap.tailing are not used in mathlib anymore. These are marked as deprecated with no replacements. If you use them in external projects, please consider using other arguments instead.

                                                                                                  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.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
                                                                                                    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 f.graph 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₄) :
                                                                                                      g.graph = ker ((-g).coprod id)
                                                                                                      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₂) :
                                                                                                      theorem LinearMap.exists_range_eq_graph {R : Type u_3} {S : Type u_4} {G : Type u_5} {H : Type u_6} {I : Type u_7} [Semiring R] [Semiring S] {σ : R →+* S} [RingHomSurjective σ] [AddCommMonoid G] [Module R G] [AddCommMonoid H] [Module S H] [AddCommMonoid I] [Module S I] {f : G →ₛₗ[σ] H × I} (hf₁ : Function.Surjective (Prod.fst f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1(f g₁).2 = (f g₂).2) :
                                                                                                      ∃ (f' : H →ₗ[S] I), range f = f'.graph

                                                                                                      Vertical line test for linear maps.

                                                                                                      Let f : G → H × I be a linear (or semilinear) map to a product. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(h, i) | i : I} at most once. Then the image of f is the graph of some linear map f' : H → I.

                                                                                                      theorem Submodule.exists_eq_graph {S : Type u_4} {H : Type u_6} {I : Type u_7} [Semiring S] [AddCommMonoid H] [Module S H] [AddCommMonoid I] [Module S I] {G : Submodule S (H × I)} (hf₁ : Function.Bijective (Prod.fst G.subtype)) :
                                                                                                      ∃ (f : H →ₗ[S] I), G = f.graph

                                                                                                      Vertical line test for linear maps.

                                                                                                      Let G ≤ H × I be a submodule of a product of modules. Assume that G maps bijectively to the first factor. Then G is the graph of some linear map f : H →ₗ[R] I.

                                                                                                      theorem LinearMap.exists_linearEquiv_eq_graph {R : Type u_3} {S : Type u_4} {G : Type u_5} {H : Type u_6} {I : Type u_7} [Semiring R] [Semiring S] {σ : R →+* S} [RingHomSurjective σ] [AddCommMonoid G] [Module R G] [AddCommMonoid H] [Module S H] [AddCommMonoid I] [Module S I] {f : G →ₛₗ[σ] H × I} (hf₁ : Function.Surjective (Prod.fst f)) (hf₂ : Function.Surjective (Prod.snd f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 (f g₁).2 = (f g₂).2) :
                                                                                                      ∃ (e : H ≃ₗ[S] I), range f = (↑e).graph

                                                                                                      Line test for module isomorphisms.

                                                                                                      Let f : G → H × I be a linear (or semilinear) map to a product of modules. Assume that f is surjective onto both factors and that the image of f intersects every "vertical line" {(h, i) | i : I} and every "horizontal line" {(h, i) | h : H} at most once. Then the image of f is the graph of some module isomorphism f' : H ≃ I.

                                                                                                      theorem Submodule.exists_equiv_eq_graph {S : Type u_4} {H : Type u_6} {I : Type u_7} [Semiring S] [AddCommMonoid H] [Module S H] [AddCommMonoid I] [Module S I] {G : Submodule S (H × I)} (hG₁ : Function.Bijective (Prod.fst G.subtype)) (hG₂ : Function.Bijective (Prod.snd G.subtype)) :
                                                                                                      ∃ (e : H ≃ₗ[S] I), G = (↑e).graph

                                                                                                      Goursat's lemma for module isomorphisms.

                                                                                                      Let G ≤ H × I be a submodule of a product of modules. Assume that the natural maps from G to both factors are bijective. Then G is the graph of some module isomorphism f : H ≃ I.