Documentation

Mathlib.LinearAlgebra.TensorProduct.Tower

The A-module structure on M โŠ—[R] N #

When M is both an R-module and an A-module, and Algebra R A, then many of the morphisms preserve the actions by A.

The Module instance itself is provided elsewhere as TensorProduct.leftModule. This file provides more general versions of the definitions already in LinearAlgebra/TensorProduct.

In this file, we use the convention that M, N, P, Q are all R-modules, but only M and P are simultaneously A-modules.

Main definitions #

Implementation notes #

We could thus consider replacing the less general definitions with these ones. If we do this, we probably should still implement the less general ones as abbreviations to the more general ones with fewer type arguments.

source
๐Ÿ“ coverage
theorem TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (a : A) (x : TensorProduct R M N) :
a โ€ข x = (LinearMap.rTensor N ((Algebra.lsmul R R M) a)) x
source
๐Ÿ”ธ coverage
def TensorProduct.AlgebraTensorModule.curry {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : TensorProduct R M N โ†’โ‚—[A] P) :
M โ†’โ‚—[A] N โ†’โ‚—[R] P

Heterobasic version of TensorProduct.curry:

Given a linear map M โŠ—[R] N โ†’[A] P, compose it with the canonical bilinear map M โ†’[A] N โ†’[R] M โŠ—[R] N to form a bilinear map M โ†’[A] N โ†’[R] P.

