feat(linear_algebra/tensor_product): allow different semirings in linear_map.flip (#6414)

This also means the `map_*₂` lemmas are more generally applicable to linear_maps over different rings, such as `linear_map.prod_equiv.to_linear_map`.

To avoid breakage, this leaves `mk₂ R` for when R is commutative, and introduces `mk₂' R S` for when two different rings are wanted.

Author: eric-wieser

src/linear_algebra/tensor_product.lean

@@ -34,77 +34,112 @@ bilinear, tensor, tensor product
 
 namespace linear_map
 
-variables {R : Type*} [comm_semiring R]
-variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*} {S : Type*}
+section semiring
 
-variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q]
-  [add_comm_monoid S]
-variables [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] [semimodule R S]
+variables {R : Type*} [semiring R] {S : Type*} [semiring S]
+variables {M : Type*} {N : Type*} {P : Type*}
+variables {M' : Type*} {N' : Type*} {P' : Type*}
+
+variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
+variables [add_comm_group M'] [add_comm_group N'] [add_comm_group P']
+variables [semimodule R M] [semimodule S N] [semimodule R P] [semimodule S P]
+variables [semimodule R M'] [semimodule S N'] [semimodule R P'] [semimodule S P']
+variables [smul_comm_class S R P] [smul_comm_class S R P']
 include R
 
-variables (R)
-/-- Create a bilinear map from a function that is linear in each component. -/
-def mk₂ (f : M → N → P)
+variables (R S)
+/-- Create a bilinear map from a function that is linear in each component. 
+See `mk₂` for the special case where both arguments come from modules over the same ring. -/
+def mk₂' (f : M → N → P)
   (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
   (H2 : ∀ (c:R) m n, f (c • m) n = c • f m n)
   (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
-  (H4 : ∀ (c:R) m n, f m (c • n) = c • f m n) : M →ₗ N →ₗ P :=
+  (H4 : ∀ (c:S) m n, f m (c • n) = c • f m n) : M →ₗ[R] N →ₗ[S] P :=
 ⟨λ m, ⟨f m, H3 m, λ c, H4 c m⟩,
 λ m₁ m₂, linear_map.ext $ H1 m₁ m₂,
 λ c m, linear_map.ext $ H2 c m⟩
-variables {R}
+variables {R S}
 
-@[simp] theorem mk₂_apply
+@[simp] theorem mk₂'_apply
   (f : M → N → P) {H1 H2 H3 H4} (m : M) (n : N) :
-  (mk₂ R f H1 H2 H3 H4 : M →ₗ[R] N →ₗ P) m n = f m n := rfl
+  (mk₂' R S f H1 H2 H3 H4 : M →ₗ[R] N →ₗ[S] P) m n = f m n := rfl
 
-theorem ext₂ {f g : M →ₗ[R] N →ₗ[R] P}
+theorem ext₂ {f g : M →ₗ[R] N →ₗ[S] P}
   (H : ∀ m n, f m n = g m n) : f = g :=
 linear_map.ext (λ m, linear_map.ext $ λ n, H m n)
 
+section
+
+local attribute [instance] smul_comm_class.symm
+
 /-- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map from `M × N` to
 `P`, change the order of variables and get a linear map from `N` to linear maps from `M` to `P`. -/
-def flip (f : M →ₗ[R] N →ₗ[R] P) : N →ₗ M →ₗ P :=
-mk₂ R (λ n m, f m n)
+def flip (f : M →ₗ[R] N →ₗ[S] P) : N →ₗ[S] M →ₗ[R] P :=
+mk₂' S R (λ n m, f m n)
   (λ n₁ n₂ m, (f m).map_add _ _)
   (λ c n m, (f m).map_smul _ _)
   (λ n m₁ m₂, by rw f.map_add; refl)
   (λ c n m, by rw f.map_smul; refl)
 
-variable (f : M →ₗ[R] N →ₗ[R] P)
+end
 
-@[simp] theorem flip_apply (m : M) (n : N) : flip f n m = f m n := rfl
+@[simp] theorem flip_apply (f : M →ₗ[R] N →ₗ[S] P) (m : M) (n : N) : flip f n m = f m n := rfl
 
 variables {R}
-theorem flip_inj {f g : M →ₗ[R] N →ₗ P} (H : flip f = flip g) : f = g :=
+theorem flip_inj {f g : M →ₗ[R] N →ₗ[S] P} (H : flip f = flip g) : f = g :=
 ext₂ $ λ m n, show flip f n m = flip g n m, by rw H
 
+theorem map_zero₂ (f : M →ₗ[R] N →ₗ[S] P) (y) : f 0 y = 0 :=
+(flip f y).map_zero
+
+theorem map_neg₂ (f : M' →ₗ[R] N →ₗ[S] P') (x y) : f (-x) y = -f x y :=
+(flip f y).map_neg _
+
+theorem map_sub₂ (f : M' →ₗ[R] N →ₗ[S] P') (x y z) : f (x - y) z = f x z - f y z :=
+(flip f z).map_sub _ _
+
+theorem map_add₂ (f : M →ₗ[R] N →ₗ[S] P) (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y :=
+(flip f y).map_add _ _
+
+theorem map_smul₂ (f : M →ₗ[R] N →ₗ[S] P) (r : R) (x y) : f (r • x) y = r • f x y :=
+(flip f y).map_smul _ _
+
+end semiring
+
+section comm_semiring
+
+variables {R : Type*} [comm_semiring R]
+variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*}
+
+variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q]
+variables [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q]
+
+variables (R)
+
+/-- Create a bilinear map from a function that is linear in each component.
+
+This is a shorthand for `mk₂'` for the common case when `R = S`. -/
+def mk₂ (f : M → N → P)
+  (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
+  (H2 : ∀ (c:R) m n, f (c • m) n = c • f m n)
+  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
+  (H4 : ∀ (c:R) m n, f m (c • n) = c • f m n) : M →ₗ[R] N →ₗ[R] P :=
+mk₂' R R f H1 H2 H3 H4
+
+@[simp] theorem mk₂_apply
+  (f : M → N → P) {H1 H2 H3 H4} (m : M) (n : N) :
+  (mk₂ R f H1 H2 H3 H4 : M →ₗ[R] N →ₗ[R] P) m n = f m n := rfl
+
 variables (R M N P)
 /-- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map `M → N → P`,
 change the order of variables and get a linear map from `N` to linear maps from `M` to `P`. -/
-def lflip : (M →ₗ[R] N →ₗ P) →ₗ[R] N →ₗ M →ₗ P :=
+def lflip : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] N →ₗ[R] M →ₗ[R] P :=
 ⟨flip, λ _ _, rfl, λ _ _, rfl⟩
 variables {R M N P}
 
-@[simp] theorem lflip_apply (m : M) (n : N) : lflip R M N P f n m = f m n := rfl
-
-theorem map_zero₂ (y) : f 0 y = 0 := (flip f y).map_zero
-
-theorem map_neg₂ {R : Type*} [comm_semiring R] {M N P : Type*}
-  [add_comm_group M] [add_comm_monoid N] [add_comm_group P]
-  [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) (x y) :
-  f (-x) y = -f x y :=
-(flip f y).map_neg _
-
-theorem map_sub₂ {R : Type*} [comm_semiring R] {M N P : Type*}
-  [add_comm_group M] [add_comm_monoid N] [add_comm_group P]
-  [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) (x y z) :
-  f (x - y) z = f x z - f y z :=
-(flip f z).map_sub _ _
-
-theorem map_add₂ (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y := (flip f y).map_add _ _
+variables (f : M →ₗ[R] N →ₗ[R] P)
 
-theorem map_smul₂ (r:R) (x y) : f (r • x) y = r • f x y := (flip f y).map_smul _ _
+@[simp] theorem lflip_apply (m : M) (n : N) : lflip R M N P f n m = f m n := rfl
 
 variables (R P)
 /-- Composing a linear map `M → N` and a linear map `N → P` to form a linear map `M → P`. -/
@@ -121,7 +156,7 @@ variables (R M N P)
 def llcomp : (N →ₗ[R] P) →ₗ[R] (M →ₗ[R] N) →ₗ M →ₗ P :=
 flip ⟨lcomp R P,
   λ f f', ext₂ $ λ g x, g.map_add _ _,
-  λ c f, ext₂ $ λ g x, g.map_smul _ _⟩
+  λ (c : R) f, ext₂ $ λ g x, g.map_smul _ _⟩
 variables {R M N P}
 
 section
@@ -153,6 +188,8 @@ variables {R M}
 
 @[simp] theorem lsmul_apply (r : R) (m : M) : lsmul R M r m = r • m := rfl
 
+end comm_semiring
+
 end linear_map
 
 section semiring