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
  • One or more equations did not get rendered due to their size.
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 i => 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₂) :
    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
    • One or more equations did not get rendered due to their size.
    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) =
      @[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), ↑(LinearMap.compLeft f 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
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem LinearMap.coe_single {R : Type u} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (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)] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] [Semiring S] [Module S M] [SMulCommClass R S M] (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) :
          def LinearMap.lsum (R : Type u) {M : Type v} {ι : Type x} [Semiring R] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] [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)] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] [Semiring S] [Module S M] [SMulCommClass R S M] (f : (i : ι) → φ i →ₗ[R] M) :
            ↑(LinearMap.lsum R φ S) f = Finset.sum Finset.univ fun i => LinearMap.comp (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 = 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)] [Finite ι] [DecidableEq ι] [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)] [Finite ι] [DecidableEq ι] [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' {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [Finite ι] [DecidableEq ι] [AddCommMonoid M] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} (h : ∀ (i : ι), LinearMap.comp f (LinearMap.single i) = LinearMap.comp g (LinearMap.single i)) :
            f = g

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

            theorem LinearMap.pi_ext'_iff {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [Finite ι] [DecidableEq ι] [AddCommMonoid M] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} :
            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) :
            { x // x ⨅ (i : ι) (_ : i J), 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
                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
                • One or more equations did not get rendered due to their size.
                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 ∀ (i : ι), i Ix 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) = Set.pi I 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 : ∀ (i : ι), i sp 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)} :
                  ⨅ (i : ι) (_ : i I), 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 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) :
                    @[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) :
                    @[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)
                    @[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.symm (LinearEquiv.piCongrLeft' R φ e)) a a_1 = (_ : e.symm (e a_1) = a_1)a (e a_1)
                    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
                    • One or more equations did not get rendered due to their size.
                    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.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
                        • One or more equations did not get rendered due to their size.
                        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.symm (LinearEquiv.piRing R M ι S)) f) g = Finset.sum Finset.univ fun 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 : α) :
                              Prod.fst (αM) (βM) (↑(LinearEquiv.sumArrowLequivProdArrow α β R M) f) a = f (Sum.inl 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 : β) :
                              Prod.snd (αM) (βM) (↑(LinearEquiv.sumArrowLequivProdArrow α β R M) f) b = f (Sum.inr 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 : α) :
                              @[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 : β) :
                              @[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] :
                              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
                              • One or more equations did not get rendered due to their size.
                              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.symm (LinearEquiv.piFinTwo R M)) = fun p => Fin.cons p.fst (Fin.cons p.snd 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
                                • One or more equations did not get rendered due to their size.
                                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 => (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 => (f 0, f 1)
                                  @[simp]
                                  theorem LinearEquiv.finTwoArrow_symm_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :
                                  ↑(LinearEquiv.symm (LinearEquiv.finTwoArrow R M)) = fun x => ![x.fst, x.snd]
                                  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
                                  • One or more equations did not get rendered due to their size.
                                  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
                                    • One or more equations did not get rendered due to their size.
                                    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
                                      • One or more equations did not get rendered due to their size.
                                      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 (Nat.succ n)M₂

                                        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
                                        • One or more equations did not get rendered due to their size.
                                        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) :
                                          ↑(LinearMap.vecCons f 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
                                          • One or more equations did not get rendered due to their size.
                                          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) :
                                            ↑(LinearMap.vecCons₂ f g) m = LinearMap.vecCons (f m) (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 (Nat.succ n)M₃

                                            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
                                            • One or more equations did not get rendered due to their size.
                                            Instances For