From ef1393836f6ce62015eda56a720e4823acbb361b Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 3 Jun 2021 11:07:21 +0000 Subject: [PATCH] feat(ring_theory/tensor_product): the base change of a linear map along an algebra (#4773) Co-authored-by: kckennylau Co-authored-by: Kenny Lau Co-authored-by: Eric Wieser Co-authored-by: Oliver Nash --- src/algebra/lie/weights.lean | 23 +-- src/linear_algebra/tensor_product.lean | 77 ++++---- src/ring_theory/tensor_product.lean | 245 +++++++++++++++++++++++-- 3 files changed, 287 insertions(+), 58 deletions(-) diff --git a/src/algebra/lie/weights.lean b/src/algebra/lie/weights.lean index f8ced446e4c8d..e6333cf7d39a5 100644 --- a/src/algebra/lie/weights.lean +++ b/src/algebra/lie/weights.lean @@ -110,13 +110,13 @@ begin let f₁ : module.End R (M₁ ⊗[R] M₂) := (to_endomorphism R L M₁ x - (χ₁ x) • 1).rtensor M₂, let f₂ : module.End R (M₁ ⊗[R] M₂) := (to_endomorphism R L M₂ x - (χ₂ x) • 1).ltensor M₁, have h_comm_square : F.comp ↑g = (g : M₁ ⊗[R] M₂ →ₗ[R] M₃).comp (f₁ + f₂), - { ext m₁ m₂, simp only [← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, tensor_product.sub_tmul, - tensor_product.tmul_sub, tensor_product.smul_tmul, lie_tmul_right, tensor_product.tmul_smul, - to_endomorphism_apply_apply, tensor_product.mk_apply, lie_module_hom.map_smul, - linear_map.one_apply, lie_module_hom.coe_to_linear_map, linear_map.compr₂_apply, pi.add_apply, - linear_map.smul_apply, function.comp_app, linear_map.coe_comp, linear_map.rtensor_tmul, - lie_module_hom.map_add, linear_map.add_apply, lie_module_hom.map_sub, linear_map.sub_apply, - linear_map.ltensor_tmul], abel, }, + { ext m₁ m₂, simp only [← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, sub_tmul, tmul_sub, smul_tmul, + lie_tmul_right, tmul_smul, to_endomorphism_apply_apply, lie_module_hom.map_smul, + linear_map.one_apply, lie_module_hom.coe_to_linear_map, linear_map.smul_apply, + function.comp_app, linear_map.coe_comp, linear_map.rtensor_tmul, lie_module_hom.map_add, + linear_map.add_apply, lie_module_hom.map_sub, linear_map.sub_apply, linear_map.ltensor_tmul, + algebra_tensor_module.curry_apply, curry_apply, linear_map.to_fun_eq_coe, + linear_map.coe_restrict_scalars_eq_coe], abel, }, suffices : ∃ k, ((f₁ + f₂)^k) (m₁ ⊗ₜ m₂) = 0, { obtain ⟨k, hk⟩ := this, use k, rw [← linear_map.comp_apply, linear_map.commute_pow_left_of_commute h_comm_square, @@ -134,12 +134,9 @@ begin /- It's now just an application of the binomial theorem. -/ use k₁ + k₂ - 1, have hf_comm : commute f₁ f₂, - { ext m₁ m₂, - simp only [smul_comm (χ₁ x) (χ₂ x), linear_map.rtensor_smul, to_endomorphism_apply_apply, - tensor_product.mk_apply, linear_map.mul_apply, linear_map.one_apply, linear_map.ltensor_sub, - linear_map.compr₂_apply, linear_map.smul_apply, linear_map.ltensor_smul, - linear_map.rtensor_tmul, linear_map.map_sub, linear_map.map_smul, linear_map.rtensor_sub, - linear_map.sub_apply, linear_map.ltensor_tmul], }, + { ext m₁ m₂, simp only [linear_map.mul_apply, linear_map.rtensor_tmul, linear_map.ltensor_tmul, + algebra_tensor_module.curry_apply, linear_map.to_fun_eq_coe, linear_map.ltensor_tmul, + curry_apply, linear_map.coe_restrict_scalars_eq_coe], }, rw hf_comm.add_pow', simp only [tensor_product.map_incl, submodule.subtype_apply, finset.sum_apply, submodule.coe_mk, linear_map.coe_fn_sum, tensor_product.map_tmul, linear_map.smul_apply], diff --git a/src/linear_algebra/tensor_product.lean b/src/linear_algebra/tensor_product.lean index 8b70e793efa0a..7a263bd9b337e 100644 --- a/src/linear_algebra/tensor_product.lean +++ b/src/linear_algebra/tensor_product.lean @@ -221,8 +221,8 @@ variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*} {S : Type*} variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] variables [module R M] [module R N] [module R P] [module R Q] [module R S] -variables [distrib_mul_action R' M] [distrib_mul_action R' N] -variables [module R'' M] [module R'' N] +variables [distrib_mul_action R' M] +variables [module R'' M] include R variables (M N) @@ -325,7 +325,7 @@ Note that `module R' (M ⊗[R] N)` is available even without this typeclass on ` needed if `tensor_product.smul_tmul`, `tensor_product.smul_tmul'`, or `tensor_product.tmul_smul` is used. -/ -class compatible_smul := +class compatible_smul [distrib_mul_action R' N] := (smul_tmul : ∀ (r : R') (m : M) (n : N), (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n)) end @@ -334,7 +334,7 @@ end `mul_action.is_scalar_tower.left`. -/ @[priority 100] instance compatible_smul.is_scalar_tower - [has_scalar R' R] [is_scalar_tower R' R M] [is_scalar_tower R' R N] : + [has_scalar R' R] [is_scalar_tower R' R M] [distrib_mul_action R' N] [is_scalar_tower R' R N] : compatible_smul R R' M N := ⟨λ r m n, begin conv_lhs {rw ← one_smul R m}, @@ -344,7 +344,7 @@ instance compatible_smul.is_scalar_tower end⟩ /-- `smul` can be moved from one side of the product to the other .-/ -lemma smul_tmul [compatible_smul R R' M N] (r : R') (m : M) (n : N) : +lemma smul_tmul [distrib_mul_action R' N] [compatible_smul R R' M N] (r : R') (m : M) (n : N) : (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n) := compatible_smul.smul_tmul _ _ _ @@ -356,14 +356,22 @@ theorem smul.aux_of {R' : Type*} [has_scalar R' M] (r : R') (m : M) (n : N) : smul.aux r (free_add_monoid.of (m, n)) = (r • m) ⊗ₜ[R] n := rfl -variables [smul_comm_class R R' M] [smul_comm_class R R' N] -variables [smul_comm_class R R'' M] [smul_comm_class R R'' N] +variables [smul_comm_class R R' M] +variables [smul_comm_class R R'' M] --- Most of the time we want the instance below this one, which is easier for typeclass resolution --- to find. The `unused_arguments` is from one of the two comm_classes - while we only make use --- of one, it makes sense to make the API symmetric. -@[nolint unused_arguments] -instance has_scalar' : has_scalar R' (M ⊗[R] N) := +/-- Given two modules over a commutative semiring `R`, if one of the factors carries a +(distributive) action of a second type of scalars `R'`, which commutes with the action of `R`, then +the tensor product (over `R`) carries an action of `R'`. + +This instance defines this `R'` action in the case that it is the left module which has the `R'` +action. Two natural ways in which this situation arises are: + * Extension of scalars + * A tensor product of a group representation with a module not carrying an action + +Note that in the special case that `R = R'`, since `R` is commutative, we just get the usual scalar +action on a tensor product of two modules. This special case is important enough that, for +performance reasons, we define it explicitly below. -/ +instance left_has_scalar : has_scalar R' (M ⊗[R] N) := ⟨λ r, (add_con_gen (tensor_product.eqv R M N)).lift (smul.aux r : _ →+ M ⊗[R] N) $ add_con.add_con_gen_le $ λ x y hxy, match x, y, hxy with | _, _, (eqv.of_zero_left n) := (add_con.ker_rel _).2 $ @@ -380,7 +388,7 @@ add_con.add_con_gen_le $ λ x y hxy, match x, y, hxy with by simp_rw [add_monoid_hom.map_add, add_comm] end⟩ -instance : has_scalar R (M ⊗[R] N) := tensor_product.has_scalar' +instance : has_scalar R (M ⊗[R] N) := tensor_product.left_has_scalar protected theorem smul_zero (r : R') : (r • 0 : M ⊗[R] N) = 0 := add_monoid_hom.map_zero _ @@ -416,9 +424,7 @@ instance : add_comm_monoid (M ⊗[R] N) := nsmul_succ' := by simp [nat.succ_eq_one_add, tensor_product.one_smul, tensor_product.add_smul], .. tensor_product.add_comm_semigroup _ _, .. tensor_product.add_zero_class _ _} --- Most of the time we want the instance below this one, which is easier for typeclass resolution --- to find. -instance distrib_mul_action' : distrib_mul_action R' (M ⊗[R] N) := +instance left_distrib_mul_action : distrib_mul_action R' (M ⊗[R] N) := have ∀ (r : R') (m : M) (n : N), r • (m ⊗ₜ[R] n) = (r • m) ⊗ₜ n := λ _ _ _, rfl, { smul := (•), smul_add := λ r x y, tensor_product.smul_add r x y, @@ -429,35 +435,30 @@ have ∀ (r : R') (m : M) (n : N), r • (m ⊗ₜ[R] n) = (r • m) ⊗ₜ n := one_smul := tensor_product.one_smul, smul_zero := tensor_product.smul_zero } -instance : distrib_mul_action R (M ⊗[R] N) := tensor_product.distrib_mul_action' +instance : distrib_mul_action R (M ⊗[R] N) := tensor_product.left_distrib_mul_action --- note that we don't actually need `compatible_smul` here, but we include it for symmetry --- with `tmul_smul` to avoid exposing our asymmetric definition. -@[nolint unused_arguments] -theorem smul_tmul' [compatible_smul R R' M N] (r : R') (m : M) (n : N) : +theorem smul_tmul' (r : R') (m : M) (n : N) : r • (m ⊗ₜ[R] n) = (r • m) ⊗ₜ n := rfl -@[simp] lemma tmul_smul [compatible_smul R R' M N] (r : R') (x : M) (y : N) : +@[simp] lemma tmul_smul + [distrib_mul_action R' N] [compatible_smul R R' M N] (r : R') (x : M) (y : N) : x ⊗ₜ (r • y) = r • (x ⊗ₜ[R] y) := (smul_tmul _ _ _).symm --- Most of the time we want the instance below this one, which is easier for typeclass resolution --- to find. -instance module' : module R'' (M ⊗[R] N) := +instance left_module : module R'' (M ⊗[R] N) := { smul := (•), add_smul := tensor_product.add_smul, zero_smul := tensor_product.zero_smul, - ..tensor_product.distrib_mul_action' } + ..tensor_product.left_distrib_mul_action } -instance : module R (M ⊗[R] N) := tensor_product.module' +instance : module R (M ⊗[R] N) := tensor_product.left_module section -- Like `R'`, `R'₂` provides a `distrib_mul_action R'₂ (M ⊗[R] N)` -variables {R'₂ : Type*} [monoid R'₂] [distrib_mul_action R'₂ M] [distrib_mul_action R'₂ N] -variables [smul_comm_class R R'₂ M] [smul_comm_class R R'₂ N] -variables [has_scalar R'₂ R'] [compatible_smul R R' M N] [compatible_smul R R'₂ M N] +variables {R'₂ : Type*} [monoid R'₂] [distrib_mul_action R'₂ M] +variables [smul_comm_class R R'₂ M] [has_scalar R'₂ R'] /-- `is_scalar_tower R'₂ R' M` implies `is_scalar_tower R'₂ R' (M ⊗[R] N)` -/ instance is_scalar_tower_left [is_scalar_tower R'₂ R' M] : @@ -467,6 +468,9 @@ instance is_scalar_tower_left [is_scalar_tower R'₂ R' M] : (λ m n, by rw [smul_tmul', smul_tmul', smul_tmul', smul_assoc]) (λ x y ihx ihy, by rw [smul_add, smul_add, smul_add, ihx, ihy])⟩ +variables [distrib_mul_action R'₂ N] [distrib_mul_action R' N] +variables [compatible_smul R R'₂ M N] [compatible_smul R R' M N] + /-- `is_scalar_tower R'₂ R' N` implies `is_scalar_tower R'₂ R' (M ⊗[R] N)` -/ instance is_scalar_tower_right [is_scalar_tower R'₂ R' N] : is_scalar_tower R'₂ R' (M ⊗[R] N) := @@ -479,7 +483,7 @@ end /-- A short-cut instance for the common case, where the requirements for the `compatible_smul` instances are sufficient. -/ -instance is_scalar_tower [has_scalar R' R] [is_scalar_tower R' R M] [is_scalar_tower R' R N] : +instance is_scalar_tower [has_scalar R' R] [is_scalar_tower R' R M] : is_scalar_tower R' R (M ⊗[R] N) := tensor_product.is_scalar_tower_left -- or right @@ -663,6 +667,9 @@ def curry (f : M ⊗ N →ₗ P) : M →ₗ N →ₗ P := lcurry R M N P f @[simp] theorem curry_apply (f : M ⊗ N →ₗ[R] P) (m : M) (n : N) : curry f m n = f (m ⊗ₜ n) := rfl +lemma curry_injective : function.injective (curry : (M ⊗[R] N →ₗ[R] P) → (M →ₗ[R] N →ₗ[R] P)) := +λ g h H, mk_compr₂_inj H + theorem ext_threefold {g h : (M ⊗[R] N) ⊗[R] P →ₗ[R] Q} (H : ∀ x y z, g ((x ⊗ₜ y) ⊗ₜ z) = h ((x ⊗ₜ y) ⊗ₜ z)) : g = h := begin @@ -904,6 +911,12 @@ by { ext m n, simp only [compr₂_apply, mk_apply, comp_apply, ltensor_tmul] } lemma rtensor_comp : (g.comp f).rtensor M = (g.rtensor M).comp (f.rtensor M) := by { ext m n, simp only [compr₂_apply, mk_apply, comp_apply, rtensor_tmul] } +lemma ltensor_mul (f g : module.End R N) : (f * g).ltensor M = (f.ltensor M) * (g.ltensor M) := +ltensor_comp M f g + +lemma rtensor_mul (f g : module.End R N) : (f * g).rtensor M = (f.rtensor M) * (g.rtensor M) := +rtensor_comp M f g + variables (N) @[simp] lemma ltensor_id : (id : N →ₗ[R] N).ltensor M = id := map_id @@ -1030,7 +1043,7 @@ lemma sub_tmul (m₁ m₂ : M) (n : N) : (m₁ - m₂) ⊗ₜ n = (m₁ ⊗ₜ[R /-- While the tensor product will automatically inherit a ℤ-module structure from `add_comm_group.int_module`, that structure won't be compatible with lemmas like `tmul_smul` unless -we use a `ℤ-module` instance provided by `tensor_product.module'`. +we use a `ℤ-module` instance provided by `tensor_product.left_module`. When `R` is a `ring` we get the required `tensor_product.compatible_smul` instance through `is_scalar_tower`, but when it is only a `semiring` we need to build it from scratch. diff --git a/src/ring_theory/tensor_product.lean b/src/ring_theory/tensor_product.lean index 7b70cbf03e186..00f6818c605ec 100644 --- a/src/ring_theory/tensor_product.lean +++ b/src/ring_theory/tensor_product.lean @@ -1,43 +1,262 @@ /- Copyright (c) 2020 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison +Authors: Scott Morrison, Johan Commelin -/ import linear_algebra.tensor_product -import algebra.algebra.basic +import algebra.algebra.tower /-! # The tensor product of R-algebras -We construct the R-algebra structure on `A ⊗[R] B`, when `A` and `B` are both `R`-algebras, -and provide the structure isomorphisms +Let `R` be a (semi)ring and `A` an `R`-algebra. +In this file we: -* `R ⊗[R] A ≃ₐ[R] A` -* `A ⊗[R] R ≃ₐ[R] A` -* `A ⊗[R] B ≃ₐ[R] B ⊗[R] A` +- Define the `A`-module structure on `A ⊗ M`, for an `R`-module `M`. +- Define the `R`-algebra structure on `A ⊗ B`, for another `R`-algebra `B`. + and provide the structure isomorphisms + * `R ⊗[R] A ≃ₐ[R] A` + * `A ⊗[R] R ≃ₐ[R] A` + * `A ⊗[R] B ≃ₐ[R] B ⊗[R] A` + * `((A ⊗[R] B) ⊗[R] C) ≃ₐ[R] (A ⊗[R] (B ⊗[R] C))` -The code for -* `((A ⊗[R] B) ⊗[R] C) ≃ₐ[R] (A ⊗[R] (B ⊗[R] C))` -is written and compiles, but takes longer than the `-T100000` time limit, -so is currently commented out. +## Main declaration + +- `linear_map.base_change A f` is the `A`-linear map `A ⊗ f`, for an `R`-linear map `f`. + +## Implementation notes + +The heterobasic definitions below such as: + * `tensor_product.algebra_tensor_module.curry` + * `tensor_product.algebra_tensor_module.uncurry` + * `tensor_product.algebra_tensor_module.lcurry` + * `tensor_product.algebra_tensor_module.lift` + * `tensor_product.algebra_tensor_module.lift.equiv` + * `tensor_product.algebra_tensor_module.mk` + * `tensor_product.algebra_tensor_module.assoc` + +are just more general versions of the definitions already in `linear_algebra/tensor_product`. 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. -/ universes u v₁ v₂ v₃ v₄ -namespace algebra - open_locale tensor_product open tensor_product namespace tensor_product +variables {R A M N P : Type*} + +/-! +### The `A`-module structure on `A ⊗[R] M` +-/ + +open linear_map +open algebra (lsmul) + +namespace algebra_tensor_module + +section semiring +variables [comm_semiring R] [semiring A] [algebra R A] +variables [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] +variables [add_comm_monoid N] [module R N] +variables [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] + +lemma smul_eq_lsmul_rtensor (a : A) (x : M ⊗[R] N) : a • x = (lsmul R M a).rtensor N x := rfl + +/-- Heterobasic version of `tensor_product.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`. -/ +@[simps] def curry (f : (M ⊗[R] N) →ₗ[A] P) : M →ₗ[A] (N →ₗ[R] P) := +{ map_smul' := λ c x, linear_map.ext $ λ y, f.map_smul c (x ⊗ₜ y), + .. curry (f.restrict_scalars R) } + +lemma restrict_scalars_curry (f : (M ⊗[R] N) →ₗ[A] P) : + restrict_scalars R (curry f) = curry (f.restrict_scalars R) := +rfl + +/-- Just as `tensor_product.mk_compr₂_inj` is marked `ext` instead of `tensor_product.ext`, this is +a better `ext` lemma than `tensor_product.algebra_tensor_module.ext` below. + +See note [partially-applied ext lemmas]. -/ +@[ext] lemma curry_injective : + function.injective (curry : (M ⊗ N →ₗ[A] P) → (M →ₗ[A] N →ₗ[R] P)) := +λ x y h, linear_map.restrict_scalars_injective R $ curry_injective $ + (congr_arg (linear_map.restrict_scalars R) h : _) + +theorem ext {g h : (M ⊗[R] N) →ₗ[A] P} + (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y)) : g = h := +curry_injective $ linear_map.ext₂ H + +end semiring + +section comm_semiring +variables [comm_semiring R] [comm_semiring A] [algebra R A] +variables [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] +variables [add_comm_monoid N] [module R N] +variables [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] + +/-- Heterobasic version of `tensor_product.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`. -/ +@[simps] def lift (f : M →ₗ[A] (N →ₗ[R] P)) : (M ⊗[R] N) →ₗ[A] P := +{ map_smul' := λ c, show ∀ x : M ⊗[R] N, (lift (f.restrict_scalars R)).comp (lsmul R _ c) x = + (lsmul R _ c).comp (lift (f.restrict_scalars R)) x, + from ext_iff.1 $ tensor_product.ext $ λ x y, + by simp only [comp_apply, algebra.lsmul_coe, smul_tmul', lift.tmul, coe_restrict_scalars_eq_coe, + f.map_smul, smul_apply], + .. lift (f.restrict_scalars R) } + +@[simp] lemma lift_tmul (f : M →ₗ[A] (N →ₗ[R] P)) (x : M) (y : N) : + lift f (x ⊗ₜ y) = f x y := +lift.tmul' x y + +variables (R A M N P) +/-- Heterobasic version of `tensor_product.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`. -/ +@[simps] def uncurry : (M →ₗ[A] (N →ₗ[R] P)) →ₗ[A] ((M ⊗[R] N) →ₗ[A] P) := +{ to_fun := lift, + map_add' := λ f g, ext $ λ x y, by simp only [lift_tmul, add_apply], + map_smul' := λ c f, ext $ λ x y, by simp only [lift_tmul, smul_apply] } + +/-- Heterobasic version of `tensor_product.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`. -/ +@[simps] def lcurry : ((M ⊗[R] N) →ₗ[A] P) →ₗ[A] (M →ₗ[A] (N →ₗ[R] P)) := +{ to_fun := curry, + map_add' := λ f g, rfl, + map_smul' := λ c f, rfl } + +/-- Heterobasic version of `tensor_product.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`. -/ +def lift.equiv : (M →ₗ[A] (N →ₗ[R] P)) ≃ₗ[A] ((M ⊗[R] N) →ₗ[A] P) := +linear_equiv.of_linear (uncurry R A M N P) (lcurry R A M N P) + (linear_map.ext $ λ f, ext $ λ x y, lift_tmul _ x y) + (linear_map.ext $ λ f, linear_map.ext $ λ x, linear_map.ext $ λ y, lift_tmul f x y) + +variables (R A M N P) +/-- Heterobasic version of `tensor_product.mk`: + +The canonical bilinear map `M →[A] N →[R] M ⊗[R] N`. -/ +@[simps] def mk : M →ₗ[A] N →ₗ[R] M ⊗[R] N := +{ map_smul' := λ c x, rfl, + .. mk R M N } + +/-- Heterobasic version of `tensor_product.assoc`: + +Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ +def assoc : ((M ⊗[A] P) ⊗[R] N) ≃ₗ[A] (M ⊗[A] (P ⊗[R] N)) := +linear_equiv.of_linear + (lift $ tensor_product.uncurry A _ _ _ $ comp (lcurry R A _ _ _) $ + tensor_product.mk A M (P ⊗[R] N)) + (tensor_product.uncurry A _ _ _ $ comp (uncurry R A _ _ _) $ + by apply tensor_product.curry; exact (mk R A _ _)) + (by { ext, refl, }) + (by { ext, refl, }) + +end comm_semiring + +end algebra_tensor_module + +end tensor_product + +namespace linear_map +open tensor_product + +/-! +### The base-change of a linear map of `R`-modules to a linear map of `A`-modules +-/ + +section semiring + +variables {R A B M N : Type*} [comm_semiring R] +variables [semiring A] [algebra R A] [semiring B] [algebra R B] +variables [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] +variables (r : R) (f g : M →ₗ[R] N) + +variables (A) + +/-- `base_change A f` for `f : M →ₗ[R] N` is the `A`-linear map `A ⊗[R] M →ₗ[A] A ⊗[R] N`. -/ +def base_change (f : M →ₗ[R] N) : A ⊗[R] M →ₗ[A] A ⊗[R] N := +{ to_fun := f.ltensor A, + map_add' := (f.ltensor A).map_add, + map_smul' := λ a x, + show (f.ltensor A) (rtensor M (algebra.lmul R A a) x) = + (rtensor N ((algebra.lmul R A) a)) ((ltensor A f) x), + by simp only [← comp_apply, ltensor_comp_rtensor, rtensor_comp_ltensor] } + +variables {A} + +@[simp] lemma base_change_tmul (a : A) (x : M) : + f.base_change A (a ⊗ₜ x) = a ⊗ₜ (f x) := rfl + +lemma base_change_eq_ltensor : + (f.base_change A : A ⊗ M → A ⊗ N) = f.ltensor A := rfl + +@[simp] lemma base_change_add : + (f + g).base_change A = f.base_change A + g.base_change A := +by { ext, simp [base_change_eq_ltensor], } + +@[simp] lemma base_change_zero : base_change A (0 : M →ₗ[R] N) = 0 := +by { ext, simp [base_change_eq_ltensor], } + +@[simp] lemma base_change_smul : (r • f).base_change A = r • (f.base_change A) := +by { ext, simp [base_change_tmul], } + +variables (R A M N) +/-- `base_change` as a linear map. -/ +@[simps] def base_change_hom : (M →ₗ[R] N) →ₗ[R] A ⊗[R] M →ₗ[A] A ⊗[R] N := +{ to_fun := base_change A, + map_add' := base_change_add, + map_smul' := base_change_smul } + +end semiring + +section ring + +variables {R A B M N : Type*} [comm_ring R] +variables [ring A] [algebra R A] [ring B] [algebra R B] +variables [add_comm_group M] [module R M] [add_comm_group N] [module R N] +variables (f g : M →ₗ[R] N) + +@[simp] lemma base_change_sub : + (f - g).base_change A = f.base_change A - g.base_change A := +by { ext, simp [base_change_eq_ltensor], } + +@[simp] lemma base_change_neg : (-f).base_change A = -(f.base_change A) := +by { ext, simp [base_change_eq_ltensor], } + +end ring + +end linear_map + +namespace algebra +namespace tensor_product + section semiring variables {R : Type u} [comm_semiring R] variables {A : Type v₁} [semiring A] [algebra R A] variables {B : Type v₂} [semiring B] [algebra R B] +/-! +### The `R`-algebra structure on `A ⊗[R] B` +-/ + /-- (Implementation detail) The multiplication map on `A ⊗[R] B`,