Documentation

Mathlib.LinearAlgebra.Contraction

Contractions #

Given modules $M, N$ over a commutative ring $R$, this file defines the natural linear maps: $M^* \otimes M \to R$, $M \otimes M^* \to R$, and $M^* \otimes N → Hom(M, N)$, as well as proving some basic properties of these maps.

Tags #

contraction, dual module, tensor product

noncomputable def contractLeft (R : Type u) (M : Type v₁) [CommSemiring R] [AddCommMonoid M] [Module R M] :

The natural left-handed pairing between a module and its dual.

Equations
Instances For
    noncomputable def contractRight (R : Type u) (M : Type v₁) [CommSemiring R] [AddCommMonoid M] [Module R M] :

    The natural right-handed pairing between a module and its dual.

    Equations
    Instances For
      noncomputable def dualTensorHom (R : Type u) (M : Type v₁) (N : Type v₂) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

      The natural map associating a linear map to the tensor product of two modules.

      Equations
      Instances For
        @[simp]
        theorem contractLeft_apply {R : Type u} {M : Type v₁} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) :
        (contractLeft R M) (f ⊗ₜ[R] m) = f m
        @[simp]
        theorem contractRight_apply {R : Type u} {M : Type v₁} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) :
        (contractRight R M) (m ⊗ₜ[R] f) = f m
        @[simp]
        theorem dualTensorHom_apply {R : Type u} {M : Type v₁} {N : Type v₂} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : Module.Dual R M) (m : M) (n : N) :
        ((dualTensorHom R M N) (f ⊗ₜ[R] n)) m = f m n
        @[simp]
        theorem transpose_dualTensorHom {R : Type u} {M : Type v₁} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) :
        Module.Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m)) = (dualTensorHom R (Module.Dual R M) (Module.Dual R M)) ((Module.Dual.eval R M) m ⊗ₜ[R] f)
        @[simp]
        theorem dualTensorHom_prodMap_zero {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) :
        ((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 = (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ LinearMap.fst R M N) ⊗ₜ[R] (LinearMap.inl R P Q) p)
        @[simp]
        theorem zero_prodMap_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : Module.Dual R N) (q : Q) :
        LinearMap.prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ LinearMap.snd R M N) ⊗ₜ[R] (LinearMap.inr R P Q) q)
        theorem map_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) (g : Module.Dual R N) (q : Q) :
        @[simp]
        theorem comp_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : Module.Dual R M) (n : N) (g : Module.Dual R N) (p : P) :
        (dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n) = g n (dualTensorHom R M P) (f ⊗ₜ[R] p)
        theorem toMatrix_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {m : Type u_1} {n : Type u_2} [Fintype m] [Finite n] [DecidableEq m] [DecidableEq n] (bM : Basis m R M) (bN : Basis n R N) (j : m) (i : n) :
        (LinearMap.toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.stdBasisMatrix i j 1

        As a matrix, dualTensorHom evaluated on a basis element of M* ⊗ N is a matrix with a single one and zeros elsewhere

        noncomputable def dualTensorHomEquivOfBasis {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) :

        If M is free, the natural linear map $M^* ⊗ N → Hom(M, N)$ is an equivalence. This function provides this equivalence in return for a basis of M.

        Equations
        Instances For
          @[simp]
          theorem dualTensorHomEquivOfBasis_apply {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) :
          @[simp]
          theorem dualTensorHomEquivOfBasis_toLinearMap {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) :
          @[simp]
          theorem dualTensorHomEquivOfBasis_symm_cancel_left {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) :
          @[simp]
          theorem dualTensorHomEquivOfBasis_symm_cancel_right {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (x : M →ₗ[R] N) :
          noncomputable def dualTensorHomEquiv (R : Type u) (M : Type v₁) (N : Type v₂) [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Free R M] [Module.Finite R M] :

          If M is finite free, the natural map $M^* ⊗ N → Hom(M, N)$ is an equivalence.

          Equations
          Instances For
            noncomputable def lTensorHomEquivHomLTensor (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] :

            When M is a finite free module, the map lTensorHomToHomLTensor is an equivalence. Note that lTensorHomEquivHomLTensor is not defined directly in terms of lTensorHomToHomLTensor, but the equivalence between the two is given by lTensorHomEquivHomLTensor_toLinearMap and lTensorHomEquivHomLTensor_apply.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def rTensorHomEquivHomRTensor (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] :

              When M is a finite free module, the map rTensorHomToHomRTensor is an equivalence. Note that rTensorHomEquivHomRTensor is not defined directly in terms of rTensorHomToHomRTensor, but the equivalence between the two is given by rTensorHomEquivHomRTensor_toLinearMap and rTensorHomEquivHomRTensor_apply.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                @[simp]
                @[simp]
                theorem lTensorHomEquivHomLTensor_apply {R : Type u} {M : Type v₁} {P : Type v₃} {Q : Type v₄} [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] (x : TensorProduct R P (M →ₗ[R] Q)) :
                @[simp]
                theorem rTensorHomEquivHomRTensor_apply {R : Type u} {M : Type v₁} {P : Type v₃} {Q : Type v₄} [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] (x : TensorProduct R (M →ₗ[R] P) Q) :
                noncomputable def homTensorHomEquiv (R : Type u) (M : Type v₁) (N : Type v₂) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] :

                When M and N are free R modules, the map homTensorHomMap is an equivalence. Note that homTensorHomEquiv is not defined directly in terms of homTensorHomMap, but the equivalence between the two is given by homTensorHomEquiv_toLinearMap and homTensorHomEquiv_apply.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem homTensorHomEquiv_toLinearMap (R : Type u) (M : Type v₁) (N : Type v₂) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] :
                  @[simp]
                  theorem homTensorHomEquiv_apply {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] (x : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q)) :