Documentation

Mathlib.LinearAlgebra.Pi

Pi types of modules #

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

It contains theorems relating these to each other, as well as to LinearMap.ker.

Main definitions #

def LinearMap.pi {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) :
M₂ →ₗ[R] (i : ι) → φ i

pi construction for linear functions. From a family of linear functions it produces a linear function into a family of modules.

Equations
  • LinearMap.pi f = { toFun := fun (c : M₂) (i : ι) => (f i) c, map_add' := , map_smul' := }
Instances For
    @[simp]
    theorem LinearMap.pi_apply {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i : ι) :
    (LinearMap.pi f) c i = (f i) c
    theorem LinearMap.ker_pi {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) :
    LinearMap.ker (LinearMap.pi f) = ⨅ (i : ι), LinearMap.ker (f i)
    theorem LinearMap.pi_eq_zero {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) :
    LinearMap.pi f = 0 ∀ (i : ι), f i = 0
    theorem LinearMap.pi_zero {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :
    (LinearMap.pi fun (x : ι) => 0) = 0
    theorem LinearMap.pi_comp {R : Type u} {M₂ : Type w} {M₃ : Type y} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) :
    LinearMap.pi f ∘ₗ g = LinearMap.pi fun (i : ι) => f i ∘ₗ g
    def LinearMap.proj {R : Type u} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) :
    ((i : ι) → φ i) →ₗ[R] φ i

    The projections from a family of modules are linear maps.

    Note: known here as LinearMap.proj, this construction is in other categories called eval, for example Pi.evalMonoidHom, Pi.evalRingHom.

    Equations
    Instances For
      @[simp]
      theorem LinearMap.coe_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) :
      theorem LinearMap.proj_apply {R : Type u} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) (b : (i : ι) → φ i) :
      (LinearMap.proj i) b = b i
      theorem LinearMap.proj_pi {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (i : ι) :
      theorem LinearMap.iInf_ker_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :
      ⨅ (i : ι), LinearMap.ker (LinearMap.proj i) =
      instance LinearMap.CompatibleSMul.pi (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [SMul R M] [SMul R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] :
      LinearMap.CompatibleSMul M (ιN) R S
      Equations
      • =
      @[simp]
      theorem LinearMap.compLeft_apply {R : Type u} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] (f : M₂ →ₗ[R] M₃) (I : Type u_1) (h : IM₂) :
      ∀ (a : I), (f.compLeft I) h a = (f h) a
      def LinearMap.compLeft {R : Type u} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] (f : M₂ →ₗ[R] M₃) (I : Type u_1) :
      (IM₂) →ₗ[R] IM₃

      Linear map between the function spaces I → M₂ and I → M₃, induced by a linear map f between M₂ and M₃.

      Equations
      • f.compLeft I = { toFun := fun (h : IM₂) => f h, map_add' := , map_smul' := }
      Instances For
        theorem LinearMap.apply_single {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [AddCommMonoid M] [Module R M] [DecidableEq ι] (f : (i : ι) → φ i →ₗ[R] M) (i : ι) (j : ι) (x : φ i) :
        (f j) (Pi.single i x j) = Pi.single i ((f i) x) j
        def LinearMap.single (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) :
        φ i →ₗ[R] (i : ι) → φ i

        The LinearMap version of AddMonoidHom.single and Pi.single.

        Equations
        Instances For
          theorem LinearMap.single_apply (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] {i : ι} (v : φ i) :
          @[simp]
          theorem LinearMap.coe_single (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) :
          theorem LinearMap.proj_comp_single_same (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) :
          LinearMap.proj i ∘ₗ LinearMap.single R φ i = LinearMap.id
          theorem LinearMap.proj_comp_single_ne (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) (j : ι) (h : i j) :
          theorem LinearMap.iSup_range_single_le_iInf_ker_proj (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (I : Set ι) (J : Set ι) (h : Disjoint I J) :
          iI, LinearMap.range (LinearMap.single R φ i) iJ, LinearMap.ker (LinearMap.proj i)
          theorem LinearMap.iInf_ker_proj_le_iSup_range_single (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] {I : Finset ι} {J : Set ι} (hu : Set.univ I J) :
          iJ, LinearMap.ker (LinearMap.proj i) iI, LinearMap.range (LinearMap.single R φ i)
          theorem LinearMap.iSup_range_single_eq_iInf_ker_proj (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] {I : Set ι} {J : Set ι} (hd : Disjoint I J) (hu : Set.univ I J) (hI : I.Finite) :
          iI, LinearMap.range (LinearMap.single R φ i) = iJ, LinearMap.ker (LinearMap.proj i)
          theorem LinearMap.iSup_range_single (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] :
          ⨆ (i : ι), LinearMap.range (LinearMap.single R φ i) =
          theorem LinearMap.disjoint_single_single (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (I : Set ι) (J : Set ι) (h : Disjoint I J) :
          Disjoint (⨆ iI, LinearMap.range (LinearMap.single R φ i)) (⨆ iJ, LinearMap.range (LinearMap.single R φ i))
          @[simp]
          theorem LinearMap.lsum_symm_apply (R : Type u) {M : Type v} {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M] (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) :
          (LinearMap.lsum R φ S).symm f i = f ∘ₗ LinearMap.single R φ i
          def LinearMap.lsum (R : Type u) {M : Type v} {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M] :
          ((i : ι) → φ i →ₗ[R] M) ≃ₗ[S] ((i : ι) → φ i) →ₗ[R] M

          The linear equivalence between linear functions on a finite product of modules and families of functions on these modules. See note [bundled maps over different rings].

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem LinearMap.lsum_apply (R : Type u) {M : Type v} {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M] (f : (i : ι) → φ i →ₗ[R] M) :
            (LinearMap.lsum R φ S) f = i : ι, f i ∘ₗ LinearMap.proj i
            @[simp]
            theorem LinearMap.lsum_single {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing R] {M : ιType u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] :
            (LinearMap.lsum R M R) (LinearMap.single R M) = LinearMap.id
            theorem LinearMap.pi_ext {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] [AddCommMonoid M] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} (h : ∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x)) :
            f = g
            theorem LinearMap.pi_ext_iff {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] [AddCommMonoid M] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} :
            f = g ∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x)
            theorem LinearMap.pi_ext'_iff {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] [AddCommMonoid M] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} :
            f = g ∀ (i : ι), f ∘ₗ LinearMap.single R φ i = g ∘ₗ LinearMap.single R φ i
            theorem LinearMap.pi_ext' {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] [AddCommMonoid M] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} (h : ∀ (i : ι), f ∘ₗ LinearMap.single R φ i = g ∘ₗ LinearMap.single R φ i) :
            f = g

            This is used as the ext lemma instead of LinearMap.pi_ext for reasons explained in note [partially-applied ext lemmas].

            def LinearMap.iInfKerProjEquiv (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {J : Set ι} [DecidablePred fun (i : ι) => i I] (hd : Disjoint I J) (hu : Set.univ I J) :
            (⨅ iJ, LinearMap.ker (LinearMap.proj i)) ≃ₗ[R] (i : I) → φ i

            If I and J are disjoint index sets, the product of the kernels of the Jth projections of φ is linearly equivalent to the product over I.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def LinearMap.diag {R : Type u} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) (j : ι) :
              φ i →ₗ[R] φ j

              diag i j is the identity map if i = j. Otherwise it is the constant 0 map.

              Equations
              Instances For
                theorem LinearMap.update_apply {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i : ι) (j : ι) (b : M₂ →ₗ[R] φ i) :
                (Function.update f i b j) c = Function.update (fun (i : ι) => (f i) c) i (b c) j
                theorem LinearMap.single_eq_pi_diag (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) :
                theorem LinearMap.ker_single (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) :
                theorem LinearMap.proj_comp_single (R : Type u) {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) (j : ι) :
                theorem LinearMap.pi_apply_eq_sum_univ {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] [DecidableEq ι] [Fintype ι] (f : (ιR) →ₗ[R] M₂) (x : ιR) :
                f x = i : ι, x i f fun (j : ι) => if i = j then 1 else 0

                A linear map f applied to x : ι → R can be computed using the image under f of elements of the canonical basis.

                def Submodule.pi {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (I : Set ι) (p : (i : ι) → Submodule R (φ i)) :
                Submodule R ((i : ι) → φ i)

                A version of Set.pi for submodules. Given an index set I and a family of submodules p : (i : ι) → Submodule R (φ i), pi I s is the submodule of dependent functions f : (i : ι) → φ i such that f i belongs to p a whenever i ∈ I.

                Equations
                • Submodule.pi I p = { carrier := I.pi fun (i : ι) => (p i), add_mem' := , zero_mem' := , smul_mem' := }
                Instances For
                  @[simp]
                  theorem Submodule.mem_pi {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} {x : (i : ι) → φ i} :
                  x Submodule.pi I p iI, x i p i
                  @[simp]
                  theorem Submodule.coe_pi {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} :
                  (Submodule.pi I p) = I.pi fun (i : ι) => (p i)
                  @[simp]
                  theorem Submodule.pi_empty {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (p : (i : ι) → Submodule R (φ i)) :
                  @[simp]
                  theorem Submodule.pi_top {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (s : Set ι) :
                  (Submodule.pi s fun (i : ι) => ) =
                  theorem Submodule.pi_mono {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} {q : (i : ι) → Submodule R (φ i)} {s : Set ι} (h : is, p i q i) :
                  theorem Submodule.biInf_comap_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} :
                  iI, Submodule.comap (LinearMap.proj i) (p i) = Submodule.pi I p
                  theorem Submodule.iInf_comap_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} :
                  ⨅ (i : ι), Submodule.comap (LinearMap.proj i) (p i) = Submodule.pi Set.univ p
                  theorem Submodule.iSup_map_single {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} [DecidableEq ι] [Finite ι] :
                  ⨆ (i : ι), Submodule.map (LinearMap.single R φ i) (p i) = Submodule.pi Set.univ p
                  theorem Submodule.le_comap_single_pi {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (p : (i : ι) → Submodule R (φ i)) {i : ι} :
                  def LinearEquiv.piCongrRight {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} {ψ : ιType u_2} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i) :
                  ((i : ι) → φ i) ≃ₗ[R] (i : ι) → ψ i

                  Combine a family of linear equivalences into a linear equivalence of pi-types.

                  This is Equiv.piCongrRight as a LinearEquiv

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem LinearEquiv.piCongrRight_apply {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} {ψ : ιType u_2} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i) (f : (i : ι) → φ i) (i : ι) :
                    (LinearEquiv.piCongrRight e) f i = (e i) (f i)
                    @[simp]
                    theorem LinearEquiv.piCongrRight_refl {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :
                    (LinearEquiv.piCongrRight fun (j : ι) => LinearEquiv.refl R (φ j)) = LinearEquiv.refl R ((i : ι) → φ i)
                    @[simp]
                    theorem LinearEquiv.piCongrRight_symm {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} {ψ : ιType u_2} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i) :
                    (LinearEquiv.piCongrRight e).symm = LinearEquiv.piCongrRight fun (i : ι) => (e i).symm
                    @[simp]
                    theorem LinearEquiv.piCongrRight_trans {R : Type u} {ι : Type x} [Semiring R] {φ : ιType u_1} {ψ : ιType u_2} {χ : ιType u_3} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] [(i : ι) → AddCommMonoid (χ i)] [(i : ι) → Module R (χ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i) (f : (i : ι) → ψ i ≃ₗ[R] χ i) :
                    LinearEquiv.piCongrRight e ≪≫ₗ LinearEquiv.piCongrRight f = LinearEquiv.piCongrRight fun (i : ι) => e i ≪≫ₗ f i
                    @[simp]
                    theorem LinearEquiv.piCongrLeft'_symm_apply (R : Type u) {ι : Type x} {ι' : Type x'} [Semiring R] (φ : ιType u_1) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (e : ι ι') :
                    ∀ (a : (b : ι') → φ (e.symm b)) (a_1 : ι), (LinearEquiv.piCongrLeft' R φ e).symm a a_1 = (Equiv.piCongrLeft' φ e).symm a a_1
                    @[simp]
                    theorem LinearEquiv.piCongrLeft'_apply (R : Type u) {ι : Type x} {ι' : Type x'} [Semiring R] (φ : ιType u_1) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (e : ι ι') :
                    ∀ (a : (a : ι) → φ a) (b : ι'), (LinearEquiv.piCongrLeft' R φ e) a b = a (e.symm b)
                    def LinearEquiv.piCongrLeft' (R : Type u) {ι : Type x} {ι' : Type x'} [Semiring R] (φ : ιType u_1) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (e : ι ι') :
                    ((i' : ι) → φ i') ≃ₗ[R] (i : ι') → φ (e.symm i)

                    Transport dependent functions through an equivalence of the base space.

                    This is Equiv.piCongrLeft' as a LinearEquiv.

                    Equations
                    Instances For
                      def LinearEquiv.piCongrLeft (R : Type u) {ι : Type x} {ι' : Type x'} [Semiring R] (φ : ιType u_1) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (e : ι' ι) :
                      ((i' : ι') → φ (e i')) ≃ₗ[R] (i : ι) → φ i

                      Transporting dependent functions through an equivalence of the base, expressed as a "simplification".

                      This is Equiv.piCongrLeft as a LinearEquiv

                      Equations
                      Instances For
                        def LinearEquiv.piCurry (R : Type u) [Semiring R] {ι : Type u_4} {κ : ιType u_5} (α : (i : ι) → κ iType u_6) [(i : ι) → (k : κ i) → AddCommMonoid (α i k)] [(i : ι) → (k : κ i) → Module R (α i k)] :
                        ((i : Sigma κ) → α i.fst i.snd) ≃ₗ[R] (i : ι) → (j : κ i) → α i j

                        Equiv.piCurry as a LinearEquiv.

                        Equations
                        Instances For
                          @[simp]
                          theorem LinearEquiv.piCurry_apply (R : Type u) [Semiring R] {ι : Type u_4} {κ : ιType u_5} (α : (i : ι) → κ iType u_6) [(i : ι) → (k : κ i) → AddCommMonoid (α i k)] [(i : ι) → (k : κ i) → Module R (α i k)] (f : (x : (i : ι) × κ i) → α x.fst x.snd) :
                          @[simp]
                          theorem LinearEquiv.piCurry_symm_apply (R : Type u) [Semiring R] {ι : Type u_4} {κ : ιType u_5} (α : (i : ι) → κ iType u_6) [(i : ι) → (k : κ i) → AddCommMonoid (α i k)] [(i : ι) → (k : κ i) → Module R (α i k)] (f : (a : ι) → (b : κ a) → α a b) :
                          def LinearEquiv.piOptionEquivProd (R : Type u) [Semiring R] {ι : Type u_4} {M : Option ιType u_5} [(i : Option ι) → AddCommGroup (M i)] [(i : Option ι) → Module R (M i)] :
                          ((i : Option ι) → M i) ≃ₗ[R] M none × ((i : ι) → M (some i))

                          This is Equiv.piOptionEquivProd as a LinearEquiv

                          Equations
                          • LinearEquiv.piOptionEquivProd R = { toFun := Equiv.piOptionEquivProd.toFun, map_add' := , map_smul' := , invFun := Equiv.piOptionEquivProd.invFun, left_inv := , right_inv := }
                          Instances For
                            def LinearEquiv.piRing (R : Type u) (M : Type v) (ι : Type x) [Semiring R] (S : Type u_4) [Fintype ι] [DecidableEq ι] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] :
                            ((ιR) →ₗ[R] M) ≃ₗ[S] ιM

                            Linear equivalence between linear functions Rⁿ → M and Mⁿ. The spaces Rⁿ and Mⁿ are represented as ι → R and ι → M, respectively, where ι is a finite type.

                            This as an S-linear equivalence, under the assumption that S acts on M commuting with R. When R is commutative, we can take this to be the usual action with S = R. Otherwise, S = ℕ shows that the equivalence is additive. See note [bundled maps over different rings].

                            Equations
                            Instances For
                              @[simp]
                              theorem LinearEquiv.piRing_apply {R : Type u} {M : Type v} {ι : Type x} [Semiring R] (S : Type u_4) [Fintype ι] [DecidableEq ι] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : (ιR) →ₗ[R] M) (i : ι) :
                              (LinearEquiv.piRing R M ι S) f i = f (Pi.single i 1)
                              @[simp]
                              theorem LinearEquiv.piRing_symm_apply {R : Type u} {M : Type v} {ι : Type x} [Semiring R] (S : Type u_4) [Fintype ι] [DecidableEq ι] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : ιM) (g : ιR) :
                              ((LinearEquiv.piRing R M ι S).symm f) g = i : ι, g i f i
                              def LinearEquiv.sumArrowLequivProdArrow (α : Type u_5) (β : Type u_6) (R : Type u_7) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] :
                              (α βM) ≃ₗ[R] (αM) × (βM)

                              Equiv.sumArrowEquivProdArrow as a linear equivalence.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem LinearEquiv.sumArrowLequivProdArrow_apply_fst {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} {β : Type u_6} (f : α βM) (a : α) :
                                @[simp]
                                theorem LinearEquiv.sumArrowLequivProdArrow_apply_snd {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} {β : Type u_6} (f : α βM) (b : β) :
                                @[simp]
                                theorem LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} {β : Type u_6} (f : αM) (g : βM) (a : α) :
                                (LinearEquiv.sumArrowLequivProdArrow α β R M).symm (f, g) (Sum.inl a) = f a
                                @[simp]
                                theorem LinearEquiv.sumArrowLequivProdArrow_symm_apply_inr {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} {β : Type u_6} (f : αM) (g : βM) (b : β) :
                                (LinearEquiv.sumArrowLequivProdArrow α β R M).symm (f, g) (Sum.inr b) = g b
                                @[simp]
                                theorem LinearEquiv.funUnique_symm_apply (ι : Type u_5) (R : Type u_6) (M : Type u_7) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] :
                                (LinearEquiv.funUnique ι R M).symm = uniqueElim
                                def LinearEquiv.funUnique (ι : Type u_5) (R : Type u_6) (M : Type u_7) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] :
                                (ιM) ≃ₗ[R] M

                                If ι has a unique element, then ι → M is linearly equivalent to M.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem LinearEquiv.funUnique_apply (ι : Type u_5) (R : Type u_6) (M : Type u_7) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] :
                                  @[simp]
                                  theorem LinearEquiv.piFinTwo_symm_apply (R : Type u) [Semiring R] (M : Fin 2Type v) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] :
                                  (LinearEquiv.piFinTwo R M).symm = fun (p : M 0 × M 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
                                  def LinearEquiv.piFinTwo (R : Type u) [Semiring R] (M : Fin 2Type v) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] :
                                  ((i : Fin 2) → M i) ≃ₗ[R] M 0 × M 1

                                  Linear equivalence between dependent functions (i : Fin 2) → M i and M 0 × M 1.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem LinearEquiv.piFinTwo_apply (R : Type u) [Semiring R] (M : Fin 2Type v) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] :
                                    (LinearEquiv.piFinTwo R M) = fun (f : (i : Fin 2) → M i) => (f 0, f 1)
                                    @[simp]
                                    theorem LinearEquiv.finTwoArrow_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :
                                    (LinearEquiv.finTwoArrow R M) = fun (f : Fin 2M) => (f 0, f 1)
                                    @[simp]
                                    theorem LinearEquiv.finTwoArrow_symm_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :
                                    (LinearEquiv.finTwoArrow R M).symm = fun (x : M × M) => ![x.1, x.2]
                                    def LinearEquiv.finTwoArrow (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :
                                    (Fin 2M) ≃ₗ[R] M × M

                                    Linear equivalence between vectors in M² = Fin 2 → M and M × M.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Function.ExtendByZero.linearMap_apply (R : Type u) {ι : Type x} {η : Type x} [Semiring R] (s : ιη) (f : ιR) :
                                      ∀ (a : η), (Function.ExtendByZero.linearMap R s) f a = Function.extend s f 0 a
                                      noncomputable def Function.ExtendByZero.linearMap (R : Type u) {ι : Type x} {η : Type x} [Semiring R] (s : ιη) :
                                      (ιR) →ₗ[R] ηR

                                      Function.extend s f 0 as a bundled linear map.

                                      Equations
                                      Instances For

                                        Bundled versions of Matrix.vecCons and Matrix.vecEmpty #

                                        The idea of these definitions is to be able to define a map as x ↦ ![f₁ x, f₂ x, f₃ x], where f₁ f₂ f₃ are already linear maps, as f₁.vecCons <| f₂.vecCons <| f₃.vecCons <| vecEmpty.

                                        While the same thing could be achieved using LinearMap.pi ![f₁, f₂, f₃], this is not definitionally equal to the result using LinearMap.vecCons, as Fin.cases and function application do not commute definitionally.

                                        Versions for when f₁ f₂ f₃ are bilinear maps are also provided.

                                        def LinearMap.vecEmpty {R : Type u} {M : Type v} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module R M₃] :
                                        M →ₗ[R] Fin 0M₃

                                        The linear map defeq to Matrix.vecEmpty

                                        Equations
                                        • LinearMap.vecEmpty = { toFun := fun (x : M) => ![], map_add' := , map_smul' := }
                                        Instances For
                                          @[simp]
                                          theorem LinearMap.vecEmpty_apply {R : Type u} {M : Type v} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module R M₃] (m : M) :
                                          LinearMap.vecEmpty m = ![]
                                          def LinearMap.vecCons {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {n : } (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin nM₂) :
                                          M →ₗ[R] Fin n.succM₂

                                          A linear map into Fin n.succ → M₃ can be built out of a map into M₃ and a map into Fin n → M₃.

                                          Equations
                                          • f.vecCons g = { toFun := fun (m : M) => Matrix.vecCons (f m) (g m), map_add' := , map_smul' := }
                                          Instances For
                                            @[simp]
                                            theorem LinearMap.vecCons_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {n : } (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin nM₂) (m : M) :
                                            (f.vecCons g) m = Matrix.vecCons (f m) (g m)
                                            @[simp]
                                            theorem LinearMap.vecEmpty₂_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] :
                                            ∀ (x : M), LinearMap.vecEmpty₂ x = LinearMap.vecEmpty
                                            def LinearMap.vecEmpty₂ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] :
                                            M →ₗ[R] M₂ →ₗ[R] Fin 0M₃

                                            The empty bilinear map defeq to Matrix.vecEmpty

                                            Equations
                                            • LinearMap.vecEmpty₂ = { toFun := fun (x : M) => LinearMap.vecEmpty, map_add' := , map_smul' := }
                                            Instances For
                                              @[simp]
                                              theorem LinearMap.vecCons₂_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] {n : } (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] Fin nM₃) (m : M) :
                                              (f.vecCons₂ g) m = (f m).vecCons (g m)
                                              def LinearMap.vecCons₂ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] {n : } (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] Fin nM₃) :
                                              M →ₗ[R] M₂ →ₗ[R] Fin n.succM₃

                                              A bilinear map into Fin n.succ → M₃ can be built out of a map into M₃ and a map into Fin n → M₃

                                              Equations
                                              • f.vecCons₂ g = { toFun := fun (m : M) => (f m).vecCons (g m), map_add' := , map_smul' := }
                                              Instances For