diff --git a/Mathlib/Algebra/Algebra/Bilinear.lean b/Mathlib/Algebra/Algebra/Bilinear.lean index 21191c3bd17ca..787bbf9335d81 100644 --- a/Mathlib/Algebra/Algebra/Bilinear.lean +++ b/Mathlib/Algebra/Algebra/Bilinear.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau, Yury Kudryashov -/ import Mathlib.Algebra.Algebra.Basic +import Mathlib.Algebra.Algebra.Equiv import Mathlib.Algebra.Hom.Iterate import Mathlib.Algebra.Hom.NonUnitalAlg import Mathlib.LinearAlgebra.TensorProduct @@ -153,7 +154,18 @@ end NonUnital section Semiring -variable (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] +variable (R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] + +variable {R A B} in +/-- A `LinearMap` preserves multiplication if pre- and post- composition with `LinearMap.mul` are +equivalent. By converting the statement into an equality of `LinearMap`s, this lemma allows various +specialized `ext` lemmas about `→ₗ[R]` to then be applied. + +This is the `LinearMap` version of `AddMonoidHom.map_mul_iff`. -/ +theorem map_mul_iff (f : A →ₗ[R] B) : + (∀ x y, f (x * y) = f x * f y) ↔ + (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f := + Iff.symm LinearMap.ext_iff₂ /-- The multiplication in an algebra is an algebra homomorphism into the endomorphisms on the algebra. diff --git a/Mathlib/Algebra/Algebra/RestrictScalars.lean b/Mathlib/Algebra/Algebra/RestrictScalars.lean index 05cff5f87b33e..319b36613aed2 100644 --- a/Mathlib/Algebra/Algebra/RestrictScalars.lean +++ b/Mathlib/Algebra/Algebra/RestrictScalars.lean @@ -32,12 +32,12 @@ typeclass instead. There are many similarly-named definitions elsewhere which do not refer to this type alias. These refer to restricting the scalar type in a bundled type, such as from `A →ₗ[R] B` to `A →ₗ[S] B`: -* `LinearMap.RestrictScalars` -* `LinearEquiv.RestrictScalars` -* `AlgHom.RestrictScalars` -* `AlgEquiv.RestrictScalars` -* `Submodule.RestrictScalars` -* `Subalgebra.RestrictScalars` +* `LinearMap.restrictScalars` +* `LinearEquiv.restrictScalars` +* `AlgHom.restrictScalars` +* `AlgEquiv.restrictScalars` +* `Submodule.restrictScalars` +* `Subalgebra.restrictScalars` -/ @@ -214,7 +214,7 @@ theorem RestrictScalars.ringEquiv_map_smul (r : R) (x : RestrictScalars R S A) : #align restrict_scalars.ring_equiv_map_smul RestrictScalars.ringEquiv_map_smul /-- `R ⟶ S` induces `S-Alg ⥤ R-Alg` -/ -instance : Algebra R (RestrictScalars R S A) := +instance RestrictScalars.algebra : Algebra R (RestrictScalars R S A) := { (algebraMap S A).comp (algebraMap R S) with smul := (· • ·) commutes' := fun _ _ ↦ Algebra.commutes' _ _ diff --git a/Mathlib/LinearAlgebra/BilinearMap.lean b/Mathlib/LinearAlgebra/BilinearMap.lean index e95a239939bfd..a770457fb5cb8 100644 --- a/Mathlib/LinearAlgebra/BilinearMap.lean +++ b/Mathlib/LinearAlgebra/BilinearMap.lean @@ -119,6 +119,9 @@ theorem congr_fun₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : LinearMap.congr_fun (LinearMap.congr_fun h x) y #align linear_map.congr_fun₂ LinearMap.congr_fun₂ +theorem ext_iff₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} : f = g ↔ ∀ m n, f m n = g m n := + ⟨congr_fun₂, ext₂⟩ + section attribute [local instance] SMulCommClass.symm diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index 0f5be38d28d7a..fc6d28083f44d 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -594,19 +594,12 @@ tensors can be directly applied by the caller (without needing `TensorProduct.on def algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[S] C) (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) (h_one : f (1 ⊗ₜ[R] 1) = 1) : A ⊗[R] B →ₐ[S] C := - AlgHom.ofLinearMap f h_one fun x y => by - simp only - refine TensorProduct.induction_on x ?_ ?_ ?_ - · rw [zero_mul, map_zero, zero_mul] - · intro a₁ b₁ - refine TensorProduct.induction_on y ?_ ?_ ?_ - · rw [mul_zero, map_zero, mul_zero] - · intro a₂ b₂ - rw [tmul_mul_tmul, h_mul] - · intro x₁ x₂ h₁ h₂ - rw [mul_add, map_add, map_add, mul_add, h₁, h₂] - · intro x₁ x₂ h₁ h₂ - rw [add_mul, map_add, map_add, add_mul, h₁, h₂] + AlgHom.ofLinearMap f h_one <| f.map_mul_iff.2 <| by + -- these instances are needed by the statement of `ext`, but not by the current definition. + letI : Algebra R C := RestrictScalars.algebra R S C + letI : IsScalarTower R S C := RestrictScalars.isScalarTower R S C + ext + exact h_mul _ _ _ _ #align algebra.tensor_product.alg_hom_of_linear_map_tensor_product Algebra.TensorProduct.algHomOfLinearMapTensorProduct @[simp] @@ -642,23 +635,9 @@ def algEquivOfLinearEquivTripleTensorProduct (f : (A ⊗[R] B) ⊗[R] C ≃ₗ[R f ((a₁ * a₂) ⊗ₜ (b₁ * b₂) ⊗ₜ (c₁ * c₂)) = f (a₁ ⊗ₜ b₁ ⊗ₜ c₁) * f (a₂ ⊗ₜ b₂ ⊗ₜ c₂)) (h_one : f (((1 : A) ⊗ₜ[R] (1 : B)) ⊗ₜ[R] (1 : C)) = 1) : (A ⊗[R] B) ⊗[R] C ≃ₐ[R] D := --- porting note : build the whole algebra isomorphism times out, so I propose to define the version --- of tensoring three rings in terms of the version tensoring with two rings -algEquivOfLinearEquivTensorProduct f (fun x₁ x₂ c₁ c₂ => by - refine TensorProduct.induction_on x₁ ?_ ?_ ?_ <;> - refine TensorProduct.induction_on x₂ ?_ ?_ ?_ <;> - simp only [zero_tmul, tmul_zero, tmul_mul_tmul, map_zero, zero_mul, mul_zero, mul_add, add_mul, - map_add, add_tmul, tmul_add, h_mul] <;> - try - intros - trivial - · intros ab₁ ab₂ h₁ h₂ a b - rw [h₁, h₂] - · intros a b ab₁ ab₂ h₁ h₂ - rw [h₁, h₂] - · intros ab₁ ab₂ _ _ x y hx hy - rw [add_add_add_comm, hx, hy, add_add_add_comm]) - h_one + AlgEquiv.ofLinearEquiv f h_one <| f.map_mul_iff.2 <| by + ext + exact h_mul _ _ _ _ _ _ #align algebra.tensor_product.alg_equiv_of_linear_equiv_triple_tensor_product Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct @[simp]