Instances For
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem TensorProduct.AlgebraTensorModule.curry_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : TensorProduct R M N โ†’โ‚—[A] P) (a : M) :
    (curry f) a = (TensorProduct.curry (โ†‘R f)) a
    source
    ๐Ÿ“ coverage
    theorem TensorProduct.AlgebraTensorModule.restrictScalars_curry {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : TensorProduct R M N โ†’โ‚—[A] P) :
    โ†‘R (curry f) = TensorProduct.curry (โ†‘R f)
    source
    ๐Ÿ“ coverage
    theorem TensorProduct.AlgebraTensorModule.curry_injective {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] :
    Function.Injective curry

    Just as TensorProduct.ext is marked ext instead of TensorProduct.ext', this is a better ext lemma than TensorProduct.AlgebraTensorModule.ext below.

    See note [partially-applied ext lemmas].

    source
    ๐Ÿ“ coverage
    theorem TensorProduct.AlgebraTensorModule.curry_injective_iff {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] {aโ‚ aโ‚‚ : TensorProduct R M N โ†’โ‚—[A] P} :
    aโ‚ = aโ‚‚ โ†” curry aโ‚ = curry aโ‚‚
    source
    theorem TensorProduct.AlgebraTensorModule.ext {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] {g h : TensorProduct R M N โ†’โ‚—[A] P} (H : โˆ€ (x : M) (y : N), g (x โŠ—โ‚œ[R] y) = h (x โŠ—โ‚œ[R] y)) :
    g = h
    source
    ๐Ÿ”ธ coverage
    def TensorProduct.AlgebraTensorModule.lift {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M โ†’โ‚—[A] N โ†’โ‚—[R] P) :
    TensorProduct R M N โ†’โ‚—[A] P

    Heterobasic version of TensorProduct.lift:

    Constructing a linear map M โŠ—[R] N โ†’[A] P given a bilinear map M โ†’[A] N โ†’[R] P with the property that its composition with the canonical bilinear map M โ†’[A] N โ†’[R] M โŠ—[R] N is the given bilinear map M โ†’[A] N โ†’[R] P.

    Instances For
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem TensorProduct.AlgebraTensorModule.lift_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M โ†’โ‚—[A] N โ†’โ‚—[R] P) (a : TensorProduct R M N) :
      (lift f) a = (TensorProduct.lift (โ†‘R f)) a
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem TensorProduct.AlgebraTensorModule.lift_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M โ†’โ‚—[A] N โ†’โ‚—[R] P) (x : M) (y : N) :
      (lift f) (x โŠ—โ‚œ[R] y) = (f x) y
      source
      ๐Ÿ”ธ coverage
      def TensorProduct.AlgebraTensorModule.uncurry (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] :
      (M โ†’โ‚—[A] N โ†’โ‚—[R] P) โ†’โ‚—[B] TensorProduct R M N โ†’โ‚—[A] P

      Heterobasic version of TensorProduct.uncurry:

      Linearly constructing a linear map M โŠ—[R] N โ†’[A] P given a bilinear map M โ†’[A] N โ†’[R] P with the property that its composition with the canonical bilinear map M โ†’[A] N โ†’[R] M โŠ—[R] N is the given bilinear map M โ†’[A] N โ†’[R] P.

      Instances For
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem TensorProduct.AlgebraTensorModule.uncurry_apply (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M โ†’โ‚—[A] N โ†’โ‚—[R] P) :
        (uncurry R A B M N P) f = lift f
        source
        ๐Ÿ”ธ coverage
        def TensorProduct.AlgebraTensorModule.lcurry (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] :
        (TensorProduct R M N โ†’โ‚—[A] P) โ†’โ‚—[B] M โ†’โ‚—[A] N โ†’โ‚—[R] P

        Heterobasic version of TensorProduct.lcurry:

        Given a linear map M โŠ—[R] N โ†’[A] P, compose it with the canonical bilinear map M โ†’[A] N โ†’[R] M โŠ—[R] N to form a bilinear map M โ†’[A] N โ†’[R] P.

        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem TensorProduct.AlgebraTensorModule.lcurry_apply (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : TensorProduct R M N โ†’โ‚—[A] P) :
          (lcurry R A B M N P) f = curry f
          source
          ๐Ÿ”ธ coverage
          def TensorProduct.AlgebraTensorModule.lift.equiv (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] :
          (M โ†’โ‚—[A] N โ†’โ‚—[R] P) โ‰ƒโ‚—[B] TensorProduct R M N โ†’โ‚—[A] P

          Heterobasic version of TensorProduct.lift.equiv:

          A linear equivalence constructing a linear map M โŠ—[R] N โ†’[A] P given a bilinear map M โ†’[A] N โ†’[R] P with the property that its composition with the canonical bilinear map M โ†’[A] N โ†’[R] M โŠ—[R] N is the given bilinear map M โ†’[A] N โ†’[R] P.

          Instances For
            source
            ๐Ÿ”ธ coverage
            def TensorProduct.AlgebraTensorModule.mk (R : Type uR) [CommSemiring R] (A : Type u_1) (M : Type u_2) (N : Type u_3) [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [SMulCommClass R A M] [AddCommMonoid N] [Module R N] :
            M โ†’โ‚—[A] N โ†’โ‚—[R] TensorProduct R M N

            Heterobasic version of TensorProduct.mk:

            The canonical bilinear map M โ†’[A] N โ†’[R] M โŠ—[R] N.

            Instances For
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem TensorProduct.AlgebraTensorModule.mk_apply (R : Type uR) [CommSemiring R] (A : Type u_1) (M : Type u_2) (N : Type u_3) [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [SMulCommClass R A M] [AddCommMonoid N] [Module R N] (m : M) :
              (mk R A M N) m = { toFun := fun (x2 : N) => m โŠ—โ‚œ[R] x2, map_add' := โ‹ฏ, map_smul' := โ‹ฏ }
              source
              ๐Ÿ”ธ coverage
              def TensorProduct.AlgebraTensorModule.map {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M โ†’โ‚—[A] P) (g : N โ†’โ‚—[R] Q) :
              TensorProduct R M N โ†’โ‚—[A] TensorProduct R P Q

              Heterobasic version of TensorProduct.map

              Instances For
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem TensorProduct.AlgebraTensorModule.map_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M โ†’โ‚—[A] P) (g : N โ†’โ‚—[R] Q) (m : M) (n : N) :
                (map f g) (m โŠ—โ‚œ[R] n) = f m โŠ—โ‚œ[R] g n
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem TensorProduct.AlgebraTensorModule.map_id {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                map LinearMap.id LinearMap.id = LinearMap.id
                source
                ๐Ÿ“ coverage
                theorem TensorProduct.AlgebraTensorModule.map_comp {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] [AddCommMonoid Q'] [Module R Q'] (fโ‚‚ : P โ†’โ‚—[A] P') (fโ‚ : M โ†’โ‚—[A] P) (gโ‚‚ : Q โ†’โ‚—[R] Q') (gโ‚ : N โ†’โ‚—[R] Q) :
                map (fโ‚‚ โˆ˜โ‚— fโ‚) (gโ‚‚ โˆ˜โ‚— gโ‚) = map fโ‚‚ gโ‚‚ โˆ˜โ‚— map fโ‚ gโ‚
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem TensorProduct.AlgebraTensorModule.map_one {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                map 1 1 = 1
                source
                ๐Ÿ“ coverage
                theorem TensorProduct.AlgebraTensorModule.map_mul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (fโ‚ fโ‚‚ : M โ†’โ‚—[A] M) (gโ‚ gโ‚‚ : N โ†’โ‚—[R] N) :
                map (fโ‚ * fโ‚‚) (gโ‚ * gโ‚‚) = map fโ‚ gโ‚ * map fโ‚‚ gโ‚‚
                source
                ๐Ÿ“ coverage
                theorem TensorProduct.AlgebraTensorModule.map_add_left {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (fโ‚ fโ‚‚ : M โ†’โ‚—[A] P) (g : N โ†’โ‚—[R] Q) :
                map (fโ‚ + fโ‚‚) g = map fโ‚ g + map fโ‚‚ g
                source
                ๐Ÿ“ coverage
                theorem TensorProduct.AlgebraTensorModule.map_add_right {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M โ†’โ‚—[A] P) (gโ‚ gโ‚‚ : N โ†’โ‚—[R] Q) :
                map f (gโ‚ + gโ‚‚) = map f gโ‚ + map f gโ‚‚
                source
                ๐Ÿ“ coverage
                theorem TensorProduct.AlgebraTensorModule.map_smul_right {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (r : R) (f : M โ†’โ‚—[A] P) (g : N โ†’โ‚—[R] Q) :
                map f (r โ€ข g) = r โ€ข map f g
                source
                ๐Ÿ“ coverage
                theorem TensorProduct.AlgebraTensorModule.map_smul_left {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (b : B) (f : M โ†’โ‚—[A] P) (g : N โ†’โ‚—[R] Q) :
                map (b โ€ข f) g = b โ€ข map f g
                source
                ๐Ÿ“ coverage
                theorem TensorProduct.AlgebraTensorModule.map_eq {R : Type uR} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] (f : M โ†’โ‚—[R] P) (g : N โ†’โ‚—[R] Q) :
                map f g = TensorProduct.map f g

                The heterobasic version of map coincides with the regular version.

                source
                ๐Ÿ”ธ coverage
                def TensorProduct.AlgebraTensorModule.lTensor {R : Type uR} (A : Type uA) (M : Type uM) {N : Type uN} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] :
                (N โ†’โ‚—[R] Q) โ†’โ‚—[R] TensorProduct R M N โ†’โ‚—[A] TensorProduct R M Q

                Heterobasic version of LinearMap.lTensor

                Instances For
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem TensorProduct.AlgebraTensorModule.coe_lTensor {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] (f : N โ†’โ‚—[R] Q) :
                  โ‡‘((lTensor A M) f) = โ‡‘(LinearMap.lTensor M f)
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem TensorProduct.AlgebraTensorModule.restrictScalars_lTensor {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] (f : N โ†’โ‚—[R] Q) :
                  โ†‘R ((lTensor A M) f) = LinearMap.lTensor M f
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem TensorProduct.AlgebraTensorModule.lTensor_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] (f : N โ†’โ‚—[R] Q) (m : M) (n : N) :
                  ((lTensor A M) f) (m โŠ—โ‚œ[R] n) = m โŠ—โ‚œ[R] f n
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem TensorProduct.AlgebraTensorModule.lTensor_id {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                  (lTensor A M) LinearMap.id = LinearMap.id
                  source
                  ๐Ÿ“ coverage
                  theorem TensorProduct.AlgebraTensorModule.lTensor_comp {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} {Q' : Type uQ'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] [AddCommMonoid Q'] [Module R Q'] (fโ‚‚ : Q โ†’โ‚—[R] Q') (fโ‚ : N โ†’โ‚—[R] Q) :
                  (lTensor A M) (fโ‚‚ โˆ˜โ‚— fโ‚) = (lTensor A M) fโ‚‚ โˆ˜โ‚— (lTensor A M) fโ‚
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem TensorProduct.AlgebraTensorModule.lTensor_one {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                  (lTensor A M) 1 = 1
                  source
                  ๐Ÿ“ coverage
                  theorem TensorProduct.AlgebraTensorModule.lTensor_mul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (fโ‚ fโ‚‚ : N โ†’โ‚—[R] N) :
                  (lTensor A M) (fโ‚ * fโ‚‚) = (lTensor A M) fโ‚ * (lTensor A M) fโ‚‚
                  source
                  ๐Ÿ”ธ coverage
                  def TensorProduct.AlgebraTensorModule.rTensor (R : Type uR) {A : Type uA} {M : Type uM} (N : Type uN) {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] :
                  (M โ†’โ‚—[A] P) โ†’โ‚—[R] TensorProduct R M N โ†’โ‚—[A] TensorProduct R P N

                  Heterobasic version of LinearMap.rTensor

                  Instances For
                    source
                    ๐Ÿ“ coverage
                    @[simp]
                    theorem TensorProduct.AlgebraTensorModule.coe_rTensor {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M โ†’โ‚—[A] P) :
                    โ‡‘((rTensor R N) f) = โ‡‘(LinearMap.rTensor N (โ†‘R f))
                    source
                    ๐Ÿ“ coverage
                    @[simp]
                    theorem TensorProduct.AlgebraTensorModule.restrictScalars_rTensor {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M โ†’โ‚—[A] P) :
                    โ†‘R ((rTensor R N) f) = LinearMap.rTensor N (โ†‘R f)
                    source
                    ๐Ÿ“ coverage
                    @[simp]
                    theorem TensorProduct.AlgebraTensorModule.rTensor_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M โ†’โ‚—[A] P) (m : M) (n : N) :
                    ((rTensor R N) f) (m โŠ—โ‚œ[R] n) = f m โŠ—โ‚œ[R] n
                    source
                    ๐Ÿ“ coverage
                    @[simp]
                    theorem TensorProduct.AlgebraTensorModule.rTensor_id {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                    (rTensor R N) LinearMap.id = LinearMap.id
                    source
                    ๐Ÿ“ coverage
                    theorem TensorProduct.AlgebraTensorModule.rTensor_comp {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {P' : Type uP'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] (fโ‚‚ : P โ†’โ‚—[A] P') (fโ‚ : M โ†’โ‚—[A] P) :
                    (rTensor R N) (fโ‚‚ โˆ˜โ‚— fโ‚) = (rTensor R N) fโ‚‚ โˆ˜โ‚— (rTensor R N) fโ‚
                    source
                    ๐Ÿ“ coverage
                    @[simp]
                    theorem TensorProduct.AlgebraTensorModule.rTensor_one {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                    (rTensor R N) 1 = 1
                    source
                    ๐Ÿ“ coverage
                    theorem TensorProduct.AlgebraTensorModule.rTensor_mul {R : Type uR} {A : Type uA} {M : Type uM} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (fโ‚ fโ‚‚ : M โ†’โ‚—[A] M) :
                    (rTensor R M) (fโ‚ * fโ‚‚) = (rTensor R M) fโ‚ * (rTensor R M) fโ‚‚
                    source
                    ๐Ÿ”ธ coverage
                    def TensorProduct.AlgebraTensorModule.mapBilinear (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] :
                    (M โ†’โ‚—[A] P) โ†’โ‚—[B] (N โ†’โ‚—[R] Q) โ†’โ‚—[R] TensorProduct R M N โ†’โ‚—[A] TensorProduct R P Q

                    Heterobasic version of TensorProduct.map_bilinear

                    Instances For
                      source
                      ๐Ÿ“ coverage
                      @[simp]
                      theorem TensorProduct.AlgebraTensorModule.mapBilinear_apply {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M โ†’โ‚—[A] P) (g : N โ†’โ‚—[R] Q) :
                      ((mapBilinear R A B M N P Q) f) g = map f g
                      source
                      ๐Ÿ”ธ coverage
                      def TensorProduct.AlgebraTensorModule.homTensorHomMap (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] :
                      TensorProduct R (M โ†’โ‚—[A] P) (N โ†’โ‚—[R] Q) โ†’โ‚—[B] TensorProduct R M N โ†’โ‚—[A] TensorProduct R P Q

                      Heterobasic version of TensorProduct.homTensorHomMap

                      Instances For
                        source
                        ๐Ÿ“ coverage
                        @[simp]
                        theorem TensorProduct.AlgebraTensorModule.homTensorHomMap_apply {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M โ†’โ‚—[A] P) (g : N โ†’โ‚—[R] Q) :
                        (homTensorHomMap R A B M N P Q) (f โŠ—โ‚œ[R] g) = map f g
                        source
                        ๐Ÿ”ธ coverage
                        def TensorProduct.AlgebraTensorModule.congr {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M โ‰ƒโ‚—[A] P) (g : N โ‰ƒโ‚—[R] Q) :
                        TensorProduct R M N โ‰ƒโ‚—[A] TensorProduct R P Q

                        Heterobasic version of TensorProduct.congr

                        Instances For
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem TensorProduct.AlgebraTensorModule.congr_refl {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                          congr (LinearEquiv.refl A M) (LinearEquiv.refl R N) = LinearEquiv.refl A (TensorProduct R M N)
                          source
                          ๐Ÿ“ coverage
                          theorem TensorProduct.AlgebraTensorModule.congr_trans {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] [AddCommMonoid Q'] [Module R Q'] (fโ‚ : M โ‰ƒโ‚—[A] P) (fโ‚‚ : P โ‰ƒโ‚—[A] P') (gโ‚ : N โ‰ƒโ‚—[R] Q) (gโ‚‚ : Q โ‰ƒโ‚—[R] Q') :
                          congr (fโ‚ โ‰ชโ‰ซโ‚— fโ‚‚) (gโ‚ โ‰ชโ‰ซโ‚— gโ‚‚) = congr fโ‚ gโ‚ โ‰ชโ‰ซโ‚— congr fโ‚‚ gโ‚‚
                          source
                          ๐Ÿ“ coverage
                          theorem TensorProduct.AlgebraTensorModule.congr_symm {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M โ‰ƒโ‚—[A] P) (g : N โ‰ƒโ‚—[R] Q) :
                          congr f.symm g.symm = (congr f g).symm
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem TensorProduct.AlgebraTensorModule.congr_one {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                          congr 1 1 = 1
                          source
                          ๐Ÿ“ coverage
                          theorem TensorProduct.AlgebraTensorModule.congr_mul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (fโ‚ fโ‚‚ : M โ‰ƒโ‚—[A] M) (gโ‚ gโ‚‚ : N โ‰ƒโ‚—[R] N) :
                          congr (fโ‚ * fโ‚‚) (gโ‚ * gโ‚‚) = congr fโ‚ gโ‚ * congr fโ‚‚ gโ‚‚
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem TensorProduct.AlgebraTensorModule.congr_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M โ‰ƒโ‚—[A] P) (g : N โ‰ƒโ‚—[R] Q) (m : M) (n : N) :
                          (congr f g) (m โŠ—โ‚œ[R] n) = f m โŠ—โ‚œ[R] g n
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem TensorProduct.AlgebraTensorModule.congr_symm_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M โ‰ƒโ‚—[A] P) (g : N โ‰ƒโ‚—[R] Q) (p : P) (q : Q) :
                          (congr f g).symm (p โŠ—โ‚œ[R] q) = f.symm p โŠ—โ‚œ[R] g.symm q
                          source
                          ๐Ÿ“ coverage
                          theorem TensorProduct.AlgebraTensorModule.congr_eq {R : Type uR} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] (f : M โ‰ƒโ‚—[R] P) (g : N โ‰ƒโ‚—[R] Q) :
                          congr f g = TensorProduct.congr f g
                          source
                          ๐Ÿ”ธ coverage
                          def TensorProduct.AlgebraTensorModule.rid (R : Type uR) (A : Type uA) (M : Type uM) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] :
                          TensorProduct R M R โ‰ƒโ‚—[A] M

                          Heterobasic version of TensorProduct.rid.

                          Instances For
                            source
                            ๐Ÿ“ coverage
                            theorem TensorProduct.AlgebraTensorModule.rid_eq_rid (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] :
                            AlgebraTensorModule.rid R R M = TensorProduct.rid R M

                            The heterobasic version of rid coincides with the regular version.

                            source
                            ๐Ÿ“ coverage
                            @[simp]
                            theorem TensorProduct.AlgebraTensorModule.rid_tmul {R : Type uR} (A : Type uA) {M : Type uM} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (r : R) (m : M) :
                            (AlgebraTensorModule.rid R A M) (m โŠ—โ‚œ[R] r) = r โ€ข m
                            source
                            ๐Ÿ“ coverage
                            @[simp]
                            theorem TensorProduct.AlgebraTensorModule.rid_symm_apply (R : Type uR) (A : Type uA) {M : Type uM} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (m : M) :
                            (AlgebraTensorModule.rid R A M).symm m = m โŠ—โ‚œ[R] 1
                            source
                            ๐Ÿ”ธ coverage
                            def TensorProduct.AlgebraTensorModule.assoc (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (P : Type uP) (Q : Type uQ) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] :
                            TensorProduct R (TensorProduct A M P) Q โ‰ƒโ‚—[B] TensorProduct A M (TensorProduct R P Q)

                            Heterobasic version of TensorProduct.assoc:

                            B-linear equivalence between (M โŠ—[A] P) โŠ—[R] Q and M โŠ—[A] (P โŠ—[R] Q).

                            Note this is especially useful with A = R (where it is a "more linear" version of TensorProduct.assoc), or with B = A.

                            Instances For
                              source
                              ๐Ÿ“ coverage
                              @[simp]
                              theorem TensorProduct.AlgebraTensorModule.assoc_tmul (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] (m : M) (p : P) (q : Q) :
                              (assoc R A B M P Q) (m โŠ—โ‚œ[A] p โŠ—โ‚œ[R] q) = m โŠ—โ‚œ[A] (p โŠ—โ‚œ[R] q)
                              source
                              ๐Ÿ“ coverage
                              @[simp]
                              theorem TensorProduct.AlgebraTensorModule.assoc_symm_tmul (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] (m : M) (p : P) (q : Q) :
                              (assoc R A B M P Q).symm (m โŠ—โ‚œ[A] (p โŠ—โ‚œ[R] q)) = m โŠ—โ‚œ[A] p โŠ—โ‚œ[R] q
                              source
                              ๐Ÿ“ coverage
                              theorem TensorProduct.AlgebraTensorModule.assoc_eq (R : Type uR) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] :
                              assoc R R R M P Q = TensorProduct.assoc R M P Q

                              The heterobasic version of assoc coincides with the regular version.

                              source
                              ๐Ÿ“ coverage
                              theorem TensorProduct.AlgebraTensorModule.rTensor_tensor (R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} {P : Type uP} (P' : Type uP') [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid P'] [Module A P'] [Module R P] [IsScalarTower R A P] [Module R P'] [IsScalarTower R A P'] (g : P โ†’โ‚—[A] P') :
                              LinearMap.rTensor (TensorProduct R M N) g = โ†‘(assoc R A A P' M N) โˆ˜โ‚— map (LinearMap.rTensor M g) LinearMap.id โˆ˜โ‚— โ†‘(assoc R A A P M N).symm
                              source
                              ๐Ÿ”ธ coverage
                              def TensorProduct.AlgebraTensorModule.cancelBaseChange (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [Algebra A B] [IsScalarTower A B M] :
                              TensorProduct A M (TensorProduct R A N) โ‰ƒโ‚—[B] TensorProduct R M N

                              B-linear equivalence between M โŠ—[A] (A โŠ—[R] N) and M โŠ—[R] N. In particular useful with B = A.

                              Instances For
                                source
                                ๐Ÿ”ธ coverage
                                def TensorProduct.AlgebraTensorModule.distribBaseChange (R : Type uR) (A : Type uA) (N : Type uN) (Q : Type uQ) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] :
                                TensorProduct R A (TensorProduct R N Q) โ‰ƒโ‚—[A] TensorProduct A (TensorProduct R A N) (TensorProduct R A Q)

                                Base change distributes over tensor product.

                                Instances For
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [Algebra A B] [IsScalarTower A B M] (m : M) (n : N) (a : A) :
                                  (cancelBaseChange R A B M N) (m โŠ—โ‚œ[A] (a โŠ—โ‚œ[R] n)) = (a โ€ข m) โŠ—โ‚œ[R] n
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [Algebra A B] [IsScalarTower A B M] (m : M) (n : N) :
                                  (cancelBaseChange R A B M N).symm (m โŠ—โ‚œ[R] n) = m โŠ—โ‚œ[A] (1 โŠ—โ‚œ[R] n)
                                  source
                                  ๐Ÿ“ coverage
                                  theorem TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] [Algebra A B] [IsScalarTower A B M] (f : N โ†’โ‚—[R] Q) :
                                  (lTensor B M) f โˆ˜โ‚— โ†‘(cancelBaseChange R A B M N) = โ†‘(cancelBaseChange R A B M Q) โˆ˜โ‚— (lTensor B M) ((lTensor A A) f)
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem TensorProduct.AlgebraTensorModule.distribBaseChange_tmul (R : Type uR) (A : Type uA) {N : Type uN} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] (n : N) (q : Q) (a : A) :
                                  (distribBaseChange R A N Q) (a โŠ—โ‚œ[R] (n โŠ—โ‚œ[R] q)) = a โŠ—โ‚œ[R] n โŠ—โ‚œ[A] (1 โŠ—โ‚œ[R] q)
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem TensorProduct.AlgebraTensorModule.distribBaseChange_symm_tmul (R : Type uR) (A : Type uA) {N : Type uN} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] (n : N) (q : Q) (a b : A) :
                                  (distribBaseChange R A N Q).symm (a โŠ—โ‚œ[R] n โŠ—โ‚œ[A] (b โŠ—โ‚œ[R] q)) = (a * b) โŠ—โ‚œ[R] (n โŠ—โ‚œ[R] q)
                                  source
                                  ๐Ÿ”ธ coverage
                                  def TensorProduct.AlgebraTensorModule.leftComm (R : Type uR) (A : Type uA) (M : Type uM) (P : Type uP) (Q : Type uQ) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] :
                                  TensorProduct A M (TensorProduct R P Q) โ‰ƒโ‚—[A] TensorProduct A P (TensorProduct R M Q)

                                  Heterobasic version of TensorProduct.leftComm

                                  Instances For
                                    source
                                    ๐Ÿ“ coverage
                                    @[simp]
                                    theorem TensorProduct.AlgebraTensorModule.leftComm_tmul (R : Type uR) (A : Type uA) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] (m : M) (p : P) (q : Q) :
                                    (leftComm R A M P Q) (m โŠ—โ‚œ[A] (p โŠ—โ‚œ[R] q)) = p โŠ—โ‚œ[A] (m โŠ—โ‚œ[R] q)
                                    source
                                    ๐Ÿ“ coverage
                                    @[simp]
                                    theorem TensorProduct.AlgebraTensorModule.leftComm_symm_tmul (R : Type uR) (A : Type uA) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] (m : M) (p : P) (q : Q) :
                                    (leftComm R A M P Q).symm (p โŠ—โ‚œ[A] (m โŠ—โ‚œ[R] q)) = m โŠ—โ‚œ[A] (p โŠ—โ‚œ[R] q)
                                    source
                                    ๐Ÿ“ coverage
                                    theorem TensorProduct.AlgebraTensorModule.leftComm_eq (R : Type uR) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] :
                                    leftComm R R M P Q = TensorProduct.leftComm R M P Q

                                    The heterobasic version of leftComm coincides with the regular version.

                                    source
                                    ๐Ÿ”ธ coverage
                                    def TensorProduct.AlgebraTensorModule.rightComm (R : Type uR) (S : Type uS) (B : Type uB) (M : Type uM) (P : Type uP) (Q : Type uQ) [CommSemiring R] [Semiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [Module B M] [IsScalarTower R B M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [CommSemiring S] [Module S M] [Module S P] [Algebra S B] [IsScalarTower S B M] [SMulCommClass R S M] [SMulCommClass S R M] :
                                    TensorProduct R (TensorProduct S M P) Q โ‰ƒโ‚—[B] TensorProduct S (TensorProduct R M Q) P

                                    A tensor product analogue of mul_right_comm.

                                    Suppose we have a diagram of algebras R โ†’ B โ† S, and a B-module M, S-module P, R-module Q, then

                                    (M โŠ—หข P)      โŽ› M โŽž โŠ—หข P
 โŠ—แดฟ       โ‰…แดฎ  โŽœ โŠ—แดฟโŽŸ
 Q            โŽ Q โŽ 
                                    Instances For
                                      source
                                      ๐Ÿ“ coverage
                                      @[simp]
                                      theorem TensorProduct.AlgebraTensorModule.rightComm_tmul (R : Type uR) {S : Type uS} (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [Module B M] [IsScalarTower R B M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [CommSemiring S] [Module S M] [Module S P] [Algebra S B] [IsScalarTower S B M] [SMulCommClass R S M] [SMulCommClass S R M] (m : M) (p : P) (q : Q) :
                                      (rightComm R S B M P Q) (m โŠ—โ‚œ[S] p โŠ—โ‚œ[R] q) = m โŠ—โ‚œ[R] q โŠ—โ‚œ[S] p
                                      source
                                      ๐Ÿ“ coverage
                                      @[simp]
                                      theorem TensorProduct.AlgebraTensorModule.rightComm_symm (R : Type uR) {S : Type uS} (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [Module B M] [IsScalarTower R B M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [CommSemiring S] [Module S M] [Module S P] [Algebra S B] [IsScalarTower S B M] [SMulCommClass R S M] [SMulCommClass S R M] :
                                      (rightComm R S B M P Q).symm = rightComm S R B M Q P
                                      source
                                      ๐Ÿ“ coverage
                                      theorem TensorProduct.AlgebraTensorModule.rightComm_symm_tmul (R : Type uR) {S : Type uS} (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [Module B M] [IsScalarTower R B M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [CommSemiring S] [Module S M] [Module S P] [Algebra S B] [IsScalarTower S B M] [SMulCommClass R S M] [SMulCommClass S R M] (m : M) (p : P) (q : Q) :
                                      (rightComm R S B M P Q).symm (m โŠ—โ‚œ[R] q โŠ—โ‚œ[S] p) = m โŠ—โ‚œ[S] p โŠ—โ‚œ[R] q
                                      source
                                      ๐Ÿ“ coverage
                                      theorem TensorProduct.AlgebraTensorModule.rightComm_eq (R : Type uR) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] :
                                      rightComm R R R M P Q = TensorProduct.rightComm R M P Q

                                      The heterobasic version of leftComm coincides with the regular version.

                                      source
                                      ๐Ÿ”ธ coverage
                                      def TensorProduct.AlgebraTensorModule.tensorTensorTensorComm (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] [CommSemiring S] [Algebra R S] [Algebra S B] [Module S M] [Module S N] [IsScalarTower R S M] [SMulCommClass A S M] [SMulCommClass S A M] [IsScalarTower S B M] [IsScalarTower R S N] :
                                      TensorProduct A (TensorProduct S M N) (TensorProduct R P Q) โ‰ƒโ‚—[B] TensorProduct S (TensorProduct A M P) (TensorProduct R N Q)

                                      Heterobasic version of tensorTensorTensorComm.

                                      Suppose we have towers of algebras R โ†’ S โ†’ B and R โ†’ A โ†’ B, and a B-module M, S-module N, A-module P, R-module Q, then

                                      (M โŠ—หข N)      โŽ› M โŽž โŠ—หข โŽ› N โŽž
 โŠ—แดฌ       โ‰…แดฎ  โŽœ โŠ—แดฌโŽŸ    โŽœ โŠ—แดฟโŽŸ
(P โŠ—แดฟ Q)      โŽ P โŽ     โŽ Q โŽ 
                                      Instances For
                                        source
                                        ๐Ÿ“ coverage
                                        @[simp]
                                        theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] [CommSemiring S] [Algebra R S] [Algebra S B] [Module S M] [Module S N] [IsScalarTower R S M] [SMulCommClass A S M] [SMulCommClass S A M] [IsScalarTower S B M] [IsScalarTower R S N] (m : M) (n : N) (p : P) (q : Q) :
                                        (tensorTensorTensorComm R S A B M N P Q) (m โŠ—โ‚œ[S] n โŠ—โ‚œ[A] (p โŠ—โ‚œ[R] q)) = m โŠ—โ‚œ[A] p โŠ—โ‚œ[S] (n โŠ—โ‚œ[R] q)
                                        source
                                        ๐Ÿ“ coverage
                                        @[simp]
                                        theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] [CommSemiring S] [Algebra R S] [Algebra S B] [Module S M] [Module S N] [IsScalarTower R S M] [SMulCommClass A S M] [SMulCommClass S A M] [IsScalarTower S B M] [IsScalarTower R S N] :
                                        (tensorTensorTensorComm R S A B M N P Q).symm = tensorTensorTensorComm R A S B M P N Q
                                        source
                                        ๐Ÿ“ coverage
                                        theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] [CommSemiring S] [Algebra R S] [Algebra S B] [Module S M] [Module S N] [IsScalarTower R S M] [SMulCommClass A S M] [SMulCommClass S A M] [IsScalarTower S B M] [IsScalarTower R S N] (m : M) (n : N) (p : P) (q : Q) :
                                        (tensorTensorTensorComm R S A B M N P Q).symm (m โŠ—โ‚œ[A] p โŠ—โ‚œ[S] (n โŠ—โ‚œ[R] q)) = m โŠ—โ‚œ[S] n โŠ—โ‚œ[A] (p โŠ—โ‚œ[R] q)
                                        source
                                        ๐Ÿ“ coverage
                                        theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq (R : Type uR) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] :
                                        tensorTensorTensorComm R R R R M N P Q = TensorProduct.tensorTensorTensorComm R M N P Q

                                        The heterobasic version of tensorTensorTensorComm coincides with the regular version.

                                        The base-change of a linear map of R-modules to a linear map of A-modules #

                                        source
                                        ๐Ÿ”ธ coverage
                                        def LinearMap.baseChange {R : Type u_1} (A : Type u_2) {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M โ†’โ‚—[R] N) :
                                        TensorProduct R A M โ†’โ‚—[A] TensorProduct R A N

                                        baseChange A f for f : M โ†’โ‚—[R] N is the A-linear map A โŠ—[R] M โ†’โ‚—[A] A โŠ—[R] N.

                                        This "base change" operation is also known as "extension of scalars".

                                        Instances For
                                          source
                                          ๐Ÿ“ coverage
                                          @[simp]
                                          theorem LinearMap.baseChange_tmul {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M โ†’โ‚—[R] N) (a : A) (x : M) :
                                          (baseChange A f) (a โŠ—โ‚œ[R] x) = a โŠ—โ‚œ[R] f x
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LinearMap.baseChange_eq_ltensor {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M โ†’โ‚—[R] N) :
                                          โ‡‘(baseChange A f) = โ‡‘(lTensor A f)
                                          source
                                          ๐Ÿ“ coverage
                                          @[simp]
                                          theorem LinearMap.baseChange_add {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : M โ†’โ‚—[R] N) :
                                          baseChange A (f + g) = baseChange A f + baseChange A g
                                          source
                                          ๐Ÿ“ coverage
                                          @[simp]
                                          theorem LinearMap.baseChange_zero {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                                          baseChange A 0 = 0
                                          source
                                          ๐Ÿ“ coverage
                                          @[simp]
                                          theorem LinearMap.baseChange_smul {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) (f : M โ†’โ‚—[R] N) :
                                          baseChange A (r โ€ข f) = r โ€ข baseChange A f
                                          source
                                          ๐Ÿ“ coverage
                                          @[simp]
                                          theorem LinearMap.baseChange_id {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
                                          baseChange A id = id
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LinearMap.baseChange_comp {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M โ†’โ‚—[R] N) (g : N โ†’โ‚—[R] P) :
                                          baseChange A (g โˆ˜โ‚— f) = baseChange A g โˆ˜โ‚— baseChange A f
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LinearMap.baseChange_baseChange {R : Type u_1} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {A : Type u_7} {B : Type u_8} [CommSemiring A] [Algebra R A] [Semiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (f : M โ†’โ‚—[R] N) :
                                          baseChange B (baseChange A f) = โ†‘(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B N).symm โˆ˜โ‚— baseChange B f โˆ˜โ‚— โ†‘(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M)
                                          source
                                          ๐Ÿ“ coverage
                                          @[simp]
                                          theorem LinearMap.baseChange_one (R : Type u_1) {A : Type u_2} (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
                                          baseChange A 1 = 1
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LinearMap.baseChange_mul {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f g : Module.End R M) :
                                          baseChange A (f * g) = baseChange A f * baseChange A g
                                          source
                                          ๐Ÿ”ธ coverage
                                          def LinearMap.baseChangeHom (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                                          (M โ†’โ‚—[R] N) โ†’โ‚—[R] TensorProduct R A M โ†’โ‚—[A] TensorProduct R A N

                                          baseChange as a linear map.

                                          When M = N, this is true more strongly as Module.End.baseChangeHom.

                                          Instances For
                                            source
                                            ๐Ÿ“ coverage
                                            @[simp]
                                            theorem LinearMap.baseChangeHom_apply (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M โ†’โ‚—[R] N) :
                                            (baseChangeHom R A M N) f = baseChange A f
                                            source
                                            ๐Ÿ”ธ coverage
                                            def Module.End.baseChangeHom (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
                                            End R M โ†’โ‚[R] End A (TensorProduct R A M)

                                            baseChange as an AlgHom.

                                            Instances For
                                              source
                                              ๐Ÿ“ coverage
                                              @[simp]
                                              theorem Module.End.baseChangeHom_apply_apply (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (a : End R M) (aโœ : TensorProduct R A M) :
                                              ((baseChangeHom R A M) a) aโœ = (TensorProduct.liftAux (โ†‘R { toFun := fun (h : M โ†’โ‚—[R] TensorProduct R A M) => h โˆ˜โ‚— a, map_add' := โ‹ฏ, map_smul' := โ‹ฏ } โˆ˜โ‚— โ†‘R (TensorProduct.AlgebraTensorModule.mk R A A M))) aโœ
                                              source
                                              ๐Ÿ“ coverage
                                              theorem LinearMap.baseChange_pow (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : Module.End R M) (n : โ„•) :
                                              baseChange A (f ^ n) = baseChange A f ^ n
                                              source
                                              ๐Ÿ”ธ coverage
                                              def LinearEquiv.baseChange (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (e : M โ‰ƒโ‚—[R] N) :
                                              TensorProduct R A M โ‰ƒโ‚—[A] TensorProduct R A N

                                              baseChange A e for e : M โ‰ƒโ‚—[R] N is the A-linear map A โŠ—[R] M โ‰ƒโ‚—[A] A โŠ—[R] N.

                                              Instances For
                                                source
                                                ๐Ÿ“ coverage
                                                @[simp]
                                                theorem LinearEquiv.coe_baseChange (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M โ‰ƒโ‚—[R] N) :
                                                โ†‘(baseChange R A M N f) = LinearMap.baseChange A โ†‘f
                                                source
                                                ๐Ÿ“ coverage
                                                @[simp]
                                                theorem LinearEquiv.baseChange_tmul (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {e : M โ‰ƒโ‚—[R] N} (a : A) (m : M) :
                                                (baseChange R A M N e) (a โŠ—โ‚œ[R] m) = a โŠ—โ‚œ[R] e m
                                                source
                                                ๐Ÿ“ coverage
                                                @[simp]
                                                theorem LinearEquiv.baseChange_symm_tmul (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {e : M โ‰ƒโ‚—[R] N} (a : A) (n : N) :
                                                (baseChange R A M N e).symm (a โŠ—โ‚œ[R] n) = a โŠ—โ‚œ[R] e.symm n
                                                source
                                                ๐Ÿ“ coverage
                                                @[simp]
                                                theorem LinearEquiv.baseChange_one (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
                                                baseChange R A M M 1 = 1
                                                source
                                                ๐Ÿ“ coverage
                                                theorem LinearEquiv.baseChange_trans (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) {P : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (e : M โ‰ƒโ‚—[R] N) (f : N โ‰ƒโ‚—[R] P) :
                                                baseChange R A M P (e โ‰ชโ‰ซโ‚— f) = baseChange R A M N e โ‰ชโ‰ซโ‚— baseChange R A N P f
                                                source
                                                ๐Ÿ“ coverage
                                                theorem LinearEquiv.baseChange_mul (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (e f : M โ‰ƒโ‚—[R] M) :
                                                baseChange R A M M (e * f) = baseChange R A M M e * baseChange R A M M f
                                                source
                                                ๐Ÿ“ coverage
                                                theorem LinearEquiv.baseChange_symm (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (e : M โ‰ƒโ‚—[R] N) :
                                                baseChange R A N M e.symm = (baseChange R A M N e).symm
                                                source
                                                ๐Ÿ“ coverage
                                                theorem LinearEquiv.baseChange_inv (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (e : M โ‰ƒโ‚—[R] M) :
                                                baseChange R A M M eโปยน = (baseChange R A M M e)โปยน
                                                source
                                                ๐Ÿ“ coverage
                                                theorem LinearEquiv.baseChange_pow (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M โ‰ƒโ‚—[R] M) (n : โ„•) :
                                                baseChange R A M M (f ^ n) = baseChange R A M M f ^ n
                                                source
                                                ๐Ÿ“ coverage
                                                theorem LinearEquiv.baseChange_zpow (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M โ‰ƒโ‚—[R] M) (n : โ„ค) :
                                                baseChange R A M M (f ^ n) = baseChange R A M M f ^ n
                                                source
                                                ๐Ÿ“ coverage
                                                theorem LinearMap.rTensor_baseChange {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (ฯ† : A โ†’โ‚[R] B) (t : TensorProduct R A M) (f : M โ†’โ‚—[R] N) :
                                                (rTensor N ฯ†.toLinearMap) ((baseChange A f) t) = (baseChange B f) ((rTensor M ฯ†.toLinearMap) t)
                                                source
                                                ๐Ÿ“ coverage
                                                @[simp]
                                                theorem LinearMap.baseChange_sub {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f g : M โ†’โ‚—[R] N) :
                                                baseChange A (f - g) = baseChange A f - baseChange A g
                                                source
                                                ๐Ÿ“ coverage
                                                @[simp]
                                                theorem LinearMap.baseChange_neg {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M โ†’โ‚—[R] N) :
                                                baseChange A (-f) = -baseChange A f
                                                source
                                                ๐Ÿ”ธ coverage
                                                def Submodule.baseChange {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
                                                Submodule A (TensorProduct R A M)

                                                If A is an R-algebra, any R-submodule p of an R-module M may be pushed forward to an A-submodule of A โŠ— M.

                                                This "base change" operation is also known as "extension of scalars".

                                                Instances For
                                                  source
                                                  ๐Ÿ“ coverage
                                                  theorem Submodule.tmul_mem_baseChange_of_mem {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] {p : Submodule R M} (a : A) {m : M} (hm : m โˆˆ p) :
                                                  a โŠ—โ‚œ[R] m โˆˆ baseChange A p
                                                  source
                                                  ๐Ÿ“ coverage
                                                  theorem Submodule.baseChange_eq_span {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
                                                  baseChange A p = span A โ†‘(map ((TensorProduct.mk R A M) 1) p)
                                                  source
                                                  ๐Ÿ“ coverage
                                                  @[simp]
                                                  theorem Submodule.baseChange_bot {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
                                                  baseChange A โŠฅ = โŠฅ
                                                  source
                                                  ๐Ÿ“ coverage
                                                  @[simp]
                                                  theorem Submodule.baseChange_top {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
                                                  baseChange A โŠค = โŠค
                                                  source
                                                  ๐Ÿ“ coverage
                                                  @[simp]
                                                  theorem Submodule.baseChange_span {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (s : Set M) :
                                                  baseChange A (span R s) = span A (โ‡‘((TensorProduct.mk R A M) 1) '' s)
                                                  source
                                                  ๐Ÿ”ธ coverage
                                                  def Submodule.toBaseChange {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
                                                  TensorProduct R A โ†ฅp โ†’โ‚—[A] โ†ฅ(baseChange A p)

                                                  Given an R-submodule p of M, and R-algebra A, we obtain an A-submodule of A โŠ—[R] M by p.baseChange A. This is then the surjective A-linear map A โŠ—[R] M โ†’ p.baseChange A.

                                                  Instances For
                                                    source
                                                    ๐Ÿ“ coverage
                                                    @[simp]
                                                    theorem Submodule.coe_toBaseChange_tmul {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) (a : A) (x : โ†ฅp) :
                                                    โ†‘((toBaseChange A p) (a โŠ—โ‚œ[R] x)) = a โŠ—โ‚œ[R] โ†‘x
                                                    source
                                                    ๐Ÿ“ coverage
                                                    theorem Submodule.toBaseChange_surjective {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
                                                    Function.Surjective โ‡‘(toBaseChange A p)
                                                    source
                                                    ๐Ÿ“ coverage
                                                    theorem Submodule.toBaseChange_surjective' {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) {y : TensorProduct R A M} (hy : y โˆˆ baseChange A p) :
                                                    โˆƒ (x : TensorProduct R A โ†ฅp), โ†‘((toBaseChange A p) x) = y

                                                    This version enables better pattern matching via the tactic obtain.