From 8a59d574eb38cdaa37c163ffda4e9b93dd0ac670 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 18:34:46 +0000 Subject: [PATCH 01/23] AAAAARRGHH --- .../linear_algebra/bilinear_form/basic.lean | 0 .../bilinear_form/tensor_product.lean | 97 +- .../linear_algebra/tensor_product.lean | 35 + .../ring_theory/tensor_product.lean | 895 ++++++++++++++++++ .../from_mathlib/complexification.lean | 19 + 5 files changed, 1045 insertions(+), 1 deletion(-) create mode 100644 src/for_mathlib/linear_algebra/bilinear_form/basic.lean create mode 100644 src/for_mathlib/linear_algebra/tensor_product.lean create mode 100644 src/for_mathlib/ring_theory/tensor_product.lean create mode 100644 src/geometric_algebra/from_mathlib/complexification.lean diff --git a/src/for_mathlib/linear_algebra/bilinear_form/basic.lean b/src/for_mathlib/linear_algebra/bilinear_form/basic.lean new file mode 100644 index 000000000..e69de29bb diff --git a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean index 361c111e4..21909f5d8 100644 --- a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean +++ b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean @@ -4,16 +4,111 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ import linear_algebra.bilinear_form.tensor_product +import ring_theory.tensor_product import linear_algebra.quadratic_form.basic import data.is_R_or_C.basic +import for_mathlib.linear_algebra.tensor_product universes u v w -variables {ι : Type*} {R : Type*} {M₁ M₂ : Type*} +variables {ι : Type*} {R S : Type*} {M₁ M₂ : Type*} open_locale tensor_product namespace bilin_form +section comm_semiring +variables [comm_semiring R] [comm_semiring S] +variables [add_comm_monoid M₁] [add_comm_monoid M₂] +variables [algebra R S] [module R M₁] [module S M₁] +variables [smul_comm_class R S M₁] [smul_comm_class S R M₁] [smul_comm_class R S S] [is_scalar_tower R S M₁] +variables [module R M₂] + +notation (name := tensor_product') + M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N + +set_option pp.parens true + +#check tensor_product.algebra_tensor_module.lift.equiv R S (M₁ ⊗ M₂) (M₁ ⊗ M₂) S + +#check tensor_product.tensor_tensor_tensor_comm R M₁ M₂ M₁ M₂ + +instance : module R (M₁ ⊗[S] M₁) := tensor_product.left_module +instance : smul_comm_class R S (M₁ ⊗[S] M₁) := tensor_product.smul_comm_class_left +instance foo : module S ((M₁ ⊗[S] M₁) ⊗[R] (M₂ ⊗[R] M₂)) := tensor_product.left_module + +instance : is_scalar_tower R S (M₁ ⊗[R] M₂) := tensor_product.is_scalar_tower_left + +instance : smul_comm_class R S (bilin_form S M₁) := bilin_form.smul_comm_class +instance : module S (bilin_form S M₁ ⊗[R] bilin_form R M₂) := tensor_product.left_module + +section +variables (R S M₁ M₂) + +def tensor_tensor_tensor_comm' : + ((M₁ ⊗[R] M₂) ⊗[S] (M₁ ⊗[R] M₂) ≃ₗ[S] (M₁ ⊗[S] M₁) ⊗[R] (M₂ ⊗[R] M₂)) := sorry + +end + +#check (( + tensor_tensor_tensor_comm' _ _ _ _ : (((M₁ ⊗[R] M₂) ⊗[S] (M₁ ⊗[R] M₂)) ≃ₗ[S] ((M₁ ⊗[S] M₁) ⊗[R] (M₂ ⊗[R] M₂))) + -- tensor_product.tensor_tensor_tensor_comm R M₁ M₂ M₁ M₂ + +).dual_map + ≪≫ₗ (tensor_product.lift.equiv S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) S).symm + ≪≫ₗ linear_map.to_bilin).to_linear_map +-- #exit +/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/ +def tensor_distrib' : bilin_form S M₁ ⊗[R] bilin_form R M₂ →ₗ[S] bilin_form S (M₁ ⊗[R] M₂) := +((tensor_tensor_tensor_comm' R S M₁ M₂).dual_map + ≪≫ₗ (tensor_product.lift.equiv S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) S).symm + ≪≫ₗ linear_map.to_bilin).to_linear_map + ∘ₗ _ + ∘ₗ (tensor_product.congr + (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv S M₁ M₁ S) + (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv R M₂ M₂ R)).to_linear_map + +@[simp] lemma tensor_distrib_tmul (B₁ : bilin_form R M₁) (B₂ : bilin_form R M₂) + (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : + tensor_distrib (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := +rfl + +/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +@[reducible] +protected def tmul (B₁ : bilin_form R M₁) (B₂ : bilin_form R M₂) : bilin_form R (M₁ ⊗[R] M₂) := +tensor_distrib (B₁ ⊗ₜ[R] B₂) + +end comm_semiring + + +section comm_semiring +variables [comm_semiring R] +variables [add_comm_monoid M₁] [add_comm_monoid M₂] +variables [module R M₁] [module R M₂] + +/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/ +def tensor_distrib'' : bilin_form R M₁ ⊗[R] bilin_form R M₂ →ₗ[R] bilin_form R (M₁ ⊗[R] M₂) := +((tensor_product.tensor_tensor_tensor_comm R M₁ M₂ M₁ M₂).dual_map + ≪≫ₗ (tensor_product.lift.equiv R (M₁ ⊗ M₂) (M₁ ⊗ M₂) R).symm + ≪≫ₗ linear_map.to_bilin).to_linear_map + ∘ₗ tensor_product.dual_distrib R _ _ + ∘ₗ (tensor_product.congr + (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv R _ _ _) + (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv R _ _ _)).to_linear_map + +#print tensor_distrib'' + +@[simp] lemma tensor_distrib_tmul (B₁ : bilin_form R M₁) (B₂ : bilin_form R M₂) + (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : + tensor_distrib (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := +rfl + +/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +@[reducible] +protected def tmul (B₁ : bilin_form R M₁) (B₂ : bilin_form R M₂) : bilin_form R (M₁ ⊗[R] M₂) := +tensor_distrib (B₁ ⊗ₜ[R] B₂) + +end comm_semiring + section comm_semiring variables [comm_semiring R] variables [add_comm_monoid M₁] [add_comm_monoid M₂] diff --git a/src/for_mathlib/linear_algebra/tensor_product.lean b/src/for_mathlib/linear_algebra/tensor_product.lean new file mode 100644 index 000000000..cbdefdfc4 --- /dev/null +++ b/src/for_mathlib/linear_algebra/tensor_product.lean @@ -0,0 +1,35 @@ +import linear_algebra.tensor_product + +section semiring +variables {R : Type*} [comm_semiring R] +variables {R' : Type*} [monoid R'] +variables {R'' : Type*} [semiring R''] +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] +variables [module R'' M] +include R + +variables {R'₂ : Type*} [monoid R'₂] [distrib_mul_action R'₂ M] +variables [smul_comm_class R R'₂ M] + + +open_locale tensor_product + +variables [smul_comm_class R R' M] +variables [smul_comm_class R R'' M] + +namespace tensor_product + +/-- `smul_comm_class R' R'₂ M` implies `smul_comm_class R' R'₂ (M ⊗[R] N)` -/ +instance smul_comm_class_left [smul_comm_class R' R'₂ M] : smul_comm_class R' R'₂ (M ⊗[R] N) := +{ smul_comm := λ r' r'₂ x, tensor_product.induction_on x + (by simp_rw tensor_product.smul_zero) + (λ m n, by simp_rw [smul_tmul', smul_comm]) + (λ x y ihx ihy, by { simp_rw tensor_product.smul_add, rw [ihx, ihy] }) } + +end tensor_product + +end semiring \ No newline at end of file diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean new file mode 100644 index 000000000..8b5c83d56 --- /dev/null +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -0,0 +1,895 @@ +import ring_theory.tensor_product + +universes u v₁ v₂ v₃ v₄ + +open_locale tensor_product +open tensor_product + +namespace tensor_product + +variables {R A M N P Q : Type*} + +/-! +### The `A`-module structure on `A ⊗[R] M` +-/ + +open linear_map +open _root_.algebra (lsmul) + +namespace algebra_tensor_module + + +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] +variables [add_comm_monoid Q] [module R Q] + +/-- The tensor product of a pair of linear maps between modules. -/ +def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] Q := +lift $ (show (Q →ₗ[R] P ⊗ Q) →ₗ[A] N →ₗ[R] P ⊗[R] Q, + from{ to_fun := λ h, h ∘ₗ g, + map_add' := λ h₁ h₂, linear_map.add_comp g h₂ h₁, + map_smul' := λ c h, linear_map.smul_comp c h g }) ∘ₗ mk R A P Q ∘ₗ f + +@[simp] theorem map_tmul (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) : + map f g (m ⊗ₜ n) = f m ⊗ₜ g n := +rfl + + +def congr (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : (M ⊗[R] N) ≃ₗ[A] (P ⊗[R] Q) := +linear_equiv.of_linear (map f g) (map f.symm g.symm) + (ext $ λ m n, by simp; simp only [linear_equiv.apply_symm_apply]) + (ext $ λ m n, by simp; simp only [linear_equiv.symm_apply_apply]) + +@[simp] theorem congr_tmul (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) : + congr f g (m ⊗ₜ n) = f m ⊗ₜ g n := +rfl + +@[simp] theorem congr_symm_tmul (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) : + (congr f g).symm (p ⊗ₜ q) = f.symm p ⊗ₜ g.symm q := +rfl + + +variables (R A M N P Q) + +notation (name := tensor_product') + M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N + + + +#check assoc R A M +/-- A tensor product analogue of `mul_left_comm`. -/ +def left_comm : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q) := +let e₁ := (assoc R A M Q P).symm, + e₂ := congr (tensor_product.comm A M P) (1 : Q ≃ₗ[R] Q), + e₃ := (assoc R A P Q M) in +e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) + +/-- Heterobasic version of `tensor_tensor_tensor_comm`: + +Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ +def tensor_tensor_tensor_comm : + (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := +(assoc R A (M ⊗[R] N) Q P).symm ≪≫ₗ _ +-- let e₁ := assoc R A M N (P ⊗[R] Q), +-- e₂ := congr (1 : M ≃ₗ[A] M) (left_comm R R N P Q), +-- e₃ := (assoc R A M P (N ⊗[R] Q)).symm in +-- e₁ ≪≫ₗ _ ≪≫ₗ e₃ -- (e₂ ≪≫ₗ e₃) + -- (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, simp only [curry_apply, tensor_product.curry_apply, mk_apply, tensor_product.mk_apply, + -- uncurry_apply, tensor_product.uncurry_apply, id_apply, lift_tmul, compr₂_apply, + -- restrict_scalars_apply, function.comp_app, to_fun_eq_coe, lcurry_apply, + -- linear_map.comp_apply] }) + +#check tensor_tensor_tensor_comm + +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 (linear_map.mul R A a) x) = + (rtensor N ((linear_map.mul R A) a)) ((ltensor A f) x), + by { rw [← comp_apply, ← comp_apply], + simp only [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`, +for a fixed pure tensor in the first argument, +as an `R`-linear map. +-/ +def mul_aux (a₁ : A) (b₁ : B) : (A ⊗[R] B) →ₗ[R] (A ⊗[R] B) := +tensor_product.map (linear_map.mul_left R a₁) (linear_map.mul_left R b₁) + +@[simp] +lemma mul_aux_apply (a₁ a₂ : A) (b₁ b₂ : B) : + (mul_aux a₁ b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) := +rfl + +/-- +(Implementation detail) +The multiplication map on `A ⊗[R] B`, +as an `R`-bilinear map. +-/ +def mul : (A ⊗[R] B) →ₗ[R] (A ⊗[R] B) →ₗ[R] (A ⊗[R] B) := +tensor_product.lift $ linear_map.mk₂ R mul_aux + (λ x₁ x₂ y, tensor_product.ext' $ λ x' y', + by simp only [mul_aux_apply, linear_map.add_apply, add_mul, add_tmul]) + (λ c x y, tensor_product.ext' $ λ x' y', + by simp only [mul_aux_apply, linear_map.smul_apply, smul_tmul', smul_mul_assoc]) + (λ x y₁ y₂, tensor_product.ext' $ λ x' y', + by simp only [mul_aux_apply, linear_map.add_apply, add_mul, tmul_add]) + (λ c x y, tensor_product.ext' $ λ x' y', + by simp only [mul_aux_apply, linear_map.smul_apply, smul_tmul, smul_tmul', smul_mul_assoc]) + +@[simp] +lemma mul_apply (a₁ a₂ : A) (b₁ b₂ : B) : + mul (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) := +rfl + +lemma mul_assoc' (mul : (A ⊗[R] B) →ₗ[R] (A ⊗[R] B) →ₗ[R] (A ⊗[R] B)) + (h : ∀ (a₁ a₂ a₃ : A) (b₁ b₂ b₃ : B), + mul (mul (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂)) (a₃ ⊗ₜ[R] b₃) = + mul (a₁ ⊗ₜ[R] b₁) (mul (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃))) : + ∀ (x y z : A ⊗[R] B), mul (mul x y) z = mul x (mul y z) := +begin + intros, + apply tensor_product.induction_on x, + { simp only [linear_map.map_zero, linear_map.zero_apply], }, + apply tensor_product.induction_on y, + { simp only [linear_map.map_zero, forall_const, linear_map.zero_apply], }, + apply tensor_product.induction_on z, + { simp only [linear_map.map_zero, forall_const], }, + { intros, simp only [h], }, + { intros, simp only [linear_map.map_add, *], }, + { intros, simp only [linear_map.map_add, *, linear_map.add_apply], }, + { intros, simp only [linear_map.map_add, *, linear_map.add_apply], }, +end + +lemma mul_assoc (x y z : A ⊗[R] B) : mul (mul x y) z = mul x (mul y z) := +mul_assoc' mul (by { intros, simp only [mul_apply, mul_assoc], }) x y z + +lemma one_mul (x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x := +begin + apply tensor_product.induction_on x; + simp {contextual := tt}, +end + +lemma mul_one (x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x := +begin + apply tensor_product.induction_on x; + simp {contextual := tt}, +end + +instance : has_one (A ⊗[R] B) := +{ one := 1 ⊗ₜ 1 } + +instance : add_monoid_with_one (A ⊗[R] B) := add_monoid_with_one.unary + +instance : semiring (A ⊗[R] B) := +{ zero := 0, + add := (+), + one := 1, + mul := λ a b, mul a b, + one_mul := one_mul, + mul_one := mul_one, + mul_assoc := mul_assoc, + zero_mul := by simp, + mul_zero := by simp, + left_distrib := by simp, + right_distrib := by simp, + .. (by apply_instance : add_monoid_with_one (A ⊗[R] B)), + .. (by apply_instance : add_comm_monoid (A ⊗[R] B)) }. + +lemma one_def : (1 : A ⊗[R] B) = (1 : A) ⊗ₜ (1 : B) := rfl + +@[simp] +lemma tmul_mul_tmul (a₁ a₂ : A) (b₁ b₂ : B) : + (a₁ ⊗ₜ[R] b₁) * (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) := +rfl + +@[simp] +lemma tmul_pow (a : A) (b : B) (k : ℕ) : + (a ⊗ₜ[R] b)^k = (a^k) ⊗ₜ[R] (b^k) := +begin + induction k with k ih, + { simp [one_def], }, + { simp [pow_succ, ih], } +end + + +/-- The ring morphism `A →+* A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/ +@[simps] +def include_left_ring_hom : A →+* A ⊗[R] B := +{ to_fun := λ a, a ⊗ₜ 1, + map_zero' := by simp, + map_add' := by simp [add_tmul], + map_one' := rfl, + map_mul' := by simp } + +variables {S : Type*} [comm_semiring S] [algebra S A] + +instance left_algebra [smul_comm_class R S A] : algebra S (A ⊗[R] B) := +{ commutes' := λ r x, + begin + apply tensor_product.induction_on x, + { simp, }, + { intros a b, dsimp, rw [algebra.commutes, _root_.mul_one, _root_.one_mul], }, + { intros y y' h h', dsimp at h h' ⊢, simp only [mul_add, add_mul, h, h'], }, + end, + smul_def' := λ r x, + begin + apply tensor_product.induction_on x, + { simp [smul_zero], }, + { intros a b, dsimp, rw [tensor_product.smul_tmul', algebra.smul_def r a, _root_.one_mul] }, + { intros, dsimp, simp [smul_add, mul_add, *], }, + end, + .. tensor_product.include_left_ring_hom.comp (algebra_map S A), + .. (by apply_instance : module S (A ⊗[R] B)) }. + +-- This is for the `undergrad.yaml` list. +/-- The tensor product of two `R`-algebras is an `R`-algebra. -/ +instance : algebra R (A ⊗[R] B) := infer_instance + +@[simp] +lemma algebra_map_apply [smul_comm_class R S A] (r : S) : + (algebra_map S (A ⊗[R] B)) r = ((algebra_map S A) r) ⊗ₜ 1 := rfl + +variables {C : Type v₃} [semiring C] [algebra R C] + +@[ext] +theorem ext {g h : (A ⊗[R] B) →ₐ[R] C} + (H : ∀ a b, g (a ⊗ₜ b) = h (a ⊗ₜ b)) : g = h := +begin + apply @alg_hom.to_linear_map_injective R (A ⊗[R] B) C _ _ _ _ _ _ _ _, + ext, + simp [H], +end + +-- TODO: with `smul_comm_class R S A` we can have this as an `S`-algebra morphism +/-- The `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/ +def include_left : A →ₐ[R] A ⊗[R] B := +{ commutes' := by simp, + ..include_left_ring_hom } + +@[simp] +lemma include_left_apply (a : A) : (include_left : A →ₐ[R] A ⊗[R] B) a = a ⊗ₜ 1 := rfl + +/-- The algebra morphism `B →ₐ[R] A ⊗[R] B` sending `b` to `1 ⊗ₜ b`. -/ +def include_right : B →ₐ[R] A ⊗[R] B := +{ to_fun := λ b, 1 ⊗ₜ b, + map_zero' := by simp, + map_add' := by simp [tmul_add], + map_one' := rfl, + map_mul' := by simp, + commutes' := λ r, + begin + simp only [algebra_map_apply], + transitivity r • ((1 : A) ⊗ₜ[R] (1 : B)), + { rw [←tmul_smul, algebra.smul_def], simp, }, + { simp [algebra.smul_def], }, + end, } + +@[simp] +lemma include_right_apply (b : B) : (include_right : B →ₐ[R] A ⊗[R] B) b = 1 ⊗ₜ b := rfl + +lemma include_left_comp_algebra_map {R S T : Type*} [comm_ring R] [comm_ring S] [comm_ring T] + [algebra R S] [algebra R T] : + (include_left.to_ring_hom.comp (algebra_map R S) : R →+* S ⊗[R] T) = + include_right.to_ring_hom.comp (algebra_map R T) := +by { ext, simp } + +end semiring + +section ring + +variables {R : Type u} [comm_ring R] +variables {A : Type v₁} [ring A] [algebra R A] +variables {B : Type v₂} [ring B] [algebra R B] + +instance : ring (A ⊗[R] B) := +{ .. (by apply_instance : add_comm_group (A ⊗[R] B)), + .. (by apply_instance : semiring (A ⊗[R] B)) }. + +end ring + +section comm_ring + +variables {R : Type u} [comm_ring R] +variables {A : Type v₁} [comm_ring A] [algebra R A] +variables {B : Type v₂} [comm_ring B] [algebra R B] + +instance : comm_ring (A ⊗[R] B) := +{ mul_comm := λ x y, + begin + apply tensor_product.induction_on x, + { simp, }, + { intros a₁ b₁, + apply tensor_product.induction_on y, + { simp, }, + { intros a₂ b₂, + simp [mul_comm], }, + { intros a₂ b₂ ha hb, + simp [mul_add, add_mul, ha, hb], }, }, + { intros x₁ x₂ h₁ h₂, + simp [mul_add, add_mul, h₁, h₂], }, + end + .. (by apply_instance : ring (A ⊗[R] B)) }. + +section right_algebra + +/-- `S ⊗[R] T` has a `T`-algebra structure. This is not a global instance or else the action of +`S` on `S ⊗[R] S` would be ambiguous. -/ +@[reducible] def right_algebra : algebra B (A ⊗[R] B) := +(algebra.tensor_product.include_right.to_ring_hom : B →+* A ⊗[R] B).to_algebra + +local attribute [instance] tensor_product.right_algebra + +instance right_is_scalar_tower : is_scalar_tower R B (A ⊗[R] B) := +is_scalar_tower.of_algebra_map_eq (λ r, (algebra.tensor_product.include_right.commutes r).symm) + +end right_algebra + +end comm_ring + +/-- +Verify that typeclass search finds the ring structure on `A ⊗[ℤ] B` +when `A` and `B` are merely rings, by treating both as `ℤ`-algebras. +-/ +example {A : Type v₁} [ring A] {B : Type v₂} [ring B] : ring (A ⊗[ℤ] B) := +by apply_instance + +/-- +Verify that typeclass search finds the comm_ring structure on `A ⊗[ℤ] B` +when `A` and `B` are merely comm_rings, by treating both as `ℤ`-algebras. +-/ +example {A : Type v₁} [comm_ring A] {B : Type v₂} [comm_ring B] : comm_ring (A ⊗[ℤ] B) := +by apply_instance + +/-! +We now build the structure maps for the symmetric monoidal category of `R`-algebras. +-/ +section monoidal + +section +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] +variables {C : Type v₃} [semiring C] [algebra R C] +variables {D : Type v₄} [semiring D] [algebra R D] + +/-- +Build an algebra morphism from a linear map out of a tensor product, +and evidence of multiplicativity on pure tensors. +-/ +def alg_hom_of_linear_map_tensor_product + (f : A ⊗[R] B →ₗ[R] C) + (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) + (w₂ : ∀ r, f ((algebra_map R A) r ⊗ₜ[R] 1) = (algebra_map R C) r): + A ⊗[R] B →ₐ[R] C := +{ map_one' := by rw [←(algebra_map R C).map_one, ←w₂, (algebra_map R A).map_one]; refl, + map_zero' := by rw [linear_map.to_fun_eq_coe, map_zero], + map_mul' := λ x y, by + { rw linear_map.to_fun_eq_coe, + apply tensor_product.induction_on x, + { rw [zero_mul, map_zero, zero_mul] }, + { intros a₁ b₁, + apply tensor_product.induction_on y, + { rw [mul_zero, map_zero, mul_zero] }, + { intros a₂ b₂, + rw [tmul_mul_tmul, w₁] }, + { intros x₁ x₂ h₁ h₂, + rw [mul_add, map_add, map_add, mul_add, h₁, h₂] } }, + { intros x₁ x₂ h₁ h₂, + rw [add_mul, map_add, map_add, add_mul, h₁, h₂] } }, + commutes' := λ r, by rw [linear_map.to_fun_eq_coe, algebra_map_apply, w₂], + .. f } + +@[simp] +lemma alg_hom_of_linear_map_tensor_product_apply (f w₁ w₂ x) : + (alg_hom_of_linear_map_tensor_product f w₁ w₂ : A ⊗[R] B →ₐ[R] C) x = f x := rfl + +/-- +Build an algebra equivalence from a linear equivalence out of a tensor product, +and evidence of multiplicativity on pure tensors. +-/ +def alg_equiv_of_linear_equiv_tensor_product + (f : A ⊗[R] B ≃ₗ[R] C) + (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) + (w₂ : ∀ r, f ((algebra_map R A) r ⊗ₜ[R] 1) = (algebra_map R C) r): + A ⊗[R] B ≃ₐ[R] C := +{ .. alg_hom_of_linear_map_tensor_product (f : A ⊗[R] B →ₗ[R] C) w₁ w₂, + .. f } + +@[simp] +lemma alg_equiv_of_linear_equiv_tensor_product_apply (f w₁ w₂ x) : + (alg_equiv_of_linear_equiv_tensor_product f w₁ w₂ : A ⊗[R] B ≃ₐ[R] C) x = f x := rfl + +/-- +Build an algebra equivalence from a linear equivalence out of a triple tensor product, +and evidence of multiplicativity on pure tensors. +-/ +def alg_equiv_of_linear_equiv_triple_tensor_product + (f : ((A ⊗[R] B) ⊗[R] C) ≃ₗ[R] D) + (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C), + f ((a₁ * a₂) ⊗ₜ (b₁ * b₂) ⊗ₜ (c₁ * c₂)) = f (a₁ ⊗ₜ b₁ ⊗ₜ c₁) * f (a₂ ⊗ₜ b₂ ⊗ₜ c₂)) + (w₂ : ∀ r, f (((algebra_map R A) r ⊗ₜ[R] (1 : B)) ⊗ₜ[R] (1 : C)) = (algebra_map R D) r) : + (A ⊗[R] B) ⊗[R] C ≃ₐ[R] D := +{ to_fun := f, + map_mul' := λ x y, + begin + apply tensor_product.induction_on x, + { simp only [map_zero, zero_mul] }, + { intros ab₁ c₁, + apply tensor_product.induction_on y, + { simp only [map_zero, mul_zero] }, + { intros ab₂ c₂, + apply tensor_product.induction_on ab₁, + { simp only [zero_tmul, map_zero, zero_mul] }, + { intros a₁ b₁, + apply tensor_product.induction_on ab₂, + { simp only [zero_tmul, map_zero, mul_zero] }, + { intros, simp only [tmul_mul_tmul, w₁] }, + { intros x₁ x₂ h₁ h₂, + simp only [tmul_mul_tmul] at h₁ h₂, + simp only [tmul_mul_tmul, mul_add, add_tmul, map_add, h₁, h₂] } }, + { intros x₁ x₂ h₁ h₂, + simp only [tmul_mul_tmul] at h₁ h₂, + simp only [tmul_mul_tmul, add_mul, add_tmul, map_add, h₁, h₂] } }, + { intros x₁ x₂ h₁ h₂, + simp only [tmul_mul_tmul, map_add, mul_add, add_mul, h₁, h₂], }, }, + { intros x₁ x₂ h₁ h₂, + simp only [tmul_mul_tmul, map_add, mul_add, add_mul, h₁, h₂], } + end, + commutes' := λ r, by simp [w₂], + .. f } + +@[simp] +lemma alg_equiv_of_linear_equiv_triple_tensor_product_apply (f w₁ w₂ x) : + (alg_equiv_of_linear_equiv_triple_tensor_product f w₁ w₂ : (A ⊗[R] B) ⊗[R] C ≃ₐ[R] D) x = f x := +rfl + +end + +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] +variables {C : Type v₃} [semiring C] [algebra R C] +variables {D : Type v₄} [semiring D] [algebra R D] + +section +variables (R A) +/-- +The base ring is a left identity for the tensor product of algebra, up to algebra isomorphism. +-/ +protected def lid : R ⊗[R] A ≃ₐ[R] A := +alg_equiv_of_linear_equiv_tensor_product (tensor_product.lid R A) +(by simp [mul_smul]) (by simp [algebra.smul_def]) + +@[simp] theorem lid_tmul (r : R) (a : A) : + (tensor_product.lid R A : (R ⊗ A → A)) (r ⊗ₜ a) = r • a := +by simp [tensor_product.lid] + +/-- +The base ring is a right identity for the tensor product of algebra, up to algebra isomorphism. +-/ +protected def rid : A ⊗[R] R ≃ₐ[R] A := +alg_equiv_of_linear_equiv_tensor_product (tensor_product.rid R A) +(by simp [mul_smul]) (by simp [algebra.smul_def]) + +@[simp] theorem rid_tmul (r : R) (a : A) : + (tensor_product.rid R A : (A ⊗ R → A)) (a ⊗ₜ r) = r • a := +by simp [tensor_product.rid] + +section +variables (R A B) + +/-- +The tensor product of R-algebras is commutative, up to algebra isomorphism. +-/ +protected def comm : A ⊗[R] B ≃ₐ[R] B ⊗[R] A := +alg_equiv_of_linear_equiv_tensor_product (tensor_product.comm R A B) +(by simp) +(λ r, begin + transitivity r • ((1 : B) ⊗ₜ[R] (1 : A)), + { rw [←tmul_smul, algebra.smul_def], simp, }, + { simp [algebra.smul_def], }, +end) + +@[simp] +theorem comm_tmul (a : A) (b : B) : + (tensor_product.comm R A B : (A ⊗[R] B → B ⊗[R] A)) (a ⊗ₜ b) = (b ⊗ₜ a) := +by simp [tensor_product.comm] + +lemma adjoin_tmul_eq_top : adjoin R {t : A ⊗[R] B | ∃ a b, a ⊗ₜ[R] b = t} = ⊤ := +top_le_iff.mp $ (top_le_iff.mpr $ span_tmul_eq_top R A B).trans (span_le_adjoin R _) + +end + +section +variables {R A B C} + +lemma assoc_aux_1 (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C) : + (tensor_product.assoc R A B C) (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) = + (tensor_product.assoc R A B C) ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * + (tensor_product.assoc R A B C) ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂) := +rfl + +lemma assoc_aux_2 (r : R) : + (tensor_product.assoc R A B C) (((algebra_map R A) r ⊗ₜ[R] 1) ⊗ₜ[R] 1) = + (algebra_map R (A ⊗ (B ⊗ C))) r := rfl + +variables (R A B C) + +/-- The associator for tensor product of R-algebras, as an algebra isomorphism. -/ +protected def assoc : ((A ⊗[R] B) ⊗[R] C) ≃ₐ[R] (A ⊗[R] (B ⊗[R] C)) := +alg_equiv_of_linear_equiv_triple_tensor_product + (tensor_product.assoc.{u v₁ v₂ v₃} R A B C : (A ⊗ B ⊗ C) ≃ₗ[R] (A ⊗ (B ⊗ C))) + (@algebra.tensor_product.assoc_aux_1.{u v₁ v₂ v₃} R _ A _ _ B _ _ C _ _) + (@algebra.tensor_product.assoc_aux_2.{u v₁ v₂ v₃} R _ A _ _ B _ _ C _ _) + +variables {R A B C} + +@[simp] theorem assoc_tmul (a : A) (b : B) (c : C) : + ((tensor_product.assoc R A B C) : + (A ⊗[R] B) ⊗[R] C → A ⊗[R] (B ⊗[R] C)) ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c) := +rfl + +end + +variables {R A B C D} + +/-- The tensor product of a pair of algebra morphisms. -/ +def map (f : A →ₐ[R] B) (g : C →ₐ[R] D) : A ⊗[R] C →ₐ[R] B ⊗[R] D := +alg_hom_of_linear_map_tensor_product + (tensor_product.map f.to_linear_map g.to_linear_map) + (by simp) + (by simp [alg_hom.commutes]) + +@[simp] theorem map_tmul (f : A →ₐ[R] B) (g : C →ₐ[R] D) (a : A) (c : C) : + map f g (a ⊗ₜ c) = f a ⊗ₜ g c := +rfl + +@[simp] lemma map_comp_include_left (f : A →ₐ[R] B) (g : C →ₐ[R] D) : + (map f g).comp include_left = include_left.comp f := alg_hom.ext $ by simp + +@[simp] lemma map_comp_include_right (f : A →ₐ[R] B) (g : C →ₐ[R] D) : + (map f g).comp include_right = include_right.comp g := alg_hom.ext $ by simp + +lemma map_range (f : A →ₐ[R] B) (g : C →ₐ[R] D) : + (map f g).range = (include_left.comp f).range ⊔ (include_right.comp g).range := +begin + apply le_antisymm, + { rw [←map_top, ←adjoin_tmul_eq_top, ←adjoin_image, adjoin_le_iff], + rintros _ ⟨_, ⟨a, b, rfl⟩, rfl⟩, + rw [map_tmul, ←_root_.mul_one (f a), ←_root_.one_mul (g b), ←tmul_mul_tmul], + exact mul_mem_sup (alg_hom.mem_range_self _ a) (alg_hom.mem_range_self _ b) }, + { rw [←map_comp_include_left f g, ←map_comp_include_right f g], + exact sup_le (alg_hom.range_comp_le_range _ _) (alg_hom.range_comp_le_range _ _) }, +end + +/-- +Construct an isomorphism between tensor products of R-algebras +from isomorphisms between the tensor factors. +-/ +def congr (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) : A ⊗[R] C ≃ₐ[R] B ⊗[R] D := +alg_equiv.of_alg_hom (map f g) (map f.symm g.symm) + (ext $ λ b d, by simp) + (ext $ λ a c, by simp) + +@[simp] +lemma congr_apply (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) (x) : + congr f g x = (map (f : A →ₐ[R] B) (g : C →ₐ[R] D)) x := rfl + +@[simp] +lemma congr_symm_apply (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) (x) : + (congr f g).symm x = (map (f.symm : B →ₐ[R] A) (g.symm : D →ₐ[R] C)) x := rfl + +end + +end monoidal + +section + +variables {R A B S : Type*} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S] +variables [algebra R A] [algebra R B] [algebra R S] +variables (f : A →ₐ[R] S) (g : B →ₐ[R] S) + +variables (R) + +/-- `linear_map.mul'` is an alg_hom on commutative rings. -/ +def lmul' : S ⊗[R] S →ₐ[R] S := +alg_hom_of_linear_map_tensor_product (linear_map.mul' R S) + (λ a₁ a₂ b₁ b₂, by simp only [linear_map.mul'_apply, mul_mul_mul_comm]) + (λ r, by simp only [linear_map.mul'_apply, _root_.mul_one]) + +variables {R} + +lemma lmul'_to_linear_map : (lmul' R : _ →ₐ[R] S).to_linear_map = linear_map.mul' R S := rfl + +@[simp] lemma lmul'_apply_tmul (a b : S) : lmul' R (a ⊗ₜ[R] b) = a * b := rfl + +@[simp] +lemma lmul'_comp_include_left : (lmul' R : _ →ₐ[R] S).comp include_left = alg_hom.id R S := +alg_hom.ext $ _root_.mul_one + +@[simp] +lemma lmul'_comp_include_right : (lmul' R : _ →ₐ[R] S).comp include_right = alg_hom.id R S := +alg_hom.ext $ _root_.one_mul + +/-- +If `S` is commutative, for a pair of morphisms `f : A →ₐ[R] S`, `g : B →ₐ[R] S`, +We obtain a map `A ⊗[R] B →ₐ[R] S` that commutes with `f`, `g` via `a ⊗ b ↦ f(a) * g(b)`. +-/ +def product_map : A ⊗[R] B →ₐ[R] S := (lmul' R).comp (tensor_product.map f g) + +@[simp] lemma product_map_apply_tmul (a : A) (b : B) : product_map f g (a ⊗ₜ b) = f a * g b := +by { unfold product_map lmul', simp } + +lemma product_map_left_apply (a : A) : + product_map f g ((include_left : A →ₐ[R] A ⊗ B) a) = f a := by simp + +@[simp] lemma product_map_left : (product_map f g).comp include_left = f := alg_hom.ext $ by simp + +lemma product_map_right_apply (b : B) : product_map f g (include_right b) = g b := by simp + +@[simp] lemma product_map_right : (product_map f g).comp include_right = g := alg_hom.ext $ by simp + +lemma product_map_range : (product_map f g).range = f.range ⊔ g.range := +by rw [product_map, alg_hom.range_comp, map_range, map_sup, ←alg_hom.range_comp, + ←alg_hom.range_comp, ←alg_hom.comp_assoc, ←alg_hom.comp_assoc, lmul'_comp_include_left, + lmul'_comp_include_right, alg_hom.id_comp, alg_hom.id_comp] + +end +section + +variables {R A A' B S : Type*} +variables [comm_semiring R] [comm_semiring A] [semiring A'] [semiring B] [comm_semiring S] +variables [algebra R A] [algebra R A'] [algebra A A'] [is_scalar_tower R A A'] [algebra R B] +variables [algebra R S] [algebra A S] [is_scalar_tower R A S] + +/-- If `A`, `B` are `R`-algebras, `A'` is an `A`-algebra, then the product map of `f : A' →ₐ[A] S` +and `g : B →ₐ[R] S` is an `A`-algebra homomorphism. -/ +@[simps] def product_left_alg_hom (f : A' →ₐ[A] S) (g : B →ₐ[R] S) : A' ⊗[R] B →ₐ[A] S := +{ commutes' := λ r, by { dsimp, simp }, + ..(product_map (f.restrict_scalars R) g).to_ring_hom } + +end +section basis + +variables {k : Type*} [comm_ring k] (R : Type*) [ring R] [algebra k R] {M : Type*} + [add_comm_monoid M] [module k M] {ι : Type*} (b : basis ι k M) + +/-- Given a `k`-algebra `R` and a `k`-basis of `M,` this is a `k`-linear isomorphism +`R ⊗[k] M ≃ (ι →₀ R)` (which is in fact `R`-linear). -/ +noncomputable def basis_aux : R ⊗[k] M ≃ₗ[k] (ι →₀ R) := +(_root_.tensor_product.congr (finsupp.linear_equiv.finsupp_unique k R punit).symm b.repr) ≪≫ₗ + (finsupp_tensor_finsupp k R k punit ι).trans (finsupp.lcongr (equiv.unique_prod ι punit) + (_root_.tensor_product.rid k R)) + +variables {R} + +lemma basis_aux_tmul (r : R) (m : M) : + basis_aux R b (r ⊗ₜ m) = r • (finsupp.map_range (algebra_map k R) + (map_zero _) (b.repr m)) := +begin + ext, + simp [basis_aux, ←algebra.commutes, algebra.smul_def], +end + +lemma basis_aux_map_smul (r : R) (x : R ⊗[k] M) : + basis_aux R b (r • x) = r • basis_aux R b x := +tensor_product.induction_on x (by simp) (λ x y, by simp only [tensor_product.smul_tmul', + basis_aux_tmul, smul_assoc]) (λ x y hx hy, by simp [hx, hy]) + +variables (R) + +/-- Given a `k`-algebra `R`, this is the `R`-basis of `R ⊗[k] M` induced by a `k`-basis of `M`. -/ +noncomputable def basis : basis ι R (R ⊗[k] M) := +{ repr := { map_smul' := basis_aux_map_smul b, .. basis_aux R b } } + +variables {R} + +@[simp] lemma basis_repr_tmul (r : R) (m : M) : + (basis R b).repr (r ⊗ₜ m) = r • (finsupp.map_range (algebra_map k R) (map_zero _) (b.repr m)) := +basis_aux_tmul _ _ _ + +@[simp] lemma basis_repr_symm_apply (r : R) (i : ι) : + (basis R b).repr.symm (finsupp.single i r) = r ⊗ₜ b.repr.symm (finsupp.single i 1) := +by simp [basis, equiv.unique_prod_symm_apply, basis_aux] + +end basis +end tensor_product +end algebra + +namespace module + +variables {R M N : Type*} [comm_semiring R] +variables [add_comm_monoid M] [add_comm_monoid N] +variables [module R M] [module R N] + +/-- The algebra homomorphism from `End M ⊗ End N` to `End (M ⊗ N)` sending `f ⊗ₜ g` to +the `tensor_product.map f g`, the tensor product of the two maps. -/ +def End_tensor_End_alg_hom : (End R M) ⊗[R] (End R N) →ₐ[R] End R (M ⊗[R] N) := +begin + refine algebra.tensor_product.alg_hom_of_linear_map_tensor_product + (hom_tensor_hom_map R M N M N) _ _, + { intros f₁ f₂ g₁ g₂, + simp only [hom_tensor_hom_map_apply, tensor_product.map_mul] }, + { intro r, + simp only [hom_tensor_hom_map_apply], + ext m n, simp [smul_tmul] } +end + +lemma End_tensor_End_alg_hom_apply (f : End R M) (g : End R N) : + End_tensor_End_alg_hom (f ⊗ₜ[R] g) = tensor_product.map f g := +by simp only [End_tensor_End_alg_hom, + algebra.tensor_product.alg_hom_of_linear_map_tensor_product_apply, hom_tensor_hom_map_apply] + +end module + +lemma subalgebra.finite_dimensional_sup {K L : Type*} [field K] [comm_ring L] [algebra K L] + (E1 E2 : subalgebra K L) [finite_dimensional K E1] [finite_dimensional K E2] : + finite_dimensional K ↥(E1 ⊔ E2) := +begin + rw [←E1.range_val, ←E2.range_val, ←algebra.tensor_product.product_map_range], + exact (algebra.tensor_product.product_map E1.val E2.val).to_linear_map.finite_dimensional_range, +end + +namespace tensor_product.algebra + +variables {R A B M : Type*} +variables [comm_semiring R] [add_comm_monoid M] [module R M] +variables [semiring A] [semiring B] [module A M] [module B M] +variables [algebra R A] [algebra R B] +variables [is_scalar_tower R A M] [is_scalar_tower R B M] + +/-- An auxiliary definition, used for constructing the `module (A ⊗[R] B) M` in +`tensor_product.algebra.module` below. -/ +def module_aux : A ⊗[R] B →ₗ[R] M →ₗ[R] M := +tensor_product.lift +{ to_fun := λ a, a • (algebra.lsmul R M : B →ₐ[R] module.End R M).to_linear_map, + map_add' := λ r t, by { ext, simp only [add_smul, linear_map.add_apply] }, + map_smul' := λ n r, by { ext, simp only [ring_hom.id_apply, linear_map.smul_apply, smul_assoc] } } + +lemma module_aux_apply (a : A) (b : B) (m : M) : + module_aux (a ⊗ₜ[R] b) m = a • b • m := rfl + +variables [smul_comm_class A B M] + +/-- If `M` is a representation of two different `R`-algebras `A` and `B` whose actions commute, +then it is a representation the `R`-algebra `A ⊗[R] B`. + +An important example arises from a semiring `S`; allowing `S` to act on itself via left and right +multiplication, the roles of `R`, `A`, `B`, `M` are played by `ℕ`, `S`, `Sᵐᵒᵖ`, `S`. This example +is important because a submodule of `S` as a `module` over `S ⊗[ℕ] Sᵐᵒᵖ` is a two-sided ideal. + +NB: This is not an instance because in the case `B = A` and `M = A ⊗[R] A` we would have a diamond +of `smul` actions. Furthermore, this would not be a mere definitional diamond but a true +mathematical diamond in which `A ⊗[R] A` had two distinct scalar actions on itself: one from its +multiplication, and one from this would-be instance. Arguably we could live with this but in any +case the real fix is to address the ambiguity in notation, probably along the lines outlined here: +https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929258 +-/ +protected def module : module (A ⊗[R] B) M := +{ smul := λ x m, module_aux x m, + zero_smul := λ m, by simp only [map_zero, linear_map.zero_apply], + smul_zero := λ x, by simp only [map_zero], + smul_add := λ x m₁ m₂, by simp only [map_add], + add_smul := λ x y m, by simp only [map_add, linear_map.add_apply], + one_smul := λ m, by simp only [module_aux_apply, algebra.tensor_product.one_def, one_smul], + mul_smul := λ x y m, + begin + apply tensor_product.induction_on x; + apply tensor_product.induction_on y, + { simp only [mul_zero, map_zero, linear_map.zero_apply], }, + { intros a b, simp only [zero_mul, map_zero, linear_map.zero_apply], }, + { intros z w hz hw, simp only [zero_mul, map_zero, linear_map.zero_apply], }, + { intros a b, simp only [mul_zero, map_zero, linear_map.zero_apply], }, + { intros a₁ b₁ a₂ b₂, + simp only [module_aux_apply, mul_smul, smul_comm a₁ b₂, algebra.tensor_product.tmul_mul_tmul, + linear_map.mul_apply], }, + { intros z w hz hw a b, + simp only at hz hw, + simp only [mul_add, hz, hw, map_add, linear_map.add_apply], }, + { intros z w hz hw, simp only [mul_zero, map_zero, linear_map.zero_apply], }, + { intros a b z w hz hw, + simp only at hz hw, + simp only [map_add, add_mul, linear_map.add_apply, hz, hw], }, + { intros u v hu hv z w hz hw, + simp only at hz hw, + simp only [add_mul, hz, hw, map_add, linear_map.add_apply], }, + end } + +local attribute [instance] tensor_product.algebra.module + +lemma smul_def (a : A) (b : B) (m : M) : (a ⊗ₜ[R] b) • m = a • b • m := rfl + +end tensor_product.algebra diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean new file mode 100644 index 000000000..0d163875d --- /dev/null +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -0,0 +1,19 @@ +import linear_algebra.clifford_algebra.basic +import data.complex.module +import ring_theory.tensor_product +import for_mathlib.linear_algebra.bilinear_form.tensor_product + +variables {V: Type*} [add_comm_group V] [module ℝ V] +. + +open_locale tensor_product + +#check bilin_form.tmul + +def quadratic_form.complexify (Q : quadratic_form ℝ V) : + quadratic_form ℂ (ℂ ⊗[ℝ] V) := +{ to_fun := , + to_fun_smul := _, + exists_companion' := _ } +-- bilin_form.to_quadratic_form $ +-- (bilin_form.tmul _ Q.associated) \ No newline at end of file From 9c82583ea08c95e49c330dd39cf8a9a4eaa3c014 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 20:31:48 +0000 Subject: [PATCH 02/23] wip --- .../linear_algebra/bilinear_form/basic.lean | 16 + .../bilinear_form/tensor_product.lean | 5 +- .../ring_theory/tensor_product.lean | 905 ++---------------- 3 files changed, 100 insertions(+), 826 deletions(-) diff --git a/src/for_mathlib/linear_algebra/bilinear_form/basic.lean b/src/for_mathlib/linear_algebra/bilinear_form/basic.lean index e69de29bb..d2f43a226 100644 --- a/src/for_mathlib/linear_algebra/bilinear_form/basic.lean +++ b/src/for_mathlib/linear_algebra/bilinear_form/basic.lean @@ -0,0 +1,16 @@ +import linear_algebra.bilinear_form + +namespace bilin_form + +variables {α β R M : Type*} +variables [semiring R] [add_comm_monoid M] [module R M] +variables [monoid α] [monoid β] [distrib_mul_action α R] [distrib_mul_action β R] +variables [smul_comm_class α R R] [smul_comm_class β R R] + +instance [smul_comm_class α β R] : smul_comm_class α β (bilin_form R M) := +⟨λ a b B, ext $ λ x y, smul_comm _ _ _⟩ + +instance [has_smul α β] [is_scalar_tower α β R] : is_scalar_tower α β (bilin_form R M) := +⟨λ a b B, ext $ λ x y, smul_assoc _ _ _⟩ + +end bilin_form \ No newline at end of file diff --git a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean index 21909f5d8..fadb6dc08 100644 --- a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean +++ b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean @@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ import linear_algebra.bilinear_form.tensor_product -import ring_theory.tensor_product +import for_mathlib.ring_theory.tensor_product import linear_algebra.quadratic_form.basic import data.is_R_or_C.basic import for_mathlib.linear_algebra.tensor_product +import for_mathlib.linear_algebra.bilinear_form.basic universes u v w variables {ι : Type*} {R S : Type*} {M₁ M₂ : Type*} @@ -63,7 +64,7 @@ def tensor_distrib' : bilin_form S M₁ ⊗[R] bilin_form R M₂ →ₗ[S] bilin ≪≫ₗ (tensor_product.lift.equiv S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) S).symm ≪≫ₗ linear_map.to_bilin).to_linear_map ∘ₗ _ - ∘ₗ (tensor_product.congr + ∘ₗ (tensor_product.algebra_tensor_module.congr (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv S M₁ M₁ S) (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv R M₂ M₂ R)).to_linear_map diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 8b5c83d56..2f207c039 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -1,4 +1,5 @@ import ring_theory.tensor_product +import linear_algebra.dual universes u v₁ v₂ v₃ v₄ @@ -26,7 +27,7 @@ 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] variables [add_comm_monoid Q] [module R Q] -/-- The tensor product of a pair of linear maps between modules. -/ +/-- . -/ def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] Q := lift $ (show (Q →ₗ[R] P ⊗ Q) →ₗ[A] N →ₗ[R] P ⊗[R] Q, from{ to_fun := λ h, h ∘ₗ g, @@ -37,6 +38,42 @@ lift $ (show (Q →ₗ[R] P ⊗ Q) →ₗ[A] N →ₗ[R] P ⊗[R] Q, map f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl +lemma map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (f₁ + f₂) g = map f₁ g + map f₂ g := +begin + ext, + simp_rw [curry_apply, tensor_product.curry_apply, restrict_scalars_apply, add_apply, map_tmul, + add_apply, add_tmul], +end + +lemma map_add_right (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) : map f (g₁ + g₂) = map f g₁ + map f g₂ := +begin + ext, + simp_rw [curry_apply, tensor_product.curry_apply, restrict_scalars_apply, add_apply, map_tmul, + add_apply, tmul_add], +end + +lemma map_smul_left (r : A) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (r • f) g = r • map f g := +begin + ext, + simp_rw [curry_apply, tensor_product.curry_apply, restrict_scalars_apply, smul_apply, map_tmul, + smul_apply, smul_tmul'], +end + +lemma map_smul_right (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map f (r • g) = r • map f g := +begin + ext, + simp_rw [curry_apply, tensor_product.curry_apply, restrict_scalars_apply, smul_apply, map_tmul, + smul_apply, tmul_smul], +end + +/-- Heterobasic `map_bilinear` -/ +def map_bilinear : (M →ₗ[A] P) →ₗ[A] (N →ₗ[R] Q) →ₗ[R] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := +{ to_fun := λ f, + { to_fun := λ g, map f g, + map_add' := λ g₁ g₂, map_add_right _ _ _, + map_smul' := λ c g, map_smul_right _ _ _, }, + map_add' := λ f₁ f₂, linear_map.ext $ λ g, map_add_left _ _ _, + map_smul' := λ c f, linear_map.ext $ λ g, map_smul_left _ _ _, } def congr (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : (M ⊗[R] N) ≃ₗ[A] (P ⊗[R] Q) := linear_equiv.of_linear (map f g) (map f.symm g.symm) @@ -51,15 +88,8 @@ rfl (congr f g).symm (p ⊗ₜ q) = f.symm p ⊗ₜ g.symm q := rfl - variables (R A M N P Q) -notation (name := tensor_product') - M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N - - - -#check assoc R A M /-- A tensor product analogue of `mul_left_comm`. -/ def left_comm : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q) := let e₁ := (assoc R A M Q P).symm, @@ -67,829 +97,56 @@ let e₁ := (assoc R A M Q P).symm, e₃ := (assoc R A P Q M) in e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) -/-- Heterobasic version of `tensor_tensor_tensor_comm`: - -Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ -def tensor_tensor_tensor_comm : - (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := -(assoc R A (M ⊗[R] N) Q P).symm ≪≫ₗ _ --- let e₁ := assoc R A M N (P ⊗[R] Q), --- e₂ := congr (1 : M ≃ₗ[A] M) (left_comm R R N P Q), --- e₃ := (assoc R A M P (N ⊗[R] Q)).symm in --- e₁ ≪≫ₗ _ ≪≫ₗ e₃ -- (e₂ ≪≫ₗ e₃) - -- (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, simp only [curry_apply, tensor_product.curry_apply, mk_apply, tensor_product.mk_apply, - -- uncurry_apply, tensor_product.uncurry_apply, id_apply, lift_tmul, compr₂_apply, - -- restrict_scalars_apply, function.comp_app, to_fun_eq_coe, lcurry_apply, - -- linear_map.comp_apply] }) - -#check tensor_tensor_tensor_comm - -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 (linear_map.mul R A a) x) = - (rtensor N ((linear_map.mul R A) a)) ((ltensor A f) x), - by { rw [← comp_apply, ← comp_apply], - simp only [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`, -for a fixed pure tensor in the first argument, -as an `R`-linear map. --/ -def mul_aux (a₁ : A) (b₁ : B) : (A ⊗[R] B) →ₗ[R] (A ⊗[R] B) := -tensor_product.map (linear_map.mul_left R a₁) (linear_map.mul_left R b₁) - -@[simp] -lemma mul_aux_apply (a₁ a₂ : A) (b₁ b₂ : B) : - (mul_aux a₁ b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) := -rfl - -/-- -(Implementation detail) -The multiplication map on `A ⊗[R] B`, -as an `R`-bilinear map. --/ -def mul : (A ⊗[R] B) →ₗ[R] (A ⊗[R] B) →ₗ[R] (A ⊗[R] B) := -tensor_product.lift $ linear_map.mk₂ R mul_aux - (λ x₁ x₂ y, tensor_product.ext' $ λ x' y', - by simp only [mul_aux_apply, linear_map.add_apply, add_mul, add_tmul]) - (λ c x y, tensor_product.ext' $ λ x' y', - by simp only [mul_aux_apply, linear_map.smul_apply, smul_tmul', smul_mul_assoc]) - (λ x y₁ y₂, tensor_product.ext' $ λ x' y', - by simp only [mul_aux_apply, linear_map.add_apply, add_mul, tmul_add]) - (λ c x y, tensor_product.ext' $ λ x' y', - by simp only [mul_aux_apply, linear_map.smul_apply, smul_tmul, smul_tmul', smul_mul_assoc]) - -@[simp] -lemma mul_apply (a₁ a₂ : A) (b₁ b₂ : B) : - mul (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) := -rfl - -lemma mul_assoc' (mul : (A ⊗[R] B) →ₗ[R] (A ⊗[R] B) →ₗ[R] (A ⊗[R] B)) - (h : ∀ (a₁ a₂ a₃ : A) (b₁ b₂ b₃ : B), - mul (mul (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂)) (a₃ ⊗ₜ[R] b₃) = - mul (a₁ ⊗ₜ[R] b₁) (mul (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃))) : - ∀ (x y z : A ⊗[R] B), mul (mul x y) z = mul x (mul y z) := -begin - intros, - apply tensor_product.induction_on x, - { simp only [linear_map.map_zero, linear_map.zero_apply], }, - apply tensor_product.induction_on y, - { simp only [linear_map.map_zero, forall_const, linear_map.zero_apply], }, - apply tensor_product.induction_on z, - { simp only [linear_map.map_zero, forall_const], }, - { intros, simp only [h], }, - { intros, simp only [linear_map.map_add, *], }, - { intros, simp only [linear_map.map_add, *, linear_map.add_apply], }, - { intros, simp only [linear_map.map_add, *, linear_map.add_apply], }, -end - -lemma mul_assoc (x y z : A ⊗[R] B) : mul (mul x y) z = mul x (mul y z) := -mul_assoc' mul (by { intros, simp only [mul_apply, mul_assoc], }) x y z - -lemma one_mul (x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x := -begin - apply tensor_product.induction_on x; - simp {contextual := tt}, -end - -lemma mul_one (x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x := -begin - apply tensor_product.induction_on x; - simp {contextual := tt}, -end - -instance : has_one (A ⊗[R] B) := -{ one := 1 ⊗ₜ 1 } - -instance : add_monoid_with_one (A ⊗[R] B) := add_monoid_with_one.unary - -instance : semiring (A ⊗[R] B) := -{ zero := 0, - add := (+), - one := 1, - mul := λ a b, mul a b, - one_mul := one_mul, - mul_one := mul_one, - mul_assoc := mul_assoc, - zero_mul := by simp, - mul_zero := by simp, - left_distrib := by simp, - right_distrib := by simp, - .. (by apply_instance : add_monoid_with_one (A ⊗[R] B)), - .. (by apply_instance : add_comm_monoid (A ⊗[R] B)) }. - -lemma one_def : (1 : A ⊗[R] B) = (1 : A) ⊗ₜ (1 : B) := rfl - -@[simp] -lemma tmul_mul_tmul (a₁ a₂ : A) (b₁ b₂ : B) : - (a₁ ⊗ₜ[R] b₁) * (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) := -rfl - -@[simp] -lemma tmul_pow (a : A) (b : B) (k : ℕ) : - (a ⊗ₜ[R] b)^k = (a^k) ⊗ₜ[R] (b^k) := -begin - induction k with k ih, - { simp [one_def], }, - { simp [pow_succ, ih], } -end - - -/-- The ring morphism `A →+* A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/ -@[simps] -def include_left_ring_hom : A →+* A ⊗[R] B := -{ to_fun := λ a, a ⊗ₜ 1, - map_zero' := by simp, - map_add' := by simp [add_tmul], - map_one' := rfl, - map_mul' := by simp } - -variables {S : Type*} [comm_semiring S] [algebra S A] - -instance left_algebra [smul_comm_class R S A] : algebra S (A ⊗[R] B) := -{ commutes' := λ r x, - begin - apply tensor_product.induction_on x, - { simp, }, - { intros a b, dsimp, rw [algebra.commutes, _root_.mul_one, _root_.one_mul], }, - { intros y y' h h', dsimp at h h' ⊢, simp only [mul_add, add_mul, h, h'], }, - end, - smul_def' := λ r x, - begin - apply tensor_product.induction_on x, - { simp [smul_zero], }, - { intros a b, dsimp, rw [tensor_product.smul_tmul', algebra.smul_def r a, _root_.one_mul] }, - { intros, dsimp, simp [smul_add, mul_add, *], }, - end, - .. tensor_product.include_left_ring_hom.comp (algebra_map S A), - .. (by apply_instance : module S (A ⊗[R] B)) }. - --- This is for the `undergrad.yaml` list. -/-- The tensor product of two `R`-algebras is an `R`-algebra. -/ -instance : algebra R (A ⊗[R] B) := infer_instance - -@[simp] -lemma algebra_map_apply [smul_comm_class R S A] (r : S) : - (algebra_map S (A ⊗[R] B)) r = ((algebra_map S A) r) ⊗ₜ 1 := rfl - -variables {C : Type v₃} [semiring C] [algebra R C] - -@[ext] -theorem ext {g h : (A ⊗[R] B) →ₐ[R] C} - (H : ∀ a b, g (a ⊗ₜ b) = h (a ⊗ₜ b)) : g = h := -begin - apply @alg_hom.to_linear_map_injective R (A ⊗[R] B) C _ _ _ _ _ _ _ _, - ext, - simp [H], -end - --- TODO: with `smul_comm_class R S A` we can have this as an `S`-algebra morphism -/-- The `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/ -def include_left : A →ₐ[R] A ⊗[R] B := -{ commutes' := by simp, - ..include_left_ring_hom } - -@[simp] -lemma include_left_apply (a : A) : (include_left : A →ₐ[R] A ⊗[R] B) a = a ⊗ₜ 1 := rfl - -/-- The algebra morphism `B →ₐ[R] A ⊗[R] B` sending `b` to `1 ⊗ₜ b`. -/ -def include_right : B →ₐ[R] A ⊗[R] B := -{ to_fun := λ b, 1 ⊗ₜ b, - map_zero' := by simp, - map_add' := by simp [tmul_add], - map_one' := rfl, - map_mul' := by simp, - commutes' := λ r, - begin - simp only [algebra_map_apply], - transitivity r • ((1 : A) ⊗ₜ[R] (1 : B)), - { rw [←tmul_smul, algebra.smul_def], simp, }, - { simp [algebra.smul_def], }, - end, } - -@[simp] -lemma include_right_apply (b : B) : (include_right : B →ₐ[R] A ⊗[R] B) b = 1 ⊗ₜ b := rfl - -lemma include_left_comp_algebra_map {R S T : Type*} [comm_ring R] [comm_ring S] [comm_ring T] - [algebra R S] [algebra R T] : - (include_left.to_ring_hom.comp (algebra_map R S) : R →+* S ⊗[R] T) = - include_right.to_ring_hom.comp (algebra_map R T) := -by { ext, simp } - -end semiring - -section ring - -variables {R : Type u} [comm_ring R] -variables {A : Type v₁} [ring A] [algebra R A] -variables {B : Type v₂} [ring B] [algebra R B] - -instance : ring (A ⊗[R] B) := -{ .. (by apply_instance : add_comm_group (A ⊗[R] B)), - .. (by apply_instance : semiring (A ⊗[R] B)) }. - -end ring - -section comm_ring - -variables {R : Type u} [comm_ring R] -variables {A : Type v₁} [comm_ring A] [algebra R A] -variables {B : Type v₂} [comm_ring B] [algebra R B] - -instance : comm_ring (A ⊗[R] B) := -{ mul_comm := λ x y, - begin - apply tensor_product.induction_on x, - { simp, }, - { intros a₁ b₁, - apply tensor_product.induction_on y, - { simp, }, - { intros a₂ b₂, - simp [mul_comm], }, - { intros a₂ b₂ ha hb, - simp [mul_add, add_mul, ha, hb], }, }, - { intros x₁ x₂ h₁ h₂, - simp [mul_add, add_mul, h₁, h₂], }, - end - .. (by apply_instance : ring (A ⊗[R] B)) }. - -section right_algebra - -/-- `S ⊗[R] T` has a `T`-algebra structure. This is not a global instance or else the action of -`S` on `S ⊗[R] S` would be ambiguous. -/ -@[reducible] def right_algebra : algebra B (A ⊗[R] B) := -(algebra.tensor_product.include_right.to_ring_hom : B →+* A ⊗[R] B).to_algebra - -local attribute [instance] tensor_product.right_algebra - -instance right_is_scalar_tower : is_scalar_tower R B (A ⊗[R] B) := -is_scalar_tower.of_algebra_map_eq (λ r, (algebra.tensor_product.include_right.commutes r).symm) - -end right_algebra - -end comm_ring - -/-- -Verify that typeclass search finds the ring structure on `A ⊗[ℤ] B` -when `A` and `B` are merely rings, by treating both as `ℤ`-algebras. --/ -example {A : Type v₁} [ring A] {B : Type v₂} [ring B] : ring (A ⊗[ℤ] B) := -by apply_instance - -/-- -Verify that typeclass search finds the comm_ring structure on `A ⊗[ℤ] B` -when `A` and `B` are merely comm_rings, by treating both as `ℤ`-algebras. --/ -example {A : Type v₁} [comm_ring A] {B : Type v₂} [comm_ring B] : comm_ring (A ⊗[ℤ] B) := -by apply_instance - -/-! -We now build the structure maps for the symmetric monoidal category of `R`-algebras. --/ -section monoidal - -section -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] -variables {C : Type v₃} [semiring C] [algebra R C] -variables {D : Type v₄} [semiring D] [algebra R D] - -/-- -Build an algebra morphism from a linear map out of a tensor product, -and evidence of multiplicativity on pure tensors. --/ -def alg_hom_of_linear_map_tensor_product - (f : A ⊗[R] B →ₗ[R] C) - (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) - (w₂ : ∀ r, f ((algebra_map R A) r ⊗ₜ[R] 1) = (algebra_map R C) r): - A ⊗[R] B →ₐ[R] C := -{ map_one' := by rw [←(algebra_map R C).map_one, ←w₂, (algebra_map R A).map_one]; refl, - map_zero' := by rw [linear_map.to_fun_eq_coe, map_zero], - map_mul' := λ x y, by - { rw linear_map.to_fun_eq_coe, - apply tensor_product.induction_on x, - { rw [zero_mul, map_zero, zero_mul] }, - { intros a₁ b₁, - apply tensor_product.induction_on y, - { rw [mul_zero, map_zero, mul_zero] }, - { intros a₂ b₂, - rw [tmul_mul_tmul, w₁] }, - { intros x₁ x₂ h₁ h₂, - rw [mul_add, map_add, map_add, mul_add, h₁, h₂] } }, - { intros x₁ x₂ h₁ h₂, - rw [add_mul, map_add, map_add, add_mul, h₁, h₂] } }, - commutes' := λ r, by rw [linear_map.to_fun_eq_coe, algebra_map_apply, w₂], - .. f } - -@[simp] -lemma alg_hom_of_linear_map_tensor_product_apply (f w₁ w₂ x) : - (alg_hom_of_linear_map_tensor_product f w₁ w₂ : A ⊗[R] B →ₐ[R] C) x = f x := rfl - -/-- -Build an algebra equivalence from a linear equivalence out of a tensor product, -and evidence of multiplicativity on pure tensors. --/ -def alg_equiv_of_linear_equiv_tensor_product - (f : A ⊗[R] B ≃ₗ[R] C) - (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) - (w₂ : ∀ r, f ((algebra_map R A) r ⊗ₜ[R] 1) = (algebra_map R C) r): - A ⊗[R] B ≃ₐ[R] C := -{ .. alg_hom_of_linear_map_tensor_product (f : A ⊗[R] B →ₗ[R] C) w₁ w₂, - .. f } - -@[simp] -lemma alg_equiv_of_linear_equiv_tensor_product_apply (f w₁ w₂ x) : - (alg_equiv_of_linear_equiv_tensor_product f w₁ w₂ : A ⊗[R] B ≃ₐ[R] C) x = f x := rfl - -/-- -Build an algebra equivalence from a linear equivalence out of a triple tensor product, -and evidence of multiplicativity on pure tensors. --/ -def alg_equiv_of_linear_equiv_triple_tensor_product - (f : ((A ⊗[R] B) ⊗[R] C) ≃ₗ[R] D) - (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C), - f ((a₁ * a₂) ⊗ₜ (b₁ * b₂) ⊗ₜ (c₁ * c₂)) = f (a₁ ⊗ₜ b₁ ⊗ₜ c₁) * f (a₂ ⊗ₜ b₂ ⊗ₜ c₂)) - (w₂ : ∀ r, f (((algebra_map R A) r ⊗ₜ[R] (1 : B)) ⊗ₜ[R] (1 : C)) = (algebra_map R D) r) : - (A ⊗[R] B) ⊗[R] C ≃ₐ[R] D := -{ to_fun := f, - map_mul' := λ x y, - begin - apply tensor_product.induction_on x, - { simp only [map_zero, zero_mul] }, - { intros ab₁ c₁, - apply tensor_product.induction_on y, - { simp only [map_zero, mul_zero] }, - { intros ab₂ c₂, - apply tensor_product.induction_on ab₁, - { simp only [zero_tmul, map_zero, zero_mul] }, - { intros a₁ b₁, - apply tensor_product.induction_on ab₂, - { simp only [zero_tmul, map_zero, mul_zero] }, - { intros, simp only [tmul_mul_tmul, w₁] }, - { intros x₁ x₂ h₁ h₂, - simp only [tmul_mul_tmul] at h₁ h₂, - simp only [tmul_mul_tmul, mul_add, add_tmul, map_add, h₁, h₂] } }, - { intros x₁ x₂ h₁ h₂, - simp only [tmul_mul_tmul] at h₁ h₂, - simp only [tmul_mul_tmul, add_mul, add_tmul, map_add, h₁, h₂] } }, - { intros x₁ x₂ h₁ h₂, - simp only [tmul_mul_tmul, map_add, mul_add, add_mul, h₁, h₂], }, }, - { intros x₁ x₂ h₁ h₂, - simp only [tmul_mul_tmul, map_add, mul_add, add_mul, h₁, h₂], } - end, - commutes' := λ r, by simp [w₂], - .. f } - -@[simp] -lemma alg_equiv_of_linear_equiv_triple_tensor_product_apply (f w₁ w₂ x) : - (alg_equiv_of_linear_equiv_triple_tensor_product f w₁ w₂ : (A ⊗[R] B) ⊗[R] C ≃ₐ[R] D) x = f x := -rfl - -end - -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] -variables {C : Type v₃} [semiring C] [algebra R C] -variables {D : Type v₄} [semiring D] [algebra R D] - -section -variables (R A) -/-- -The base ring is a left identity for the tensor product of algebra, up to algebra isomorphism. --/ -protected def lid : R ⊗[R] A ≃ₐ[R] A := -alg_equiv_of_linear_equiv_tensor_product (tensor_product.lid R A) -(by simp [mul_smul]) (by simp [algebra.smul_def]) - -@[simp] theorem lid_tmul (r : R) (a : A) : - (tensor_product.lid R A : (R ⊗ A → A)) (r ⊗ₜ a) = r • a := -by simp [tensor_product.lid] - -/-- -The base ring is a right identity for the tensor product of algebra, up to algebra isomorphism. --/ -protected def rid : A ⊗[R] R ≃ₐ[R] A := -alg_equiv_of_linear_equiv_tensor_product (tensor_product.rid R A) -(by simp [mul_smul]) (by simp [algebra.smul_def]) - -@[simp] theorem rid_tmul (r : R) (a : A) : - (tensor_product.rid R A : (A ⊗ R → A)) (a ⊗ₜ r) = r • a := -by simp [tensor_product.rid] - -section -variables (R A B) - -/-- -The tensor product of R-algebras is commutative, up to algebra isomorphism. --/ -protected def comm : A ⊗[R] B ≃ₐ[R] B ⊗[R] A := -alg_equiv_of_linear_equiv_tensor_product (tensor_product.comm R A B) -(by simp) -(λ r, begin - transitivity r • ((1 : B) ⊗ₜ[R] (1 : A)), - { rw [←tmul_smul, algebra.smul_def], simp, }, - { simp [algebra.smul_def], }, -end) - -@[simp] -theorem comm_tmul (a : A) (b : B) : - (tensor_product.comm R A B : (A ⊗[R] B → B ⊗[R] A)) (a ⊗ₜ b) = (b ⊗ₜ a) := -by simp [tensor_product.comm] - -lemma adjoin_tmul_eq_top : adjoin R {t : A ⊗[R] B | ∃ a b, a ⊗ₜ[R] b = t} = ⊤ := -top_le_iff.mp $ (top_le_iff.mpr $ span_tmul_eq_top R A B).trans (span_le_adjoin R _) - -end - -section -variables {R A B C} - -lemma assoc_aux_1 (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C) : - (tensor_product.assoc R A B C) (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) = - (tensor_product.assoc R A B C) ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * - (tensor_product.assoc R A B C) ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂) := -rfl - -lemma assoc_aux_2 (r : R) : - (tensor_product.assoc R A B C) (((algebra_map R A) r ⊗ₜ[R] 1) ⊗ₜ[R] 1) = - (algebra_map R (A ⊗ (B ⊗ C))) r := rfl - -variables (R A B C) - -/-- The associator for tensor product of R-algebras, as an algebra isomorphism. -/ -protected def assoc : ((A ⊗[R] B) ⊗[R] C) ≃ₐ[R] (A ⊗[R] (B ⊗[R] C)) := -alg_equiv_of_linear_equiv_triple_tensor_product - (tensor_product.assoc.{u v₁ v₂ v₃} R A B C : (A ⊗ B ⊗ C) ≃ₗ[R] (A ⊗ (B ⊗ C))) - (@algebra.tensor_product.assoc_aux_1.{u v₁ v₂ v₃} R _ A _ _ B _ _ C _ _) - (@algebra.tensor_product.assoc_aux_2.{u v₁ v₂ v₃} R _ A _ _ B _ _ C _ _) - -variables {R A B C} - -@[simp] theorem assoc_tmul (a : A) (b : B) (c : C) : - ((tensor_product.assoc R A B C) : - (A ⊗[R] B) ⊗[R] C → A ⊗[R] (B ⊗[R] C)) ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c) := -rfl - -end - -variables {R A B C D} - -/-- The tensor product of a pair of algebra morphisms. -/ -def map (f : A →ₐ[R] B) (g : C →ₐ[R] D) : A ⊗[R] C →ₐ[R] B ⊗[R] D := -alg_hom_of_linear_map_tensor_product - (tensor_product.map f.to_linear_map g.to_linear_map) - (by simp) - (by simp [alg_hom.commutes]) - -@[simp] theorem map_tmul (f : A →ₐ[R] B) (g : C →ₐ[R] D) (a : A) (c : C) : - map f g (a ⊗ₜ c) = f a ⊗ₜ g c := -rfl - -@[simp] lemma map_comp_include_left (f : A →ₐ[R] B) (g : C →ₐ[R] D) : - (map f g).comp include_left = include_left.comp f := alg_hom.ext $ by simp - -@[simp] lemma map_comp_include_right (f : A →ₐ[R] B) (g : C →ₐ[R] D) : - (map f g).comp include_right = include_right.comp g := alg_hom.ext $ by simp - -lemma map_range (f : A →ₐ[R] B) (g : C →ₐ[R] D) : - (map f g).range = (include_left.comp f).range ⊔ (include_right.comp g).range := -begin - apply le_antisymm, - { rw [←map_top, ←adjoin_tmul_eq_top, ←adjoin_image, adjoin_le_iff], - rintros _ ⟨_, ⟨a, b, rfl⟩, rfl⟩, - rw [map_tmul, ←_root_.mul_one (f a), ←_root_.one_mul (g b), ←tmul_mul_tmul], - exact mul_mem_sup (alg_hom.mem_range_self _ a) (alg_hom.mem_range_self _ b) }, - { rw [←map_comp_include_left f g, ←map_comp_include_right f g], - exact sup_le (alg_hom.range_comp_le_range _ _) (alg_hom.range_comp_le_range _ _) }, -end - -/-- -Construct an isomorphism between tensor products of R-algebras -from isomorphisms between the tensor factors. --/ -def congr (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) : A ⊗[R] C ≃ₐ[R] B ⊗[R] D := -alg_equiv.of_alg_hom (map f g) (map f.symm g.symm) - (ext $ λ b d, by simp) - (ext $ λ a c, by simp) - -@[simp] -lemma congr_apply (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) (x) : - congr f g x = (map (f : A →ₐ[R] B) (g : C →ₐ[R] D)) x := rfl - -@[simp] -lemma congr_symm_apply (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) (x) : - (congr f g).symm x = (map (f.symm : B →ₐ[R] A) (g.symm : D →ₐ[R] C)) x := rfl - -end - -end monoidal - -section - -variables {R A B S : Type*} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S] -variables [algebra R A] [algebra R B] [algebra R S] -variables (f : A →ₐ[R] S) (g : B →ₐ[R] S) - -variables (R) - -/-- `linear_map.mul'` is an alg_hom on commutative rings. -/ -def lmul' : S ⊗[R] S →ₐ[R] S := -alg_hom_of_linear_map_tensor_product (linear_map.mul' R S) - (λ a₁ a₂ b₁ b₂, by simp only [linear_map.mul'_apply, mul_mul_mul_comm]) - (λ r, by simp only [linear_map.mul'_apply, _root_.mul_one]) +open module (dual) -variables {R} +/- Heterobasic `tensor_product.hom_tensor_hom_map` -/ +def hom_tensor_hom_map : ((M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q)) →ₗ[A] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := +lift map_bilinear -lemma lmul'_to_linear_map : (lmul' R : _ →ₐ[R] S).to_linear_map = linear_map.mul' R S := rfl - -@[simp] lemma lmul'_apply_tmul (a b : S) : lmul' R (a ⊗ₜ[R] b) = a * b := rfl - -@[simp] -lemma lmul'_comp_include_left : (lmul' R : _ →ₐ[R] S).comp include_left = alg_hom.id R S := -alg_hom.ext $ _root_.mul_one - -@[simp] -lemma lmul'_comp_include_right : (lmul' R : _ →ₐ[R] S).comp include_right = alg_hom.id R S := -alg_hom.ext $ _root_.one_mul - -/-- -If `S` is commutative, for a pair of morphisms `f : A →ₐ[R] S`, `g : B →ₐ[R] S`, -We obtain a map `A ⊗[R] B →ₐ[R] S` that commutes with `f`, `g` via `a ⊗ b ↦ f(a) * g(b)`. --/ -def product_map : A ⊗[R] B →ₐ[R] S := (lmul' R).comp (tensor_product.map f g) - -@[simp] lemma product_map_apply_tmul (a : A) (b : B) : product_map f g (a ⊗ₜ b) = f a * g b := -by { unfold product_map lmul', simp } - -lemma product_map_left_apply (a : A) : - product_map f g ((include_left : A →ₐ[R] A ⊗ B) a) = f a := by simp - -@[simp] lemma product_map_left : (product_map f g).comp include_left = f := alg_hom.ext $ by simp - -lemma product_map_right_apply (b : B) : product_map f g (include_right b) = g b := by simp - -@[simp] lemma product_map_right : (product_map f g).comp include_right = g := alg_hom.ext $ by simp - -lemma product_map_range : (product_map f g).range = f.range ⊔ g.range := -by rw [product_map, alg_hom.range_comp, map_range, map_sup, ←alg_hom.range_comp, - ←alg_hom.range_comp, ←alg_hom.comp_assoc, ←alg_hom.comp_assoc, lmul'_comp_include_left, - lmul'_comp_include_right, alg_hom.id_comp, alg_hom.id_comp] - -end -section - -variables {R A A' B S : Type*} -variables [comm_semiring R] [comm_semiring A] [semiring A'] [semiring B] [comm_semiring S] -variables [algebra R A] [algebra R A'] [algebra A A'] [is_scalar_tower R A A'] [algebra R B] -variables [algebra R S] [algebra A S] [is_scalar_tower R A S] - -/-- If `A`, `B` are `R`-algebras, `A'` is an `A`-algebra, then the product map of `f : A' →ₐ[A] S` -and `g : B →ₐ[R] S` is an `A`-algebra homomorphism. -/ -@[simps] def product_left_alg_hom (f : A' →ₐ[A] S) (g : B →ₐ[R] S) : A' ⊗[R] B →ₐ[A] S := -{ commutes' := λ r, by { dsimp, simp }, - ..(product_map (f.restrict_scalars R) g).to_ring_hom } - -end -section basis - -variables {k : Type*} [comm_ring k] (R : Type*) [ring R] [algebra k R] {M : Type*} - [add_comm_monoid M] [module k M] {ι : Type*} (b : basis ι k M) - -/-- Given a `k`-algebra `R` and a `k`-basis of `M,` this is a `k`-linear isomorphism -`R ⊗[k] M ≃ (ι →₀ R)` (which is in fact `R`-linear). -/ -noncomputable def basis_aux : R ⊗[k] M ≃ₗ[k] (ι →₀ R) := -(_root_.tensor_product.congr (finsupp.linear_equiv.finsupp_unique k R punit).symm b.repr) ≪≫ₗ - (finsupp_tensor_finsupp k R k punit ι).trans (finsupp.lcongr (equiv.unique_prod ι punit) - (_root_.tensor_product.rid k R)) - -variables {R} +set_option pp.parens true +notation (name := tensor_product') + M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N -lemma basis_aux_tmul (r : R) (m : M) : - basis_aux R b (r ⊗ₜ m) = r • (finsupp.map_range (algebra_map k R) - (map_zero _) (b.repr m)) := +/- Heterobasic `tensor_product.dual_distrib` -/ +def dual_distrib : (dual A M) ⊗[R] (dual R N) →ₗ[A] dual A (M ⊗[R] N) := begin - ext, - simp [basis_aux, ←algebra.commutes, algebra.smul_def], + refine _ ∘ₗ hom_tensor_hom_map _ _ _ _ _ _, + refine comp_right _, + exact (algebra.tensor_product.rid R A), + exact (comp_right ↑(tensor_product.lid R R)), end -lemma basis_aux_map_smul (r : R) (x : R ⊗[k] M) : - basis_aux R b (r • x) = r • basis_aux R b x := -tensor_product.induction_on x (by simp) (λ x y, by simp only [tensor_product.smul_tmul', - basis_aux_tmul, smul_assoc]) (λ x y hx hy, by simp [hx, hy]) - -variables (R) +#check tensor_product.rid + +-- set_option pp.parens true +-- notation (name := tensor_product') +-- M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N + +-- /-- A tensor product analogue of `mul_left_comm`. -/ +-- def right_comm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := +-- -- assoc R A _ _ _ ≪≫ₗ begin +-- -- sorry +-- -- end +-- linear_equiv.of_linear +-- (lift _) +-- (lift _) _ _ +-- let e₁ := (assoc R A M Q P).symm, +-- e₂ := congr (tensor_product.comm A M P) (1 : Q ≃ₗ[R] Q), +-- e₃ := (assoc R A P Q M) in +-- e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) + +-- /-- Heterobasic version of `tensor_tensor_tensor_comm`: + +-- Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ +-- def tensor_tensor_tensor_comm : +-- (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := +-- let e₁ := (assoc R A (M ⊗[R] N) Q P).symm, +-- e₁' := assoc R A M N (P ⊗[R] Q) in +-- e₁ ≪≫ₗ congr (sorry : ((M ⊗[R] N) ⊗[A] P) ≃ₗ[A] ((M ⊗[A] P) ⊗[R] N)) (1 : Q ≃ₗ[R] Q) ≪≫ₗ +-- sorry -/-- Given a `k`-algebra `R`, this is the `R`-basis of `R ⊗[k] M` induced by a `k`-basis of `M`. -/ -noncomputable def basis : basis ι R (R ⊗[k] M) := -{ repr := { map_smul' := basis_aux_map_smul b, .. basis_aux R b } } - -variables {R} - -@[simp] lemma basis_repr_tmul (r : R) (m : M) : - (basis R b).repr (r ⊗ₜ m) = r • (finsupp.map_range (algebra_map k R) (map_zero _) (b.repr m)) := -basis_aux_tmul _ _ _ +end comm_semiring -@[simp] lemma basis_repr_symm_apply (r : R) (i : ι) : - (basis R b).repr.symm (finsupp.single i r) = r ⊗ₜ b.repr.symm (finsupp.single i 1) := -by simp [basis, equiv.unique_prod_symm_apply, basis_aux] +end algebra_tensor_module -end basis end tensor_product -end algebra - -namespace module - -variables {R M N : Type*} [comm_semiring R] -variables [add_comm_monoid M] [add_comm_monoid N] -variables [module R M] [module R N] - -/-- The algebra homomorphism from `End M ⊗ End N` to `End (M ⊗ N)` sending `f ⊗ₜ g` to -the `tensor_product.map f g`, the tensor product of the two maps. -/ -def End_tensor_End_alg_hom : (End R M) ⊗[R] (End R N) →ₐ[R] End R (M ⊗[R] N) := -begin - refine algebra.tensor_product.alg_hom_of_linear_map_tensor_product - (hom_tensor_hom_map R M N M N) _ _, - { intros f₁ f₂ g₁ g₂, - simp only [hom_tensor_hom_map_apply, tensor_product.map_mul] }, - { intro r, - simp only [hom_tensor_hom_map_apply], - ext m n, simp [smul_tmul] } -end - -lemma End_tensor_End_alg_hom_apply (f : End R M) (g : End R N) : - End_tensor_End_alg_hom (f ⊗ₜ[R] g) = tensor_product.map f g := -by simp only [End_tensor_End_alg_hom, - algebra.tensor_product.alg_hom_of_linear_map_tensor_product_apply, hom_tensor_hom_map_apply] - -end module - -lemma subalgebra.finite_dimensional_sup {K L : Type*} [field K] [comm_ring L] [algebra K L] - (E1 E2 : subalgebra K L) [finite_dimensional K E1] [finite_dimensional K E2] : - finite_dimensional K ↥(E1 ⊔ E2) := -begin - rw [←E1.range_val, ←E2.range_val, ←algebra.tensor_product.product_map_range], - exact (algebra.tensor_product.product_map E1.val E2.val).to_linear_map.finite_dimensional_range, -end - -namespace tensor_product.algebra - -variables {R A B M : Type*} -variables [comm_semiring R] [add_comm_monoid M] [module R M] -variables [semiring A] [semiring B] [module A M] [module B M] -variables [algebra R A] [algebra R B] -variables [is_scalar_tower R A M] [is_scalar_tower R B M] - -/-- An auxiliary definition, used for constructing the `module (A ⊗[R] B) M` in -`tensor_product.algebra.module` below. -/ -def module_aux : A ⊗[R] B →ₗ[R] M →ₗ[R] M := -tensor_product.lift -{ to_fun := λ a, a • (algebra.lsmul R M : B →ₐ[R] module.End R M).to_linear_map, - map_add' := λ r t, by { ext, simp only [add_smul, linear_map.add_apply] }, - map_smul' := λ n r, by { ext, simp only [ring_hom.id_apply, linear_map.smul_apply, smul_assoc] } } - -lemma module_aux_apply (a : A) (b : B) (m : M) : - module_aux (a ⊗ₜ[R] b) m = a • b • m := rfl - -variables [smul_comm_class A B M] - -/-- If `M` is a representation of two different `R`-algebras `A` and `B` whose actions commute, -then it is a representation the `R`-algebra `A ⊗[R] B`. - -An important example arises from a semiring `S`; allowing `S` to act on itself via left and right -multiplication, the roles of `R`, `A`, `B`, `M` are played by `ℕ`, `S`, `Sᵐᵒᵖ`, `S`. This example -is important because a submodule of `S` as a `module` over `S ⊗[ℕ] Sᵐᵒᵖ` is a two-sided ideal. - -NB: This is not an instance because in the case `B = A` and `M = A ⊗[R] A` we would have a diamond -of `smul` actions. Furthermore, this would not be a mere definitional diamond but a true -mathematical diamond in which `A ⊗[R] A` had two distinct scalar actions on itself: one from its -multiplication, and one from this would-be instance. Arguably we could live with this but in any -case the real fix is to address the ambiguity in notation, probably along the lines outlined here: -https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929258 --/ -protected def module : module (A ⊗[R] B) M := -{ smul := λ x m, module_aux x m, - zero_smul := λ m, by simp only [map_zero, linear_map.zero_apply], - smul_zero := λ x, by simp only [map_zero], - smul_add := λ x m₁ m₂, by simp only [map_add], - add_smul := λ x y m, by simp only [map_add, linear_map.add_apply], - one_smul := λ m, by simp only [module_aux_apply, algebra.tensor_product.one_def, one_smul], - mul_smul := λ x y m, - begin - apply tensor_product.induction_on x; - apply tensor_product.induction_on y, - { simp only [mul_zero, map_zero, linear_map.zero_apply], }, - { intros a b, simp only [zero_mul, map_zero, linear_map.zero_apply], }, - { intros z w hz hw, simp only [zero_mul, map_zero, linear_map.zero_apply], }, - { intros a b, simp only [mul_zero, map_zero, linear_map.zero_apply], }, - { intros a₁ b₁ a₂ b₂, - simp only [module_aux_apply, mul_smul, smul_comm a₁ b₂, algebra.tensor_product.tmul_mul_tmul, - linear_map.mul_apply], }, - { intros z w hz hw a b, - simp only at hz hw, - simp only [mul_add, hz, hw, map_add, linear_map.add_apply], }, - { intros z w hz hw, simp only [mul_zero, map_zero, linear_map.zero_apply], }, - { intros a b z w hz hw, - simp only at hz hw, - simp only [map_add, add_mul, linear_map.add_apply, hz, hw], }, - { intros u v hu hv z w hz hw, - simp only at hz hw, - simp only [add_mul, hz, hw, map_add, linear_map.add_apply], }, - end } - -local attribute [instance] tensor_product.algebra.module - -lemma smul_def (a : A) (b : B) (m : M) : (a ⊗ₜ[R] b) • m = a • b • m := rfl - -end tensor_product.algebra From da87b80035bac86c56efbdbfdabf3606d70c3b90 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 21:58:54 +0000 Subject: [PATCH 03/23] rid --- .../ring_theory/tensor_product.lean | 21 ++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 2f207c039..2f89b6df1 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -27,7 +27,7 @@ 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] variables [add_comm_monoid Q] [module R Q] -/-- . -/ +/-- Heterobasic `tensor_product.map`. -/ def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] Q := lift $ (show (Q →ₗ[R] P ⊗ Q) →ₗ[A] N →ₗ[R] P ⊗[R] Q, from{ to_fun := λ h, h ∘ₗ g, @@ -90,6 +90,17 @@ rfl variables (R A M N P Q) +/- Heterobasic `tensor_product.id` -/ +def rid : A ⊗[R] R ≃ₗ[A] A := +linear_equiv.of_linear + (lift $ linear_map.flip $ + (algebra.lsmul A A : A →ₐ[A] _).to_linear_map.restrict_scalars R ∘ₗ algebra.linear_map R A) + ((mk R A A R).flip 1) + (ext_ring $ show algebra_map R A 1 * 1 = 1, by simp) + (ext $ λ x y, show (algebra_map R A y * x) ⊗ₜ[R] 1 = x ⊗ₜ[R] y, + by rw [←_root_.algebra.smul_def, smul_tmul, smul_eq_mul, mul_one]) + + /-- A tensor product analogue of `mul_left_comm`. -/ def left_comm : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q) := let e₁ := (assoc R A M Q P).symm, @@ -110,14 +121,10 @@ notation (name := tensor_product') /- Heterobasic `tensor_product.dual_distrib` -/ def dual_distrib : (dual A M) ⊗[R] (dual R N) →ₗ[A] dual A (M ⊗[R] N) := begin - refine _ ∘ₗ hom_tensor_hom_map _ _ _ _ _ _, - refine comp_right _, - exact (algebra.tensor_product.rid R A), - exact (comp_right ↑(tensor_product.lid R R)), + refine _ ∘ₗ hom_tensor_hom_map R A M N A R, + exact comp_right (rid R A), end -#check tensor_product.rid - -- set_option pp.parens true -- notation (name := tensor_product') -- M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N From ebf7e8705af944757289f844686860e34af323c0 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 21:59:22 +0000 Subject: [PATCH 04/23] cleanup --- src/for_mathlib/ring_theory/tensor_product.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 2f89b6df1..3d08156db 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -114,10 +114,6 @@ open module (dual) def hom_tensor_hom_map : ((M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q)) →ₗ[A] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := lift map_bilinear -set_option pp.parens true -notation (name := tensor_product') - M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N - /- Heterobasic `tensor_product.dual_distrib` -/ def dual_distrib : (dual A M) ⊗[R] (dual R N) →ₗ[A] dual A (M ⊗[R] N) := begin @@ -125,9 +121,9 @@ begin exact comp_right (rid R A), end --- set_option pp.parens true --- notation (name := tensor_product') --- M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N +set_option pp.parens true +notation (name := tensor_product') + M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N -- /-- A tensor product analogue of `mul_left_comm`. -/ -- def right_comm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := From 1290423aa7cc509bd6f621d073736746e025d444 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 22:28:46 +0000 Subject: [PATCH 05/23] all but tensor^3_comm --- .../linear_algebra/bilinear_form/basic.lean | 12 ++ .../bilinear_form/tensor_product.lean | 107 +++++------------- .../ring_theory/tensor_product.lean | 40 +++++-- 3 files changed, 68 insertions(+), 91 deletions(-) diff --git a/src/for_mathlib/linear_algebra/bilinear_form/basic.lean b/src/for_mathlib/linear_algebra/bilinear_form/basic.lean index d2f43a226..67da16651 100644 --- a/src/for_mathlib/linear_algebra/bilinear_form/basic.lean +++ b/src/for_mathlib/linear_algebra/bilinear_form/basic.lean @@ -3,6 +3,8 @@ import linear_algebra.bilinear_form namespace bilin_form variables {α β R M : Type*} + +section semiring variables [semiring R] [add_comm_monoid M] [module R M] variables [monoid α] [monoid β] [distrib_mul_action α R] [distrib_mul_action β R] variables [smul_comm_class α R R] [smul_comm_class β R R] @@ -13,4 +15,14 @@ instance [smul_comm_class α β R] : smul_comm_class α β (bilin_form R M) := instance [has_smul α β] [is_scalar_tower α β R] : is_scalar_tower α β (bilin_form R M) := ⟨λ a b B, ext $ λ x y, smul_assoc _ _ _⟩ +end semiring + +section comm_semiring +variables [comm_semiring R] [add_comm_monoid M] [module R M] + +@[simp] +lemma linear_map.to_bilin_apply (l : M →ₗ[R] M →ₗ[R] R) (v w : M) : l.to_bilin v w = l v w := rfl + +end comm_semiring + end bilin_form \ No newline at end of file diff --git a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean index fadb6dc08..996c96e7f 100644 --- a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean +++ b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean @@ -11,102 +11,47 @@ import for_mathlib.linear_algebra.tensor_product import for_mathlib.linear_algebra.bilinear_form.basic universes u v w -variables {ι : Type*} {R S : Type*} {M₁ M₂ : Type*} +variables {ι : Type*} {R A : Type*} {M₁ M₂ : Type*} open_locale tensor_product namespace bilin_form section comm_semiring -variables [comm_semiring R] [comm_semiring S] +variables [comm_semiring R] [comm_semiring A] variables [add_comm_monoid M₁] [add_comm_monoid M₂] -variables [algebra R S] [module R M₁] [module S M₁] -variables [smul_comm_class R S M₁] [smul_comm_class S R M₁] [smul_comm_class R S S] [is_scalar_tower R S M₁] +variables [algebra R A] [module R M₁] [module A M₁] +variables [smul_comm_class R A M₁] [smul_comm_class A R M₁] [smul_comm_class R A A] [is_scalar_tower R A M₁] variables [module R M₂] -notation (name := tensor_product') - M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N - -set_option pp.parens true - -#check tensor_product.algebra_tensor_module.lift.equiv R S (M₁ ⊗ M₂) (M₁ ⊗ M₂) S - -#check tensor_product.tensor_tensor_tensor_comm R M₁ M₂ M₁ M₂ - -instance : module R (M₁ ⊗[S] M₁) := tensor_product.left_module -instance : smul_comm_class R S (M₁ ⊗[S] M₁) := tensor_product.smul_comm_class_left -instance foo : module S ((M₁ ⊗[S] M₁) ⊗[R] (M₂ ⊗[R] M₂)) := tensor_product.left_module - -instance : is_scalar_tower R S (M₁ ⊗[R] M₂) := tensor_product.is_scalar_tower_left - -instance : smul_comm_class R S (bilin_form S M₁) := bilin_form.smul_comm_class -instance : module S (bilin_form S M₁ ⊗[R] bilin_form R M₂) := tensor_product.left_module - -section -variables (R S M₁ M₂) - -def tensor_tensor_tensor_comm' : - ((M₁ ⊗[R] M₂) ⊗[S] (M₁ ⊗[R] M₂) ≃ₗ[S] (M₁ ⊗[S] M₁) ⊗[R] (M₂ ⊗[R] M₂)) := sorry - -end - -#check (( - tensor_tensor_tensor_comm' _ _ _ _ : (((M₁ ⊗[R] M₂) ⊗[S] (M₁ ⊗[R] M₂)) ≃ₗ[S] ((M₁ ⊗[S] M₁) ⊗[R] (M₂ ⊗[R] M₂))) - -- tensor_product.tensor_tensor_tensor_comm R M₁ M₂ M₁ M₂ - -).dual_map - ≪≫ₗ (tensor_product.lift.equiv S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) S).symm - ≪≫ₗ linear_map.to_bilin).to_linear_map --- #exit /-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/ -def tensor_distrib' : bilin_form S M₁ ⊗[R] bilin_form R M₂ →ₗ[S] bilin_form S (M₁ ⊗[R] M₂) := -((tensor_tensor_tensor_comm' R S M₁ M₂).dual_map - ≪≫ₗ (tensor_product.lift.equiv S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) S).symm +def tensor_distrib' : bilin_form A M₁ ⊗[R] bilin_form R M₂ →ₗ[A] bilin_form A (M₁ ⊗[R] M₂) := +((tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm R A M₁ M₂ M₁ M₂).dual_map + ≪≫ₗ (tensor_product.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm ≪≫ₗ linear_map.to_bilin).to_linear_map - ∘ₗ _ + ∘ₗ tensor_product.algebra_tensor_module.dual_distrib R _ _ _ ∘ₗ (tensor_product.algebra_tensor_module.congr - (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv S M₁ M₁ S) + (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv A M₁ M₁ A) (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv R M₂ M₂ R)).to_linear_map -@[simp] lemma tensor_distrib_tmul (B₁ : bilin_form R M₁) (B₂ : bilin_form R M₂) +@[simp] lemma tensor_distrib_tmul' (B₁ : bilin_form A M₁) (B₂ : bilin_form R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : - tensor_distrib (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := -rfl - -/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ -@[reducible] -protected def tmul (B₁ : bilin_form R M₁) (B₂ : bilin_form R M₂) : bilin_form R (M₁ ⊗[R] M₂) := -tensor_distrib (B₁ ⊗ₜ[R] B₂) - -end comm_semiring - - -section comm_semiring -variables [comm_semiring R] -variables [add_comm_monoid M₁] [add_comm_monoid M₂] -variables [module R M₁] [module R M₂] - -/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/ -def tensor_distrib'' : bilin_form R M₁ ⊗[R] bilin_form R M₂ →ₗ[R] bilin_form R (M₁ ⊗[R] M₂) := -((tensor_product.tensor_tensor_tensor_comm R M₁ M₂ M₁ M₂).dual_map - ≪≫ₗ (tensor_product.lift.equiv R (M₁ ⊗ M₂) (M₁ ⊗ M₂) R).symm - ≪≫ₗ linear_map.to_bilin).to_linear_map - ∘ₗ tensor_product.dual_distrib R _ _ - ∘ₗ (tensor_product.congr - (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv R _ _ _) - (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv R _ _ _)).to_linear_map - -#print tensor_distrib'' - -@[simp] lemma tensor_distrib_tmul (B₁ : bilin_form R M₁) (B₂ : bilin_form R M₂) - (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : - tensor_distrib (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := -rfl - -/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ -@[reducible] -protected def tmul (B₁ : bilin_form R M₁) (B₂ : bilin_form R M₂) : bilin_form R (M₁ ⊗[R] M₂) := -tensor_distrib (B₁ ⊗ₜ[R] B₂) + tensor_distrib' (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * algebra_map R A (B₂ m₂ m₂') := +begin + -- will be refl once we fill the sorry in `tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm` + simp only [tensor_distrib', linear_map.comp_apply, linear_equiv.coe_to_linear_map, + tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm_apply, linear_equiv.trans_apply, + linear_map.to_bilin_apply, tensor_product.algebra_tensor_module.dual_distrib_apply, + tensor_product.algebra_tensor_module.congr_tmul, + linear_equiv.dual_map_apply, + tensor_product.lift.equiv_apply, + bilin_form.to_lin_apply, + tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm_apply, + tensor_product.algebra_tensor_module.dual_distrib_apply, + tensor_product.lift.equiv_apply, + tensor_product.lift.equiv_symm_apply, + linear_equiv.dual_map_apply], +end end comm_semiring diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 3d08156db..10fb8fc9d 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -90,16 +90,17 @@ rfl variables (R A M N P Q) -/- Heterobasic `tensor_product.id` -/ +/- Heterobasic `tensor_product.rid` -/ def rid : A ⊗[R] R ≃ₗ[A] A := linear_equiv.of_linear (lift $ linear_map.flip $ - (algebra.lsmul A A : A →ₐ[A] _).to_linear_map.restrict_scalars R ∘ₗ algebra.linear_map R A) + (algebra.lsmul A A : A →ₐ[A] _).to_linear_map.flip.restrict_scalars R ∘ₗ algebra.linear_map R A) ((mk R A A R).flip 1) - (ext_ring $ show algebra_map R A 1 * 1 = 1, by simp) - (ext $ λ x y, show (algebra_map R A y * x) ⊗ₜ[R] 1 = x ⊗ₜ[R] y, - by rw [←_root_.algebra.smul_def, smul_tmul, smul_eq_mul, mul_one]) - + (ext_ring $ show 1 * algebra_map R A 1 = 1, by simp) + (ext $ λ x y, show (x * algebra_map R A y) ⊗ₜ[R] 1 = x ⊗ₜ[R] y, + by rw [←algebra.commutes, ←_root_.algebra.smul_def, smul_tmul, smul_eq_mul, mul_one]) + +lemma rid_apply (a : A) (r : R) : rid R A (a ⊗ₜ r) = a * algebra_map R A r := rfl /-- A tensor product analogue of `mul_left_comm`. -/ def left_comm : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q) := @@ -114,6 +115,10 @@ open module (dual) def hom_tensor_hom_map : ((M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q)) →ₗ[A] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := lift map_bilinear +@[simp] lemma hom_tensor_hom_map_apply (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : + hom_tensor_hom_map R A M N P Q (f ⊗ₜ g) = map f g := +rfl + /- Heterobasic `tensor_product.dual_distrib` -/ def dual_distrib : (dual A M) ⊗[R] (dual R N) →ₗ[A] dual A (M ⊗[R] N) := begin @@ -121,6 +126,16 @@ begin exact comp_right (rid R A), end +variables {R A M N P Q} + +@[simp] +lemma dual_distrib_apply (f : dual A M) (g : dual R N) (m : M) (n : N) : + dual_distrib R A M N (f ⊗ₜ g) (m ⊗ₜ n) = f m * algebra_map R A (g n) := +rfl + + +variables (R A M N P Q) + set_option pp.parens true notation (name := tensor_product') M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N @@ -138,11 +153,16 @@ notation (name := tensor_product') -- e₃ := (assoc R A P Q M) in -- e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) --- /-- Heterobasic version of `tensor_tensor_tensor_comm`: +/-- Heterobasic version of `tensor_tensor_tensor_comm`: + +Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ +def tensor_tensor_tensor_comm : + (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := +sorry --- Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ --- def tensor_tensor_tensor_comm : --- (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := +@[simp] lemma tensor_tensor_tensor_comm_apply (m : M) (n : N) (p : P) (q : Q) : + tensor_tensor_tensor_comm R A M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q) := +sorry -- let e₁ := (assoc R A (M ⊗[R] N) Q P).symm, -- e₁' := assoc R A M N (P ⊗[R] Q) in -- e₁ ≪≫ₗ congr (sorry : ((M ⊗[R] N) ⊗[A] P) ≃ₗ[A] ((M ⊗[A] P) ⊗[R] N)) (1 : Q ≃ₗ[R] Q) ≪≫ₗ From 44c306e4a25d83a54568687dda768dbda7affe67 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 22:33:47 +0000 Subject: [PATCH 06/23] complexify --- .../linear_algebra/bilinear_form/tensor_product.lean | 7 +++++++ .../from_mathlib/complexification.lean | 11 +++-------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean index 996c96e7f..529151e91 100644 --- a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean +++ b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean @@ -53,6 +53,13 @@ begin linear_equiv.dual_map_apply], end +/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +@[reducible] +protected def tmul' (B₁ : bilin_form A M₁) (B₂ : bilin_form R M₂) : bilin_form A (M₁ ⊗[R] M₂) := +tensor_distrib (B₁ ⊗ₜ[R] B₂) + +#check bilin_form.tensor_distrib + end comm_semiring section comm_semiring diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index 0d163875d..e47f4ce9c 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -8,12 +8,7 @@ variables {V: Type*} [add_comm_group V] [module ℝ V] open_locale tensor_product -#check bilin_form.tmul - -def quadratic_form.complexify (Q : quadratic_form ℝ V) : +noncomputable def quadratic_form.complexify (Q : quadratic_form ℝ V) : quadratic_form ℂ (ℂ ⊗[ℝ] V) := -{ to_fun := , - to_fun_smul := _, - exists_companion' := _ } --- bilin_form.to_quadratic_form $ --- (bilin_form.tmul _ Q.associated) \ No newline at end of file +bilin_form.to_quadratic_form $ + (bilin_form.tmul' (linear_map.mul ℂ ℂ).to_bilin Q.associated) \ No newline at end of file From cc355b99017fb664d6a4273afcd70f1f99dc2103 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 22:35:49 +0000 Subject: [PATCH 07/23] oops --- .../linear_algebra/bilinear_form/tensor_product.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean index 529151e91..5572e7269 100644 --- a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean +++ b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean @@ -34,7 +34,7 @@ def tensor_distrib' : bilin_form A M₁ ⊗[R] bilin_form R M₂ →ₗ[A] bilin (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv A M₁ M₁ A) (bilin_form.to_lin ≪≫ₗ tensor_product.lift.equiv R M₂ M₂ R)).to_linear_map -@[simp] lemma tensor_distrib_tmul' (B₁ : bilin_form A M₁) (B₂ : bilin_form R M₂) +@[simp] lemma tensor_distrib'_tmul (B₁ : bilin_form A M₁) (B₂ : bilin_form R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensor_distrib' (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * algebra_map R A (B₂ m₂ m₂') := begin @@ -56,7 +56,7 @@ end /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ @[reducible] protected def tmul' (B₁ : bilin_form A M₁) (B₂ : bilin_form R M₂) : bilin_form A (M₁ ⊗[R] M₂) := -tensor_distrib (B₁ ⊗ₜ[R] B₂) +tensor_distrib' (B₁ ⊗ₜ[R] B₂) #check bilin_form.tensor_distrib From 5a584b97ad9361eb3d204e83fd3f49ed8768fff7 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 22:36:04 +0000 Subject: [PATCH 08/23] tidy --- .../linear_algebra/bilinear_form/tensor_product.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean index 5572e7269..1e5f07b98 100644 --- a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean +++ b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean @@ -58,8 +58,6 @@ end protected def tmul' (B₁ : bilin_form A M₁) (B₂ : bilin_form R M₂) : bilin_form A (M₁ ⊗[R] M₂) := tensor_distrib' (B₁ ⊗ₜ[R] B₂) -#check bilin_form.tensor_distrib - end comm_semiring section comm_semiring From 2dfeb3c60298210caa707cb21c4142ea406b1822 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 22:54:20 +0000 Subject: [PATCH 09/23] done --- .../ring_theory/tensor_product.lean | 40 ++++++++++++++++++- 1 file changed, 38 insertions(+), 2 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 10fb8fc9d..ef99e2aca 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -141,7 +141,8 @@ notation (name := tensor_product') M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N -- /-- A tensor product analogue of `mul_left_comm`. -/ --- def right_comm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := +def right_comm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := +sorry -- -- assoc R A _ _ _ ≪≫ₗ begin -- -- sorry -- -- end @@ -153,12 +154,47 @@ notation (name := tensor_product') -- e₃ := (assoc R A P Q M) in -- e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) +#print tensor_product.assoc + +/-- Heterobasic version of `tensor_product.assoc`: + +Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ +def assoc' : ((M ⊗[R] N) ⊗[R] Q) ≃ₗ[A] (M ⊗[R] (N ⊗[R] Q)) := +begin + refine linear_equiv.of_linear + (lift $ lift $ _ ∘ₗ mk R A M (N ⊗[R] Q)) -- (lcurry R _ _ _ _) + (lift $ _ ∘ₗ (curry $ mk R A (M ⊗[R] N) Q)) _ _, -- (uncurry R _ _ _) + -- (ext $ linear_map.ext $ λ m, ext' $ λ n p, _) + -- (ext $ flip_inj $ linear_map.ext $ λ p, ext' $ λ m n, _), + repeat { rw lift.tmul <|> rw compr₂_apply <|> rw comp_apply <|> + rw mk_apply <|> rw flip_apply <|> rw lcurry_apply <|> + rw uncurry_apply <|> rw curry_apply <|> rw id_apply } +end + +#check assoc +-- 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, simp only [curry_apply, tensor_product.curry_apply, mk_apply, tensor_product.mk_apply, +-- uncurry_apply, tensor_product.uncurry_apply, id_apply, lift_tmul, compr₂_apply, +-- restrict_scalars_apply, function.comp_app, to_fun_eq_coe, lcurry_apply, +-- linear_map.comp_apply] }) + + /-- Heterobasic version of `tensor_tensor_tensor_comm`: + + Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ def tensor_tensor_tensor_comm : (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := -sorry +(assoc R A _ _ _).symm ≪≫ₗ begin + sorry + +end @[simp] lemma tensor_tensor_tensor_comm_apply (m : M) (n : N) (p : P) (q : Q) : tensor_tensor_tensor_comm R A M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q) := From cd4499a5e30736d3d5d4e4cd52a3149e50fecf9e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 01:11:34 +0000 Subject: [PATCH 10/23] so close --- .../bilinear_form/tensor_product.lean | 16 +--- .../ring_theory/tensor_product.lean | 80 +++++++++++-------- 2 files changed, 49 insertions(+), 47 deletions(-) diff --git a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean index 1e5f07b98..652a4d98a 100644 --- a/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean +++ b/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean @@ -37,21 +37,7 @@ def tensor_distrib' : bilin_form A M₁ ⊗[R] bilin_form R M₂ →ₗ[A] bilin @[simp] lemma tensor_distrib'_tmul (B₁ : bilin_form A M₁) (B₂ : bilin_form R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensor_distrib' (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * algebra_map R A (B₂ m₂ m₂') := -begin - -- will be refl once we fill the sorry in `tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm` - simp only [tensor_distrib', linear_map.comp_apply, linear_equiv.coe_to_linear_map, - tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm_apply, linear_equiv.trans_apply, - linear_map.to_bilin_apply, tensor_product.algebra_tensor_module.dual_distrib_apply, - tensor_product.algebra_tensor_module.congr_tmul, - linear_equiv.dual_map_apply, - tensor_product.lift.equiv_apply, - bilin_form.to_lin_apply, - tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm_apply, - tensor_product.algebra_tensor_module.dual_distrib_apply, - tensor_product.lift.equiv_apply, - tensor_product.lift.equiv_symm_apply, - linear_equiv.dual_map_apply], -end +rfl /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ @[reducible] diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index ef99e2aca..47a34ac8b 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -140,9 +140,6 @@ set_option pp.parens true notation (name := tensor_product') M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N --- /-- A tensor product analogue of `mul_left_comm`. -/ -def right_comm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := -sorry -- -- assoc R A _ _ _ ≪≫ₗ begin -- -- sorry -- -- end @@ -155,35 +152,61 @@ sorry -- e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) #print tensor_product.assoc +#check curry + +/-- 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' : (N →ₗ[R] (Q →ₗ[R] P)) →ₗ[A] ((N ⊗[R] Q) →ₗ[R] 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, ring_hom.id_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' : ((N ⊗[R] Q) →ₗ[R] P) →ₗ[A] (N →ₗ[R] (Q →ₗ[R] P)) := +{ to_fun := curry, + map_add' := λ f g, rfl, + map_smul' := λ c f, rfl } /-- Heterobasic version of `tensor_product.assoc`: Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ def assoc' : ((M ⊗[R] N) ⊗[R] Q) ≃ₗ[A] (M ⊗[R] (N ⊗[R] Q)) := +linear_equiv.of_linear + (lift $ lift $ lcurry' R A N _ Q ∘ₗ mk R A M (N ⊗[R] Q)) -- (lcurry R _ _ _ _) + (lift $ (uncurry' R _ _ _ _) ∘ₗ (curry $ mk R A (M ⊗[R] N) Q)) + (curry_injective $ linear_map.ext $ λ m, + curry_injective $ linear_map.ext $ λ n, linear_map.ext $ λ q, + by exact eq.refl (m ⊗ₜ[R] (n ⊗ₜ[R] q))) + (curry_injective $ ext $ λ m n, linear_map.ext $ λ q, + by exact eq.refl ((m ⊗ₜ[R] n) ⊗ₜ[R] q)) +. +instance : is_scalar_tower R A (P →ₗ[A] ((M ⊗[A] P) ⊗[R] Q)) := linear_map.is_scalar_tower +instance : linear_map.compatible_smul + ((M ⊗[A] P) →ₗ[A] ((M ⊗[A] P) ⊗[R] Q)) + (M →ₗ[A] (P →ₗ[A] ((M ⊗[A] P) ⊗[R] Q))) + R + A := is_scalar_tower.compatible_smul + +-- /-- A tensor product analogue of `mul_left_comm`. -/ +def right_comm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := begin refine linear_equiv.of_linear - (lift $ lift $ _ ∘ₗ mk R A M (N ⊗[R] Q)) -- (lcurry R _ _ _ _) - (lift $ _ ∘ₗ (curry $ mk R A (M ⊗[R] N) Q)) _ _, -- (uncurry R _ _ _) - -- (ext $ linear_map.ext $ λ m, ext' $ λ n p, _) - -- (ext $ flip_inj $ linear_map.ext $ λ p, ext' $ λ m n, _), - repeat { rw lift.tmul <|> rw compr₂_apply <|> rw comp_apply <|> - rw mk_apply <|> rw flip_apply <|> rw lcurry_apply <|> - rw uncurry_apply <|> rw curry_apply <|> rw id_apply } + (lift $ lift $ flip $ lcurry R A M Q _ ∘ₗ (mk A A (M ⊗[R] Q) P).flip) + (lift $ lift $ flip $ + (tensor_product.lcurry A M P ((M ⊗[A] P) ⊗[R] Q)).restrict_scalars R + ∘ₗ (mk R A (M ⊗[A] P) Q).flip) + (curry_injective _) + (curry_injective _), + sorry, + sorry, end -#check assoc --- 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, simp only [curry_apply, tensor_product.curry_apply, mk_apply, tensor_product.mk_apply, --- uncurry_apply, tensor_product.uncurry_apply, id_apply, lift_tmul, compr₂_apply, --- restrict_scalars_apply, function.comp_app, to_fun_eq_coe, lcurry_apply, --- linear_map.comp_apply] }) - - /-- Heterobasic version of `tensor_tensor_tensor_comm`: @@ -191,18 +214,11 @@ end Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ def tensor_tensor_tensor_comm : (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := -(assoc R A _ _ _).symm ≪≫ₗ begin - sorry - -end +(assoc R A _ _ _).symm ≪≫ₗ congr (right_comm R A _ _ _).symm 1 ≪≫ₗ assoc' R A _ _ _ @[simp] lemma tensor_tensor_tensor_comm_apply (m : M) (n : N) (p : P) (q : Q) : tensor_tensor_tensor_comm R A M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q) := -sorry --- let e₁ := (assoc R A (M ⊗[R] N) Q P).symm, --- e₁' := assoc R A M N (P ⊗[R] Q) in --- e₁ ≪≫ₗ congr (sorry : ((M ⊗[R] N) ⊗[A] P) ≃ₗ[A] ((M ⊗[A] P) ⊗[R] N)) (1 : Q ≃ₗ[R] Q) ≪≫ₗ --- sorry +rfl end comm_semiring From ca143e9d5bf18e50d87285c59b30ab05b1bc9ebb Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 01:45:28 +0000 Subject: [PATCH 11/23] finally done --- .../ring_theory/tensor_product.lean | 49 ++++++------------- .../from_mathlib/complexification.lean | 9 +++- 2 files changed, 22 insertions(+), 36 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 47a34ac8b..50a1d5824 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -136,24 +136,6 @@ rfl variables (R A M N P Q) -set_option pp.parens true -notation (name := tensor_product') - M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N - --- -- assoc R A _ _ _ ≪≫ₗ begin --- -- sorry --- -- end --- linear_equiv.of_linear --- (lift _) --- (lift _) _ _ --- let e₁ := (assoc R A M Q P).symm, --- e₂ := congr (tensor_product.comm A M P) (1 : Q ≃ₗ[R] Q), --- e₃ := (assoc R A P Q M) in --- e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) - -#print tensor_product.assoc -#check curry - /-- 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` @@ -186,31 +168,28 @@ linear_equiv.of_linear (curry_injective $ ext $ λ m n, linear_map.ext $ λ q, by exact eq.refl ((m ⊗ₜ[R] n) ⊗ₜ[R] q)) . -instance : is_scalar_tower R A (P →ₗ[A] ((M ⊗[A] P) ⊗[R] Q)) := linear_map.is_scalar_tower -instance : linear_map.compatible_smul - ((M ⊗[A] P) →ₗ[A] ((M ⊗[A] P) ⊗[R] Q)) - (M →ₗ[A] (P →ₗ[A] ((M ⊗[A] P) ⊗[R] Q))) - R - A := is_scalar_tower.compatible_smul - --- /-- A tensor product analogue of `mul_left_comm`. -/ + +-- /-- A tensor product analogue of `mul_right_comm`. -/ def right_comm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := begin + haveI : is_scalar_tower R A (P →ₗ[A] ((M ⊗[A] P) ⊗[R] Q)) := linear_map.is_scalar_tower, + haveI : linear_map.compatible_smul + ((M ⊗[A] P) →ₗ[A] ((M ⊗[A] P) ⊗[R] Q)) (M →ₗ[A] (P →ₗ[A] ((M ⊗[A] P) ⊗[R] Q))) R A := + is_scalar_tower.compatible_smul, refine linear_equiv.of_linear - (lift $ lift $ flip $ lcurry R A M Q _ ∘ₗ (mk A A (M ⊗[R] Q) P).flip) - (lift $ lift $ flip $ + (lift $ tensor_product.lift $ flip $ + lcurry R A M Q ((M ⊗[R] Q) ⊗[A] P) ∘ₗ (mk A A (M ⊗[R] Q) P).flip) + (tensor_product.lift $ lift $ flip $ (tensor_product.lcurry A M P ((M ⊗[A] P) ⊗[R] Q)).restrict_scalars R - ∘ₗ (mk R A (M ⊗[A] P) Q).flip) - (curry_injective _) - (curry_injective _), - sorry, - sorry, + ∘ₗ (mk R A (M ⊗[A] P) Q).flip) _ _, + { refine (tensor_product.ext $ ext $ λ m q, linear_map.ext $ λ p, _), + exact eq.refl ((m ⊗ₜ[R] q) ⊗ₜ[A] p) }, + { refine (curry_injective $ tensor_product.ext' $ λ m p, linear_map.ext $ λ q, _), + exact eq.refl ((m ⊗ₜ[A] p) ⊗ₜ[R] q) }, end /-- Heterobasic version of `tensor_tensor_tensor_comm`: - - Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ def tensor_tensor_tensor_comm : (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index e47f4ce9c..4cc0a050e 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -11,4 +11,11 @@ open_locale tensor_product noncomputable def quadratic_form.complexify (Q : quadratic_form ℝ V) : quadratic_form ℂ (ℂ ⊗[ℝ] V) := bilin_form.to_quadratic_form $ - (bilin_form.tmul' (linear_map.mul ℂ ℂ).to_bilin Q.associated) \ No newline at end of file + (bilin_form.tmul' (linear_map.mul ℂ ℂ).to_bilin Q.associated) + +lemma complexify_apply (Q : quadratic_form ℝ V) (c : ℂ) (v : V) : + Q.complexify (c ⊗ₜ v) = (c*c) * algebra_map _ _ (Q v) := +begin + change (c*c) * algebra_map _ _ (Q.associated.to_quadratic_form v) = _, + rw quadratic_form.to_quadratic_form_associated, +end From 05c387fc7d0ecbacc255b4c6739edb7170fa245e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 10:07:26 +0000 Subject: [PATCH 12/23] docstrings --- .../ring_theory/tensor_product.lean | 34 +++++++------------ 1 file changed, 13 insertions(+), 21 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 50a1d5824..9c880dc24 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -16,10 +16,10 @@ variables {R A M N P Q : Type*} open linear_map open _root_.algebra (lsmul) +open module (dual) namespace algebra_tensor_module - 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] @@ -75,6 +75,7 @@ def map_bilinear : (M →ₗ[A] P) →ₗ[A] (N →ₗ[R] Q) →ₗ[R] (M ⊗[R] map_add' := λ f₁ f₂, linear_map.ext $ λ g, map_add_left _ _ _, map_smul' := λ c f, linear_map.ext $ λ g, map_smul_left _ _ _, } +/-- Heterobasic `tensor_product.congr`. -/ def congr (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : (M ⊗[R] N) ≃ₗ[A] (P ⊗[R] Q) := linear_equiv.of_linear (map f g) (map f.symm g.symm) (ext $ λ m n, by simp; simp only [linear_equiv.apply_symm_apply]) @@ -102,15 +103,13 @@ linear_equiv.of_linear lemma rid_apply (a : A) (r : R) : rid R A (a ⊗ₜ r) = a * algebra_map R A r := rfl -/-- A tensor product analogue of `mul_left_comm`. -/ +/-- Heterobasic `tensor_product.left_comm`. -/ def left_comm : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q) := let e₁ := (assoc R A M Q P).symm, e₂ := congr (tensor_product.comm A M P) (1 : Q ≃ₗ[R] Q), e₃ := (assoc R A P Q M) in e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) -open module (dual) - /- Heterobasic `tensor_product.hom_tensor_hom_map` -/ def hom_tensor_hom_map : ((M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q)) →ₗ[A] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := lift map_bilinear @@ -136,28 +135,22 @@ rfl variables (R A M N P Q) -/-- 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`. -/ +/-- A variant of `algebra_tensor_module.uncurry`, where only the outermost map is +`A`-linear. -/ @[simps] def uncurry' : (N →ₗ[R] (Q →ₗ[R] P)) →ₗ[A] ((N ⊗[R] Q) →ₗ[R] 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, ring_hom.id_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`. -/ +/-- A variant of `algebra_tensor_module.lcurry`, where only the outermost map is +`A`-linear. -/ @[simps] def lcurry' : ((N ⊗[R] Q) →ₗ[R] P) →ₗ[A] (N →ₗ[R] (Q →ₗ[R] P)) := { to_fun := curry, map_add' := λ f g, rfl, map_smul' := λ c f, rfl } -/-- Heterobasic version of `tensor_product.assoc`: - -Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ +/-- A variant of `algebra_tensor_module.assoc`, where only the outermost map is +`A`-linear. -/ def assoc' : ((M ⊗[R] N) ⊗[R] Q) ≃ₗ[A] (M ⊗[R] (N ⊗[R] Q)) := linear_equiv.of_linear (lift $ lift $ lcurry' R A N _ Q ∘ₗ mk R A M (N ⊗[R] Q)) -- (lcurry R _ _ _ _) @@ -167,9 +160,8 @@ linear_equiv.of_linear by exact eq.refl (m ⊗ₜ[R] (n ⊗ₜ[R] q))) (curry_injective $ ext $ λ m n, linear_map.ext $ λ q, by exact eq.refl ((m ⊗ₜ[R] n) ⊗ₜ[R] q)) -. --- /-- A tensor product analogue of `mul_right_comm`. -/ +/-- A tensor product analogue of `mul_right_comm`. -/ def right_comm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := begin haveI : is_scalar_tower R A (P →ₗ[A] ((M ⊗[A] P) ⊗[R] Q)) := linear_map.is_scalar_tower, @@ -188,13 +180,13 @@ begin exact eq.refl ((m ⊗ₜ[A] p) ⊗ₜ[R] q) }, end -/-- Heterobasic version of `tensor_tensor_tensor_comm`: - -Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ +/-- Heterobasic version of `tensor_tensor_tensor_comm`. -/ def tensor_tensor_tensor_comm : (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := (assoc R A _ _ _).symm ≪≫ₗ congr (right_comm R A _ _ _).symm 1 ≪≫ₗ assoc' R A _ _ _ +variables {M N P Q} + @[simp] lemma tensor_tensor_tensor_comm_apply (m : M) (n : N) (p : P) (q : Q) : tensor_tensor_tensor_comm R A M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q) := rfl From 4b908e6af93e0a27fa9b10868ca3249b09f9334f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 13:37:07 +0000 Subject: [PATCH 13/23] banish another sorry --- src/for_mathlib/algebra/ring_quot.lean | 12 ++ .../ring_theory/tensor_product.lean | 33 +++- .../from_mathlib/complexification.lean | 147 +++++++++++++++++- 3 files changed, 190 insertions(+), 2 deletions(-) create mode 100644 src/for_mathlib/algebra/ring_quot.lean diff --git a/src/for_mathlib/algebra/ring_quot.lean b/src/for_mathlib/algebra/ring_quot.lean new file mode 100644 index 000000000..8973662bc --- /dev/null +++ b/src/for_mathlib/algebra/ring_quot.lean @@ -0,0 +1,12 @@ +import algebra.ring_quot + +variables {S R A : Type*} [comm_semiring S] [comm_semiring R] [semiring A] [algebra S A] + [algebra R A] (r : A → A → Prop) + +instance [has_smul R S] [is_scalar_tower R S A] : is_scalar_tower R S (ring_quot r) := +⟨λ r s ⟨a⟩, quot.induction_on a $ λ a', + by simpa only [ring_quot.smul_quot] using congr_arg (quot.mk _) (smul_assoc r s a' : _)⟩ + +instance [smul_comm_class R S A] : smul_comm_class R S (ring_quot r) := +⟨λ r s ⟨a⟩, quot.induction_on a $ λ a', + by simpa only [ring_quot.smul_quot] using congr_arg (quot.mk _) (smul_comm r s a' : _)⟩ diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 9c880dc24..b0b353e19 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -8,7 +8,7 @@ open tensor_product namespace tensor_product -variables {R A M N P Q : Type*} +variables {R A B C M N P Q : Type*} /-! ### The `A`-module structure on `A ⊗[R] M` @@ -196,3 +196,34 @@ end comm_semiring end algebra_tensor_module end tensor_product + +namespace algebra.tensor_product +variables {R S A B C : Type*} + +open_locale tensor_product + +variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] [semiring C] +variables [algebra R A] [algebra R B] [algebra R C] +variables [algebra S A] [algebra S C] +variables [algebra R S] [smul_comm_class R S A] [is_scalar_tower R S A] [is_scalar_tower R S C] + +/-- The `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/ +@[simps] +def include_left' : A →ₐ[S] A ⊗[R] B := +{ commutes' := by simp, + ..include_left_ring_hom } + +@[ext] +def ext' ⦃f g : (A ⊗[R] B) →ₐ[S] C⦄ + (ha : f.comp include_left' = g.comp include_left') + (hb : (f.restrict_scalars R).comp include_right = (g.restrict_scalars R).comp include_right) : + f = g := +begin + apply @alg_hom.to_linear_map_injective S (A ⊗[R] B) C _ _ _ _ _ _ _ _, + ext a b, + have := congr_arg2 (*) (alg_hom.congr_fun ha a) (alg_hom.congr_fun hb b), + dsimp at *, + rwa [←f.map_mul, ←g.map_mul, tmul_mul_tmul, _root_.one_mul, _root_.mul_one] at this, +end + +end algebra.tensor_product diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index 4cc0a050e..b4f2bec04 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -2,6 +2,7 @@ import linear_algebra.clifford_algebra.basic import data.complex.module import ring_theory.tensor_product import for_mathlib.linear_algebra.bilinear_form.tensor_product +import for_mathlib.algebra.ring_quot variables {V: Type*} [add_comm_group V] [module ℝ V] . @@ -13,9 +14,153 @@ noncomputable def quadratic_form.complexify (Q : quadratic_form ℝ V) : bilin_form.to_quadratic_form $ (bilin_form.tmul' (linear_map.mul ℂ ℂ).to_bilin Q.associated) -lemma complexify_apply (Q : quadratic_form ℝ V) (c : ℂ) (v : V) : +@[simp] lemma complexify_apply (Q : quadratic_form ℝ V) (c : ℂ) (v : V) : Q.complexify (c ⊗ₜ v) = (c*c) * algebra_map _ _ (Q v) := begin change (c*c) * algebra_map _ _ (Q.associated.to_quadratic_form v) = _, rw quadratic_form.to_quadratic_form_associated, end + +local attribute [-instance] module.complex_to_real + +section algebra_tower_instances + +instance free_algebra.algebra' : algebra ℝ (free_algebra ℂ (ℂ ⊗[ℝ] V)) := +(restrict_scalars.algebra ℝ ℂ (free_algebra ℂ (ℂ ⊗[ℝ] V)) : _) + +instance tensor_algebra.algebra' : algebra ℝ (tensor_algebra ℂ (ℂ ⊗[ℝ] V)) := +ring_quot.algebra _ + +instance tensor_algebra.is_scalar_tower' : is_scalar_tower ℝ ℂ (tensor_algebra ℂ (ℂ ⊗[ℝ] V)) := +ring_quot.is_scalar_tower _ + +local attribute [semireducible] clifford_algebra + +instance clifford_algebra.algebra' (Q : quadratic_form ℝ V) : + algebra ℝ (clifford_algebra Q.complexify) := +ring_quot.algebra (clifford_algebra.rel Q.complexify) + +instance clifford_algebra.is_scalar_tower (Q : quadratic_form ℝ V) : + is_scalar_tower ℝ ℂ (clifford_algebra Q.complexify) := +ring_quot.is_scalar_tower _ + +instance clifford_algebra.smul_comm_class (Q : quadratic_form ℝ V) : + smul_comm_class ℝ ℂ (clifford_algebra Q.complexify) := +ring_quot.smul_comm_class _ + +instance clifford_algebra.smul_comm_class' (Q : quadratic_form ℝ V) : + smul_comm_class ℂ ℝ (clifford_algebra Q.complexify) := +ring_quot.smul_comm_class _ + +end algebra_tower_instances + +local attribute [semireducible] clifford_algebra + +noncomputable def of_complexify_aux (Q : quadratic_form ℝ V) : + clifford_algebra Q →ₐ[ℝ] clifford_algebra Q.complexify := +clifford_algebra.lift Q begin + refine ⟨(clifford_algebra.ι Q.complexify).restrict_scalars ℝ ∘ₗ tensor_product.mk ℝ ℂ V 1, λ v, _⟩, + refine (clifford_algebra.ι_sq_scalar Q.complexify (1 ⊗ₜ v)).trans _, + rw [complexify_apply, one_mul, one_mul, ←is_scalar_tower.algebra_map_apply], +end + +@[simp] lemma of_complexify_aux_ι (Q : quadratic_form ℝ V) (v : V) : + of_complexify_aux Q (clifford_algebra.ι Q v) = clifford_algebra.ι Q.complexify (1 ⊗ₜ v) := +clifford_algebra.lift_ι_apply _ _ _ + +noncomputable def of_complexify (Q : quadratic_form ℝ V) : + ℂ ⊗[ℝ] clifford_algebra Q →ₐ[ℂ] clifford_algebra Q.complexify := +-- `algebra.tensor_product.product_left_alg_hom` doesn't work here :( +alg_hom.of_linear_map + (tensor_product.algebra_tensor_module.lift $ + let f : ℂ →ₗ[ℂ] _ := (algebra.lsmul ℂ (clifford_algebra Q.complexify)).to_linear_map in + linear_map.flip $ linear_map.flip (({ + to_fun := λ f : clifford_algebra Q.complexify →ₗ[ℂ] clifford_algebra Q.complexify, + linear_map.restrict_scalars ℝ f, + map_add' := λ f g, linear_map.ext $ λ x, rfl, + map_smul' := λ (c : ℂ) g, linear_map.ext $ λ x, rfl, + } : _ →ₗ[ℂ] _) ∘ₗ f) ∘ₗ (of_complexify_aux Q).to_linear_map) + (show (1 : ℂ) • of_complexify_aux Q 1 = 1, by simp only [map_one, one_smul]) + (λ x y, sorry) + +@[simp] lemma of_complexify_tmul_ι (Q : quadratic_form ℝ V) (z : ℂ) (v : V) : + of_complexify Q (z ⊗ₜ clifford_algebra.ι Q v) = clifford_algebra.ι _ (z ⊗ₜ v) := +begin + show z • of_complexify_aux Q (clifford_algebra.ι Q v) + = clifford_algebra.ι Q.complexify (z ⊗ₜ[ℝ] v), + rw [of_complexify_aux_ι, ←map_smul, tensor_product.smul_tmul', smul_eq_mul, mul_one], +end + +@[simp] lemma of_complexify_tmul_one (Q : quadratic_form ℝ V) (z : ℂ) : + of_complexify Q (z ⊗ₜ 1) = algebra_map _ _ z := +begin + show z • of_complexify_aux Q 1 = _, + rw [map_one, ←algebra.algebra_map_eq_smul_one], +end + +noncomputable def to_complexify (Q : quadratic_form ℝ V) : + clifford_algebra Q.complexify →ₐ[ℂ] ℂ ⊗[ℝ] clifford_algebra Q := +clifford_algebra.lift _ $ begin + let φ := tensor_product.algebra_tensor_module.map (linear_map.id : ℂ →ₗ[ℂ] ℂ) (clifford_algebra.ι Q), + refine ⟨φ, _⟩, + suffices : ∀ z v, φ (z ⊗ₜ v) * φ (z ⊗ₜ v) = algebra_map _ _ (Q.complexify (z ⊗ₜ v)), + { intro m, + induction m using tensor_product.induction_on with z v x y hx hy, + { simp }, + { exact this _ _ }, + { simp only [map_add], + -- not true :( + sorry } }, + intros z v, + suffices : ∀ v, φ (1 ⊗ₜ v) * φ (1 ⊗ₜ v) = algebra_map _ _ (Q v), + { have := congr_arg ((•) (z*z)) (this v), + rw [←smul_mul_smul, ←map_smul, tensor_product.smul_tmul', smul_eq_mul, mul_one] at this, + rw [this, complexify_apply, map_mul, algebra.smul_def, ←is_scalar_tower.algebra_map_apply] }, + intro v, + dsimp only [φ, tensor_product.algebra_tensor_module.map_tmul, complexify_apply, alg_hom.id_apply, + linear_map.id_apply, algebra.tensor_product.algebra_map_apply, algebra.tensor_product.tmul_mul_tmul], + rw [algebra.algebra_map_eq_smul_one, tensor_product.smul_tmul, ←algebra.algebra_map_eq_smul_one, + mul_one, clifford_algebra.ι_sq_scalar], +end + +@[simp] lemma to_complexify_ι (Q : quadratic_form ℝ V) (z : ℂ) (v : V) : + to_complexify Q (clifford_algebra.ι _ (z ⊗ₜ v)) = z ⊗ₜ clifford_algebra.ι Q v := +clifford_algebra.lift_ι_apply _ _ _ + +local attribute [ext] tensor_product.ext + +lemma to_complexify_comp_of_complexify (Q : quadratic_form ℝ V) : + (to_complexify Q).comp (of_complexify Q) = alg_hom.id _ _ := +begin + ext z, + { change to_complexify Q (of_complexify Q (z ⊗ₜ[ℝ] 1)) = z ⊗ₜ[ℝ] 1, + rw [of_complexify_tmul_one, alg_hom.commutes, algebra.tensor_product.algebra_map_apply, + algebra.id.map_eq_self] }, + { ext v, + change to_complexify Q (of_complexify Q (1 ⊗ₜ[ℝ] clifford_algebra.ι Q v)) + = 1 ⊗ₜ[ℝ] clifford_algebra.ι Q v, + rw [of_complexify_tmul_ι, to_complexify_ι] }, +end + +@[simp] lemma to_complexify_of_complexify (Q : quadratic_form ℝ V) (x : ℂ ⊗[ℝ] clifford_algebra Q) : + to_complexify Q (of_complexify Q x) = x := +alg_hom.congr_fun (to_complexify_comp_of_complexify Q : _) x + +lemma of_complexify_comp_to_complexify (Q : quadratic_form ℝ V) : + (of_complexify Q).comp (to_complexify Q) = alg_hom.id _ _ := +begin + ext, + show of_complexify Q (to_complexify Q (clifford_algebra.ι Q.complexify (1 ⊗ₜ[ℝ] x))) + = clifford_algebra.ι Q.complexify (1 ⊗ₜ[ℝ] x), + rw [to_complexify_ι, of_complexify_tmul_ι], +end + +@[simp] lemma of_complexify_to_complexify (Q : quadratic_form ℝ V) (x : clifford_algebra Q.complexify) : + of_complexify Q (to_complexify Q x) = x := +alg_hom.congr_fun (of_complexify_comp_to_complexify Q : _) x + +noncomputable def equiv_complexify (Q : quadratic_form ℝ V) : + clifford_algebra Q.complexify ≃ₐ[ℂ] ℂ ⊗[ℝ] clifford_algebra Q := +alg_equiv.of_alg_hom (to_complexify Q) (of_complexify Q) + (to_complexify_comp_of_complexify Q) + (of_complexify_comp_to_complexify Q) \ No newline at end of file From 7f5385cb78c5e7458e4c906841ca22e320e6cee4 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 13:59:30 +0000 Subject: [PATCH 14/23] one remains, but it's false --- .../ring_theory/tensor_product.lean | 44 +++++++++++++++++-- .../from_mathlib/complexification.lean | 12 +++-- 2 files changed, 48 insertions(+), 8 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index b0b353e19..288e4d785 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -198,21 +198,57 @@ end algebra_tensor_module end tensor_product namespace algebra.tensor_product -variables {R S A B C : Type*} +variables {R S A B C D : Type*} open_locale tensor_product -variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] [semiring C] -variables [algebra R A] [algebra R B] [algebra R C] +variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] [semiring C] [semiring D] +variables [algebra R A] [algebra R B] [algebra R C] [algebra R D] variables [algebra S A] [algebra S C] variables [algebra R S] [smul_comm_class R S A] [is_scalar_tower R S A] [is_scalar_tower R S C] -/-- The `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/ +/-- a stronger version of `alg_hom_of_linear_map_tensor_product` -/ +def alg_hom_of_linear_map_tensor_product' + (f : A ⊗[R] B →ₗ[S] C) + (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) + (w₂ : ∀ r, f ((algebra_map S A) r ⊗ₜ[R] 1) = (algebra_map S C) r): + A ⊗[R] B →ₐ[S] C := +{ map_one' := by rw [←(algebra_map S C).map_one, ←w₂, (algebra_map S A).map_one]; refl, + map_zero' := by rw [linear_map.to_fun_eq_coe, map_zero], + map_mul' := λ x y, by + { rw linear_map.to_fun_eq_coe, + apply tensor_product.induction_on x, + { rw [zero_mul, map_zero, zero_mul] }, + { intros a₁ b₁, + apply tensor_product.induction_on y, + { rw [mul_zero, map_zero, mul_zero] }, + { intros a₂ b₂, + rw [tmul_mul_tmul, w₁] }, + { intros x₁ x₂ h₁ h₂, + rw [mul_add, map_add, map_add, mul_add, h₁, h₂] } }, + { intros x₁ x₂ h₁ h₂, + rw [add_mul, map_add, map_add, add_mul, h₁, h₂] } }, + commutes' := λ r, by rw [linear_map.to_fun_eq_coe, algebra_map_apply, w₂], + .. f } + +@[simp] +lemma alg_hom_of_linear_map_tensor_product'_apply (f w₁ w₂ x) : + (alg_hom_of_linear_map_tensor_product' f w₁ w₂ : A ⊗[R] B →ₐ[R] C) x = f x := rfl + +/-- a stronger version of `map` -/ +def map' (f : A →ₐ[S] C) (g : B →ₐ[R] D) : A ⊗[R] B →ₐ[S] C ⊗[R] D := +alg_hom_of_linear_map_tensor_product' + (tensor_product.algebra_tensor_module.map f.to_linear_map g.to_linear_map) + (by simp) + (by simp [alg_hom.commutes]) + +/-- a stronger version of `include_left` -/ @[simps] def include_left' : A →ₐ[S] A ⊗[R] B := { commutes' := by simp, ..include_left_ring_hom } +/-- a stronger version of `ext` -/ @[ext] def ext' ⦃f g : (A ⊗[R] B) →ₐ[S] C⦄ (ha : f.comp include_left' = g.comp include_left') diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index b4f2bec04..01374c67c 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -70,8 +70,7 @@ clifford_algebra.lift_ι_apply _ _ _ noncomputable def of_complexify (Q : quadratic_form ℝ V) : ℂ ⊗[ℝ] clifford_algebra Q →ₐ[ℂ] clifford_algebra Q.complexify := --- `algebra.tensor_product.product_left_alg_hom` doesn't work here :( -alg_hom.of_linear_map +algebra.tensor_product.alg_hom_of_linear_map_tensor_product' (tensor_product.algebra_tensor_module.lift $ let f : ℂ →ₗ[ℂ] _ := (algebra.lsmul ℂ (clifford_algebra Q.complexify)).to_linear_map in linear_map.flip $ linear_map.flip (({ @@ -80,8 +79,13 @@ alg_hom.of_linear_map map_add' := λ f g, linear_map.ext $ λ x, rfl, map_smul' := λ (c : ℂ) g, linear_map.ext $ λ x, rfl, } : _ →ₗ[ℂ] _) ∘ₗ f) ∘ₗ (of_complexify_aux Q).to_linear_map) - (show (1 : ℂ) • of_complexify_aux Q 1 = 1, by simp only [map_one, one_smul]) - (λ x y, sorry) + (λ z₁ z₂ b₁ b₂, + show (z₁ * z₂) • of_complexify_aux Q (b₁ * b₂) + = z₁ • of_complexify_aux Q b₁ * z₂ • of_complexify_aux Q b₂, + by rw [map_mul, smul_mul_smul]) + (λ r, + show r • of_complexify_aux Q 1 = algebra_map ℂ (clifford_algebra Q.complexify) r, + by rw [map_one, algebra.algebra_map_eq_smul_one]) @[simp] lemma of_complexify_tmul_ι (Q : quadratic_form ℝ V) (z : ℂ) (v : V) : of_complexify Q (z ⊗ₜ clifford_algebra.ι Q v) = clifford_algebra.ι _ (z ⊗ₜ v) := From b1e7844696777ddb720f0e1580629a8481804664 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 22:12:16 +0000 Subject: [PATCH 15/23] fully sorry-free! --- .../ring_theory/tensor_product.lean | 4 + src/geometric_algebra/from_mathlib/basic.lean | 29 +++++- .../from_mathlib/complexification.lean | 91 +++++++++++++------ 3 files changed, 92 insertions(+), 32 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 288e4d785..fef484a4a 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -207,6 +207,10 @@ variables [algebra R A] [algebra R B] [algebra R C] [algebra R D] variables [algebra S A] [algebra S C] variables [algebra R S] [smul_comm_class R S A] [is_scalar_tower R S A] [is_scalar_tower R S C] +lemma algebra_map_tmul_one (r : R) : + algebra_map R A r ⊗ₜ[R] (1 : B) = 1 ⊗ₜ[R] algebra_map R B r := +by simpa only [algebra.algebra_map_eq_smul_one] using tensor_product.smul_tmul _ _ _ + /-- a stronger version of `alg_hom_of_linear_map_tensor_product` -/ def alg_hom_of_linear_map_tensor_product' (f : A ⊗[R] B →ₗ[S] C) diff --git a/src/geometric_algebra/from_mathlib/basic.lean b/src/geometric_algebra/from_mathlib/basic.lean index 537e61c25..b3d3c5389 100644 --- a/src/geometric_algebra/from_mathlib/basic.lean +++ b/src/geometric_algebra/from_mathlib/basic.lean @@ -4,10 +4,12 @@ Released under MIT license as described in the file LICENSE. Authors: Eric Wieser -/ import linear_algebra.clifford_algebra.basic +import linear_algebra.bilinear_map variables {R : Type*} [comm_ring R] variables {M : Type*} [add_comm_group M] [module R M] variables {Q : quadratic_form R M} +variables {A : Type*} notation `↑ₐ`:max x:max := algebra_map _ _ x @@ -16,9 +18,32 @@ namespace clifford_algebra -- if this fails then you have the wrong branch of mathlib example : ring (clifford_algebra Q) := infer_instance -variables (Q) -abbreviation clifford_hom (A : Type*) [semiring A] [algebra R A] := +variables (Q A) +abbreviation clifford_hom [semiring A] [algebra R A] := { f : M →ₗ[R] A // ∀ m, f m * f m = ↑ₐ(Q m) } + +variables {A} + +lemma preserves_iff_bilin [ring A] [algebra R A] (h2 : is_unit (2 : R)) + (f : M →ₗ[R] A) : + (∀ x, f x * f x = algebra_map _ _ (Q x)) ↔ + ((linear_map.mul R A).compl₂ f) ∘ₗ f + ((linear_map.mul R A).flip.compl₂ f) ∘ₗ f = + Q.polar_bilin.to_lin.compr₂ (algebra.linear_map R A) := +begin + simp_rw fun_like.ext_iff, + dsimp only [linear_map.compr₂_apply, linear_map.compl₂_apply, linear_map.comp_apply, + algebra.linear_map_apply, linear_map.mul_apply', bilin_form.to_lin_apply, linear_map.add_apply, + linear_map.flip_apply], + have h2a := h2.map (algebra_map R A), + refine ⟨λ h x y, _, λ h x, _⟩, + { rw [quadratic_form.polar_bilin_apply, quadratic_form.polar, sub_sub, map_sub, map_add, + ←h x, ←h y, ←h (x + y), eq_sub_iff_add_eq, map_add, + add_mul, mul_add, mul_add, add_comm (f x * f x) (f x * f y), + add_add_add_comm] }, + { apply h2a.mul_left_cancel, + simp_rw [←algebra.smul_def, two_smul], + rw [h x x, quadratic_form.polar_bilin_apply, quadratic_form.polar_self, two_mul, map_add], }, +end variables {Q} /-- TODO: work out what the necessary conditions are here, then make this an instance -/ diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index 01374c67c..bb155a88f 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -3,13 +3,28 @@ import data.complex.module import ring_theory.tensor_product import for_mathlib.linear_algebra.bilinear_form.tensor_product import for_mathlib.algebra.ring_quot +import geometric_algebra.from_mathlib.basic + +/-! # Complexification of a clifford algebra + +In this file we show the isomorphism + +* `equiv_complexify Q : clifford_algebra Q.complexify ≃ₐ[ℂ] (ℂ ⊗[ℝ] clifford_algebra Q)` + +where + +* `quadratic_form.complexify Q : quadratic_form ℂ (ℂ ⊗[ℝ] V)` + +-/ variables {V: Type*} [add_comm_group V] [module ℝ V] . open_locale tensor_product -noncomputable def quadratic_form.complexify (Q : quadratic_form ℝ V) : +namespace quadratic_form + +noncomputable def complexify (Q : quadratic_form ℝ V) : quadratic_form ℂ (ℂ ⊗[ℝ] V) := bilin_form.to_quadratic_form $ (bilin_form.tmul' (linear_map.mul ℂ ℂ).to_bilin Q.associated) @@ -21,6 +36,26 @@ begin rw quadratic_form.to_quadratic_form_associated, end +lemma complexify.polar_bilin (Q : quadratic_form ℝ V) : + Q.complexify.polar_bilin = (linear_map.mul ℂ ℂ).to_bilin.tmul' Q.polar_bilin := +begin + apply bilin_form.to_lin.injective _, + ext v w : 6, + change polar (Q.complexify) (1 ⊗ₜ[ℝ] v) (1 ⊗ₜ[ℝ] w) = 1 * 1 * algebra_map _ _ (polar Q v w), + simp_rw [polar, complexify_apply, ←tensor_product.tmul_add, complexify_apply, one_mul, + _root_.map_sub], +end + +@[simp] lemma complexify_polar_apply (Q : quadratic_form ℝ V) + (c₁ : ℂ) (v₁ : V) (c₂ : ℂ) (v₂ : V): + polar Q.complexify (c₁ ⊗ₜ[ℝ] v₁) (c₂ ⊗ₜ[ℝ] v₂) = (c₁ * c₂) * algebra_map _ _ (polar Q v₁ v₂) := +bilin_form.congr_fun (complexify.polar_bilin Q) _ _ + + + +end quadratic_form + + local attribute [-instance] module.complex_to_real section algebra_tower_instances @@ -54,18 +89,21 @@ ring_quot.smul_comm_class _ end algebra_tower_instances +open clifford_algebra (ι) +open quadratic_form (complexify_apply) + local attribute [semireducible] clifford_algebra noncomputable def of_complexify_aux (Q : quadratic_form ℝ V) : clifford_algebra Q →ₐ[ℝ] clifford_algebra Q.complexify := clifford_algebra.lift Q begin - refine ⟨(clifford_algebra.ι Q.complexify).restrict_scalars ℝ ∘ₗ tensor_product.mk ℝ ℂ V 1, λ v, _⟩, + refine ⟨(ι Q.complexify).restrict_scalars ℝ ∘ₗ tensor_product.mk ℝ ℂ V 1, λ v, _⟩, refine (clifford_algebra.ι_sq_scalar Q.complexify (1 ⊗ₜ v)).trans _, rw [complexify_apply, one_mul, one_mul, ←is_scalar_tower.algebra_map_apply], end @[simp] lemma of_complexify_aux_ι (Q : quadratic_form ℝ V) (v : V) : - of_complexify_aux Q (clifford_algebra.ι Q v) = clifford_algebra.ι Q.complexify (1 ⊗ₜ v) := + of_complexify_aux Q (ι Q v) = ι Q.complexify (1 ⊗ₜ v) := clifford_algebra.lift_ι_apply _ _ _ noncomputable def of_complexify (Q : quadratic_form ℝ V) : @@ -88,10 +126,10 @@ algebra.tensor_product.alg_hom_of_linear_map_tensor_product' by rw [map_one, algebra.algebra_map_eq_smul_one]) @[simp] lemma of_complexify_tmul_ι (Q : quadratic_form ℝ V) (z : ℂ) (v : V) : - of_complexify Q (z ⊗ₜ clifford_algebra.ι Q v) = clifford_algebra.ι _ (z ⊗ₜ v) := + of_complexify Q (z ⊗ₜ ι Q v) = ι _ (z ⊗ₜ v) := begin - show z • of_complexify_aux Q (clifford_algebra.ι Q v) - = clifford_algebra.ι Q.complexify (z ⊗ₜ[ℝ] v), + show z • of_complexify_aux Q (ι Q v) + = ι Q.complexify (z ⊗ₜ[ℝ] v), rw [of_complexify_aux_ι, ←map_smul, tensor_product.smul_tmul', smul_eq_mul, mul_one], end @@ -102,33 +140,26 @@ begin rw [map_one, ←algebra.algebra_map_eq_smul_one], end +localized "notation (name := tensor_product) + M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N" in tensor_product + + noncomputable def to_complexify (Q : quadratic_form ℝ V) : clifford_algebra Q.complexify →ₐ[ℂ] ℂ ⊗[ℝ] clifford_algebra Q := clifford_algebra.lift _ $ begin - let φ := tensor_product.algebra_tensor_module.map (linear_map.id : ℂ →ₗ[ℂ] ℂ) (clifford_algebra.ι Q), + let φ := tensor_product.algebra_tensor_module.map (linear_map.id : ℂ →ₗ[ℂ] ℂ) (ι Q), refine ⟨φ, _⟩, - suffices : ∀ z v, φ (z ⊗ₜ v) * φ (z ⊗ₜ v) = algebra_map _ _ (Q.complexify (z ⊗ₜ v)), - { intro m, - induction m using tensor_product.induction_on with z v x y hx hy, - { simp }, - { exact this _ _ }, - { simp only [map_add], - -- not true :( - sorry } }, - intros z v, - suffices : ∀ v, φ (1 ⊗ₜ v) * φ (1 ⊗ₜ v) = algebra_map _ _ (Q v), - { have := congr_arg ((•) (z*z)) (this v), - rw [←smul_mul_smul, ←map_smul, tensor_product.smul_tmul', smul_eq_mul, mul_one] at this, - rw [this, complexify_apply, map_mul, algebra.smul_def, ←is_scalar_tower.algebra_map_apply] }, - intro v, - dsimp only [φ, tensor_product.algebra_tensor_module.map_tmul, complexify_apply, alg_hom.id_apply, - linear_map.id_apply, algebra.tensor_product.algebra_map_apply, algebra.tensor_product.tmul_mul_tmul], - rw [algebra.algebra_map_eq_smul_one, tensor_product.smul_tmul, ←algebra.algebra_map_eq_smul_one, - mul_one, clifford_algebra.ι_sq_scalar], + rw clifford_algebra.preserves_iff_bilin _ (is_unit.mk0 (2 : ℂ) two_ne_zero), + ext v w, + change (1 * 1) ⊗ₜ[ℝ] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[ℝ] (ι Q w * ι Q v) = + quadratic_form.polar (Q.complexify) (1 ⊗ₜ[ℝ] v) (1 ⊗ₜ[ℝ] w) ⊗ₜ[ℝ] 1, + rw [← tensor_product.tmul_add, clifford_algebra.ι_mul_ι_add_swap, + quadratic_form.complexify_polar_apply, one_mul, one_mul, + algebra.tensor_product.algebra_map_tmul_one], end @[simp] lemma to_complexify_ι (Q : quadratic_form ℝ V) (z : ℂ) (v : V) : - to_complexify Q (clifford_algebra.ι _ (z ⊗ₜ v)) = z ⊗ₜ clifford_algebra.ι Q v := + to_complexify Q (ι _ (z ⊗ₜ v)) = z ⊗ₜ ι Q v := clifford_algebra.lift_ι_apply _ _ _ local attribute [ext] tensor_product.ext @@ -141,8 +172,8 @@ begin rw [of_complexify_tmul_one, alg_hom.commutes, algebra.tensor_product.algebra_map_apply, algebra.id.map_eq_self] }, { ext v, - change to_complexify Q (of_complexify Q (1 ⊗ₜ[ℝ] clifford_algebra.ι Q v)) - = 1 ⊗ₜ[ℝ] clifford_algebra.ι Q v, + change to_complexify Q (of_complexify Q (1 ⊗ₜ[ℝ] ι Q v)) + = 1 ⊗ₜ[ℝ] ι Q v, rw [of_complexify_tmul_ι, to_complexify_ι] }, end @@ -154,8 +185,8 @@ lemma of_complexify_comp_to_complexify (Q : quadratic_form ℝ V) : (of_complexify Q).comp (to_complexify Q) = alg_hom.id _ _ := begin ext, - show of_complexify Q (to_complexify Q (clifford_algebra.ι Q.complexify (1 ⊗ₜ[ℝ] x))) - = clifford_algebra.ι Q.complexify (1 ⊗ₜ[ℝ] x), + show of_complexify Q (to_complexify Q (ι Q.complexify (1 ⊗ₜ[ℝ] x))) + = ι Q.complexify (1 ⊗ₜ[ℝ] x), rw [to_complexify_ι, of_complexify_tmul_ι], end From f60556e8644b8ef13abe786a1dc674da34d01599 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 22:34:13 +0000 Subject: [PATCH 16/23] docstrings --- .../ring_theory/tensor_product.lean | 9 +++++ .../from_mathlib/complexification.lean | 36 ++++++++++--------- 2 files changed, 29 insertions(+), 16 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index fef484a4a..971c7bb96 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -1,6 +1,15 @@ import ring_theory.tensor_product import linear_algebra.dual +/-! # Extras for `ring_theory.tensor_product` + +This file in mathlib starts with some heterobasic results, but quickly drops back to forcing +various rings or algebra to be equal. This isn't enough for us when trying to base change a +quadratic form. + +https://github.com/leanprover-community/mathlib4/pull/6035 adds some of these results to mathlib4. +-/ + universes u v₁ v₂ v₃ v₄ open_locale tensor_product diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index bb155a88f..d2417991e 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -9,23 +9,23 @@ import geometric_algebra.from_mathlib.basic In this file we show the isomorphism -* `equiv_complexify Q : clifford_algebra Q.complexify ≃ₐ[ℂ] (ℂ ⊗[ℝ] clifford_algebra Q)` +* `clifford_algebra.equiv_complexify Q : clifford_algebra Q.complexify ≃ₐ[ℂ] (ℂ ⊗[ℝ] clifford_algebra Q)` where * `quadratic_form.complexify Q : quadratic_form ℂ (ℂ ⊗[ℝ] V)` +This covers §2.2 of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf. -/ -variables {V: Type*} [add_comm_group V] [module ℝ V] -. +variables {V : Type*} [add_comm_group V] [module ℝ V] open_locale tensor_product namespace quadratic_form -noncomputable def complexify (Q : quadratic_form ℝ V) : - quadratic_form ℂ (ℂ ⊗[ℝ] V) := +/-- The complexification of a quadratic form, defined by $Q_ℂ(z ⊗ v) = z^2Q(v)$. -/ +noncomputable def complexify (Q : quadratic_form ℝ V) : quadratic_form ℂ (ℂ ⊗[ℝ] V) := bilin_form.to_quadratic_form $ (bilin_form.tmul' (linear_map.mul ℂ ℂ).to_bilin Q.associated) @@ -51,11 +51,9 @@ end polar Q.complexify (c₁ ⊗ₜ[ℝ] v₁) (c₂ ⊗ₜ[ℝ] v₂) = (c₁ * c₂) * algebra_map _ _ (polar Q v₁ v₂) := bilin_form.congr_fun (complexify.polar_bilin Q) _ _ - - end quadratic_form - +-- this instance is nasty local attribute [-instance] module.complex_to_real section algebra_tower_instances @@ -89,11 +87,10 @@ ring_quot.smul_comm_class _ end algebra_tower_instances -open clifford_algebra (ι) +namespace clifford_algebra open quadratic_form (complexify_apply) -local attribute [semireducible] clifford_algebra - +/-- Auxiliary construction: note this is really just a heterobasic `clifford_algebra.map`. -/ noncomputable def of_complexify_aux (Q : quadratic_form ℝ V) : clifford_algebra Q →ₐ[ℝ] clifford_algebra Q.complexify := clifford_algebra.lift Q begin @@ -106,6 +103,8 @@ end of_complexify_aux Q (ι Q v) = ι Q.complexify (1 ⊗ₜ v) := clifford_algebra.lift_ι_apply _ _ _ +/-- Convert from the complexified clifford algebra to the clifford algebra over a complexified +module. -/ noncomputable def of_complexify (Q : quadratic_form ℝ V) : ℂ ⊗[ℝ] clifford_algebra Q →ₐ[ℂ] clifford_algebra Q.complexify := algebra.tensor_product.alg_hom_of_linear_map_tensor_product' @@ -140,10 +139,8 @@ begin rw [map_one, ←algebra.algebra_map_eq_smul_one], end -localized "notation (name := tensor_product) - M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N" in tensor_product - - +/-- Convert from the clifford algebra over a complexified module to the complexified clifford +algebra. -/ noncomputable def to_complexify (Q : quadratic_form ℝ V) : clifford_algebra Q.complexify →ₐ[ℂ] ℂ ⊗[ℝ] clifford_algebra Q := clifford_algebra.lift _ $ begin @@ -194,8 +191,15 @@ end of_complexify Q (to_complexify Q x) = x := alg_hom.congr_fun (of_complexify_comp_to_complexify Q : _) x +/-- Complexifying the vector space of a clifford algebra is isomorphic as a ℂ-algebra to +complexifying the clifford algebra itself; $𝒞ℓ(ℂ ⊗ V, Q_ℂ) \iso ℂ ⊗ 𝒞ℓ(V, Q)$. + +This is `clifford_algebra.to_complexify` and `clifford_algebra.of_complexify` as an equivalence. -/ +@[simps] noncomputable def equiv_complexify (Q : quadratic_form ℝ V) : clifford_algebra Q.complexify ≃ₐ[ℂ] ℂ ⊗[ℝ] clifford_algebra Q := alg_equiv.of_alg_hom (to_complexify Q) (of_complexify Q) (to_complexify_comp_of_complexify Q) - (of_complexify_comp_to_complexify Q) \ No newline at end of file + (of_complexify_comp_to_complexify Q) + +end clifford_algebra From 69a38ce19721229f5d55178d790668be2d6030d8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 22 Jul 2023 10:22:05 +0000 Subject: [PATCH 17/23] generalize --- .../from_mathlib/complexification.lean | 57 +++++++++++++------ 1 file changed, 39 insertions(+), 18 deletions(-) diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index d2417991e..1ee772d72 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -18,41 +18,61 @@ where This covers §2.2 of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf. -/ -variables {V : Type*} [add_comm_group V] [module ℝ V] +variables {R A V : Type*} open_locale tensor_product namespace quadratic_form -/-- The complexification of a quadratic form, defined by $Q_ℂ(z ⊗ v) = z^2Q(v)$. -/ -noncomputable def complexify (Q : quadratic_form ℝ V) : quadratic_form ℂ (ℂ ⊗[ℝ] V) := +variables [comm_ring R] [comm_ring A] [algebra R A] [invertible (2 : R)] +variables [add_comm_group V] [module R V] + +variables (A) + +/-- Change the base of a quadratic form, defined by $Q_A(a ⊗ v) = a^2Q(v)$. -/ +def base_change (Q : quadratic_form R V) : quadratic_form A (A ⊗[R] V) := bilin_form.to_quadratic_form $ - (bilin_form.tmul' (linear_map.mul ℂ ℂ).to_bilin Q.associated) + (bilin_form.tmul' (linear_map.mul A A).to_bilin $ quadratic_form.associated Q) -@[simp] lemma complexify_apply (Q : quadratic_form ℝ V) (c : ℂ) (v : V) : - Q.complexify (c ⊗ₜ v) = (c*c) * algebra_map _ _ (Q v) := +variables {A} + +@[simp] lemma base_change_apply (Q : quadratic_form R V) (c : A) (v : V) : + Q.base_change A (c ⊗ₜ v) = (c*c) * algebra_map _ _ (Q v) := begin change (c*c) * algebra_map _ _ (Q.associated.to_quadratic_form v) = _, rw quadratic_form.to_quadratic_form_associated, end -lemma complexify.polar_bilin (Q : quadratic_form ℝ V) : - Q.complexify.polar_bilin = (linear_map.mul ℂ ℂ).to_bilin.tmul' Q.polar_bilin := +variables (A) + +lemma base_change.polar_bilin (Q : quadratic_form R V) : + polar_bilin (Q.base_change A) = (linear_map.mul A A).to_bilin.tmul' Q.polar_bilin := begin apply bilin_form.to_lin.injective _, ext v w : 6, - change polar (Q.complexify) (1 ⊗ₜ[ℝ] v) (1 ⊗ₜ[ℝ] w) = 1 * 1 * algebra_map _ _ (polar Q v w), - simp_rw [polar, complexify_apply, ←tensor_product.tmul_add, complexify_apply, one_mul, + change polar (Q.base_change A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) = 1 * 1 * algebra_map _ _ (polar Q v w), + simp_rw [polar, base_change_apply, ←tensor_product.tmul_add, base_change_apply, one_mul, _root_.map_sub], end -@[simp] lemma complexify_polar_apply (Q : quadratic_form ℝ V) - (c₁ : ℂ) (v₁ : V) (c₂ : ℂ) (v₂ : V): - polar Q.complexify (c₁ ⊗ₜ[ℝ] v₁) (c₂ ⊗ₜ[ℝ] v₂) = (c₁ * c₂) * algebra_map _ _ (polar Q v₁ v₂) := -bilin_form.congr_fun (complexify.polar_bilin Q) _ _ +@[simp] lemma base_change_polar_apply (Q : quadratic_form R V) + (c₁ : A) (v₁ : V) (c₂ : A) (v₂ : V) : + polar (Q.base_change A) (c₁ ⊗ₜ[R] v₁) (c₂ ⊗ₜ[R] v₂) + = (c₁ * c₂) * algebra_map _ _ (polar Q v₁ v₂) := +bilin_form.congr_fun (base_change.polar_bilin A Q) _ _ + + +variables {A} + +/-- The complexification of a quadratic form, defined by $Q_ℂ(z ⊗ v) = z^2Q(v)$. -/ +@[reducible] +noncomputable def complexify [module ℝ V] (Q : quadratic_form ℝ V) : quadratic_form ℂ (ℂ ⊗[ℝ] V) := +Q.base_change ℂ end quadratic_form +variables [add_comm_group V] [module ℝ V] + -- this instance is nasty local attribute [-instance] module.complex_to_real @@ -88,7 +108,7 @@ ring_quot.smul_comm_class _ end algebra_tower_instances namespace clifford_algebra -open quadratic_form (complexify_apply) +open quadratic_form (base_change_apply) /-- Auxiliary construction: note this is really just a heterobasic `clifford_algebra.map`. -/ noncomputable def of_complexify_aux (Q : quadratic_form ℝ V) : @@ -96,7 +116,7 @@ noncomputable def of_complexify_aux (Q : quadratic_form ℝ V) : clifford_algebra.lift Q begin refine ⟨(ι Q.complexify).restrict_scalars ℝ ∘ₗ tensor_product.mk ℝ ℂ V 1, λ v, _⟩, refine (clifford_algebra.ι_sq_scalar Q.complexify (1 ⊗ₜ v)).trans _, - rw [complexify_apply, one_mul, one_mul, ←is_scalar_tower.algebra_map_apply], + rw [base_change_apply, one_mul, one_mul, ←is_scalar_tower.algebra_map_apply], end @[simp] lemma of_complexify_aux_ι (Q : quadratic_form ℝ V) (v : V) : @@ -151,7 +171,7 @@ clifford_algebra.lift _ $ begin change (1 * 1) ⊗ₜ[ℝ] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[ℝ] (ι Q w * ι Q v) = quadratic_form.polar (Q.complexify) (1 ⊗ₜ[ℝ] v) (1 ⊗ₜ[ℝ] w) ⊗ₜ[ℝ] 1, rw [← tensor_product.tmul_add, clifford_algebra.ι_mul_ι_add_swap, - quadratic_form.complexify_polar_apply, one_mul, one_mul, + quadratic_form.base_change_polar_apply, one_mul, one_mul, algebra.tensor_product.algebra_map_tmul_one], end @@ -187,7 +207,8 @@ begin rw [to_complexify_ι, of_complexify_tmul_ι], end -@[simp] lemma of_complexify_to_complexify (Q : quadratic_form ℝ V) (x : clifford_algebra Q.complexify) : +@[simp] lemma of_complexify_to_complexify + (Q : quadratic_form ℝ V) (x : clifford_algebra Q.complexify) : of_complexify Q (to_complexify Q x) = x := alg_hom.congr_fun (of_complexify_comp_to_complexify Q : _) x From f7917e3af7006fcf527c469754caa26a943c90e5 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 3 Aug 2023 20:56:17 +0000 Subject: [PATCH 18/23] involution lemma --- .../ring_theory/tensor_product.lean | 4 ++++ .../from_mathlib/complexification.lean | 22 +++++++++++++++++-- 2 files changed, 24 insertions(+), 2 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 971c7bb96..4b748227d 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -255,6 +255,10 @@ alg_hom_of_linear_map_tensor_product' (by simp) (by simp [alg_hom.commutes]) +@[simp] lemma map'_tmul (f : A →ₐ[S] C) (g : B →ₐ[R] D) (a : A) (b : B) : + map' f g (a ⊗ₜ b) = f a ⊗ₜ g b := +rfl + /-- a stronger version of `include_left` -/ @[simps] def include_left' : A →ₐ[S] A ⊗[R] B := diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index 1ee772d72..145434989 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -1,4 +1,4 @@ -import linear_algebra.clifford_algebra.basic +import linear_algebra.clifford_algebra.conjugation import data.complex.module import ring_theory.tensor_product import for_mathlib.linear_algebra.bilinear_form.tensor_product @@ -18,7 +18,8 @@ where This covers §2.2 of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf. -/ -variables {R A V : Type*} +universes uR uA uV +variables {R : Type uR} {A : Type uA} {V : Type uV} open_locale tensor_product @@ -179,6 +180,23 @@ end to_complexify Q (ι _ (z ⊗ₜ v)) = z ⊗ₜ ι Q v := clifford_algebra.lift_ι_apply _ _ _ +lemma to_complexify_comp_involute (Q : quadratic_form ℝ V) : + (to_complexify Q).comp (involute : clifford_algebra Q.complexify →ₐ[ℂ] _) = + (algebra.tensor_product.map' (alg_hom.id _ _) involute).comp (to_complexify Q) := +begin + ext v, + show to_complexify Q (involute (ι Q.complexify (1 ⊗ₜ[ℝ] v))) + = (algebra.tensor_product.map' _ involute) (to_complexify Q (ι Q.complexify (1 ⊗ₜ[ℝ] v))), + rw [to_complexify_ι, involute_ι, map_neg, to_complexify_ι, algebra.tensor_product.map'_tmul, + alg_hom.id_apply, involute_ι, tensor_product.tmul_neg], +end + +/-- The involution acts only on the right of the tensor product. -/ +lemma to_complexify_involute (Q : quadratic_form ℝ V) (x : clifford_algebra Q.complexify) : + to_complexify Q (involute x) = + tensor_product.map linear_map.id (involute.to_linear_map) (to_complexify Q x) := +fun_like.congr_fun (to_complexify_comp_involute Q) x + local attribute [ext] tensor_product.ext lemma to_complexify_comp_of_complexify (Q : quadratic_form ℝ V) : From c65cc7bd2d9e6abba28655ca63c1799f8bdae98c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 4 Aug 2023 08:54:56 +0000 Subject: [PATCH 19/23] complexification of reverse is also trivial But not trivially proven! --- .../ring_theory/tensor_product.lean | 23 +++++++++++- .../from_mathlib/complexification.lean | 35 ++++++++++++++++++- .../from_mathlib/conjugation.lean | 18 ++++++++++ 3 files changed, 74 insertions(+), 2 deletions(-) diff --git a/src/for_mathlib/ring_theory/tensor_product.lean b/src/for_mathlib/ring_theory/tensor_product.lean index 4b748227d..ff0f7e227 100644 --- a/src/for_mathlib/ring_theory/tensor_product.lean +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -17,7 +17,7 @@ open tensor_product namespace tensor_product -variables {R A B C M N P Q : Type*} +variables {R A B C M N P Q P' Q' : Type*} /-! ### The `A`-module structure on `A ⊗[R] M` @@ -35,6 +35,8 @@ 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] variables [add_comm_monoid Q] [module R Q] +variables [add_comm_monoid P'] [module R P'] [module A P'] [is_scalar_tower R A P'] +variables [add_comm_monoid Q'] [module R Q'] /-- Heterobasic `tensor_product.map`. -/ def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] Q := @@ -43,10 +45,29 @@ lift $ (show (Q →ₗ[R] P ⊗ Q) →ₗ[A] N →ₗ[R] P ⊗[R] Q, map_add' := λ h₁ h₂, linear_map.add_comp g h₂ h₁, map_smul' := λ c h, linear_map.smul_comp c h g }) ∘ₗ mk R A P Q ∘ₗ f +theorem map_apply (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (x) : + map f g x = tensor_product.map (f.restrict_scalars R) g x := rfl + @[simp] theorem map_tmul (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) : map f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl +@[simp] theorem map_id : + map (linear_map.id : M →ₗ[A] M) (linear_map.id : N →ₗ[R] N) = linear_map.id := +by ext; refl + +theorem map_id_apply (x) : + map (linear_map.id : M →ₗ[A] M) (linear_map.id : N →ₗ[R] N) x = x := +fun_like.congr_fun map_id x + +theorem map_comp (f : P →ₗ[A] P') (f' : M →ₗ[A] P) (g : Q →ₗ[R] Q') (g' : N →ₗ[R] Q) : + map (f.comp f') (g.comp g') = (map f g).comp (map f' g') := +by { ext, refl } + +theorem map_map (f : P →ₗ[A] P') (f' : M →ₗ[A] P) (g : Q →ₗ[R] Q') (g' : N →ₗ[R] Q) (x) : + map f g (map f' g' x) = map (f.comp f') (g.comp g') x:= +fun_like.congr_fun (map_comp f f' g g').symm x + lemma map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (f₁ + f₂) g = map f₁ g + map f₂ g := begin ext, diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index 145434989..9da68861e 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -1,9 +1,10 @@ -import linear_algebra.clifford_algebra.conjugation import data.complex.module import ring_theory.tensor_product +import for_mathlib.linear_algebra.tensor_product.opposite import for_mathlib.linear_algebra.bilinear_form.tensor_product import for_mathlib.algebra.ring_quot import geometric_algebra.from_mathlib.basic +import geometric_algebra.from_mathlib.conjugation /-! # Complexification of a clifford algebra @@ -197,6 +198,38 @@ lemma to_complexify_involute (Q : quadratic_form ℝ V) (x : clifford_algebra Q. tensor_product.map linear_map.id (involute.to_linear_map) (to_complexify Q x) := fun_like.congr_fun (to_complexify_comp_involute Q) x +open mul_opposite + +/-- Auxiliary lemma used to prove `to_complexify_reverse` without needing induction. -/ +lemma to_complexify_comp_reverse_aux (Q : quadratic_form ℝ V) : + (to_complexify Q).op.comp (reverse_aux Q.complexify) = + ((algebra.tensor_product.op_alg_equiv ℂ).to_alg_hom.comp $ + (algebra.tensor_product.map' ((alg_hom.id ℂ ℂ).to_opposite commute.all) (reverse_aux Q)).comp + (to_complexify Q)) := +begin + ext v, + show + op (to_complexify Q (reverse (ι Q.complexify (1 ⊗ₜ[ℝ] v)))) = + algebra.tensor_product.op_alg_equiv ℂ + (algebra.tensor_product.map' ((alg_hom.id ℂ ℂ).to_opposite commute.all) (reverse_aux Q) + (to_complexify Q (ι Q.complexify (1 ⊗ₜ[ℝ] v)))), + rw [to_complexify_ι, reverse_ι, to_complexify_ι, algebra.tensor_product.map'_tmul, + algebra.tensor_product.op_alg_equiv_tmul, unop_reverse_aux, reverse_ι], + refl, +end + +/-- The reverse acts only on the right of the tensor product. -/ +lemma to_complexify_reverse (Q : quadratic_form ℝ V) (x : clifford_algebra Q.complexify) : + to_complexify Q (reverse x) = + tensor_product.map linear_map.id (reverse : _ →ₗ[ℝ] _) (to_complexify Q x) := +begin + have := fun_like.congr_fun (to_complexify_comp_reverse_aux Q) x, + refine (congr_arg unop this).trans _; clear this, + refine (tensor_product.algebra_tensor_module.map_map _ _ _ _ _).trans _, + erw [←reverse_eq_reverse_aux, alg_hom.to_linear_map_to_opposite, + tensor_product.algebra_tensor_module.map_apply], +end + local attribute [ext] tensor_product.ext lemma to_complexify_comp_of_complexify (Q : quadratic_form ℝ V) : diff --git a/src/geometric_algebra/from_mathlib/conjugation.lean b/src/geometric_algebra/from_mathlib/conjugation.lean index 025d72662..b28d77dbc 100644 --- a/src/geometric_algebra/from_mathlib/conjugation.lean +++ b/src/geometric_algebra/from_mathlib/conjugation.lean @@ -21,6 +21,24 @@ The links above will take you to the collection of mathlib theorems. namespace clifford_algebra + +open mul_opposite + +section +variables (Q) + +def reverse_aux : clifford_algebra Q →ₐ[R] (clifford_algebra Q)ᵐᵒᵖ := + clifford_algebra.lift Q ⟨(op_linear_equiv R).to_linear_map.comp (ι Q), + λ m, unop_injective $ by simp⟩ + +lemma reverse_eq_reverse_aux : + reverse = (op_linear_equiv R).symm.to_linear_map ∘ₗ (reverse_aux Q).to_linear_map := rfl + +@[simp] lemma unop_reverse_aux (x : clifford_algebra Q) : + unop (reverse_aux Q x) = reverse x := rfl + +end + section reverse open mul_opposite From f6e5a6f246ae7e22243d689779cb5e32dfa27d5e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 4 Aug 2023 11:19:03 +0000 Subject: [PATCH 20/23] fix docstrings --- .../from_mathlib/complexification.lean | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index 9da68861e..d587bd39e 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -11,12 +11,22 @@ import geometric_algebra.from_mathlib.conjugation In this file we show the isomorphism * `clifford_algebra.equiv_complexify Q : clifford_algebra Q.complexify ≃ₐ[ℂ] (ℂ ⊗[ℝ] clifford_algebra Q)` + with forward direction `clifford_algebra.to_complexify Q` and reverse direction + `clifford_algebra.of_complexify Q`. where -* `quadratic_form.complexify Q : quadratic_form ℂ (ℂ ⊗[ℝ] V)` +* `quadratic_form.complexify Q : quadratic_form ℂ (ℂ ⊗[ℝ] V)`, which is defined in terms of a more + general `quadratic_form.base_change`. This covers §2.2 of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf. + +We show: + +* `clifford_algebra.to_complexify_ι`: the effect of complexifying pure vectors. +* `clifford_algebra.of_complexify_tmul_ι`: the effect of un-complexifying a tensor of pure vectors. +* `clifford_algebra.to_complexify_involute`: the effect of complexifying an involution. +* `clifford_algebra.to_complexify_reverse`: the effect of complexifying a reversal. -/ universes uR uA uV @@ -31,7 +41,7 @@ variables [add_comm_group V] [module R V] variables (A) -/-- Change the base of a quadratic form, defined by $Q_A(a ⊗ v) = a^2Q(v)$. -/ +/-- Change the base of a quadratic form, defined by $Q_A(a ⊗_R v) = a^2Q(v)$. -/ def base_change (Q : quadratic_form R V) : quadratic_form A (A ⊗[R] V) := bilin_form.to_quadratic_form $ (bilin_form.tmul' (linear_map.mul A A).to_bilin $ quadratic_form.associated Q) @@ -218,7 +228,7 @@ begin refl, end -/-- The reverse acts only on the right of the tensor product. -/ +/-- `reverse` acts only on the right of the tensor product. -/ lemma to_complexify_reverse (Q : quadratic_form ℝ V) (x : clifford_algebra Q.complexify) : to_complexify Q (reverse x) = tensor_product.map linear_map.id (reverse : _ →ₗ[ℝ] _) (to_complexify Q x) := @@ -264,7 +274,7 @@ end alg_hom.congr_fun (of_complexify_comp_to_complexify Q : _) x /-- Complexifying the vector space of a clifford algebra is isomorphic as a ℂ-algebra to -complexifying the clifford algebra itself; $𝒞ℓ(ℂ ⊗ V, Q_ℂ) \iso ℂ ⊗ 𝒞ℓ(V, Q)$. +complexifying the clifford algebra itself; $Cℓ(ℂ ⊗_ℝ V, Q_ℂ) ≅ ℂ ⊗_ℝ Cℓ(V, Q)$. This is `clifford_algebra.to_complexify` and `clifford_algebra.of_complexify` as an equivalence. -/ @[simps] From 88af79f6292cb43635caf25b7f8b13cffcaf82b8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 4 Aug 2023 11:30:05 +0000 Subject: [PATCH 21/23] missing file --- src/for_mathlib/algebra/algebra/opposite.lean | 92 +++++++++++++++++++ .../tensor_product/opposite.lean | 54 +++++++++++ 2 files changed, 146 insertions(+) create mode 100644 src/for_mathlib/algebra/algebra/opposite.lean create mode 100644 src/for_mathlib/linear_algebra/tensor_product/opposite.lean diff --git a/src/for_mathlib/algebra/algebra/opposite.lean b/src/for_mathlib/algebra/algebra/opposite.lean new file mode 100644 index 000000000..e9e98a884 --- /dev/null +++ b/src/for_mathlib/algebra/algebra/opposite.lean @@ -0,0 +1,92 @@ + +import algebra.algebra.equiv +import algebra.module.opposites +import algebra.ring.opposite + +/-! +# Algebra structures on the multiplicative opposite +-/ + +variables {R S A B : Type _} +variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] +variables [algebra R S] [algebra R A] [algebra R B] [algebra S A] [smul_comm_class R S A] +variables [is_scalar_tower R S A] + +open mul_opposite + +namespace alg_hom + +/-- An algebra homomorphism `f : A →ₐ[R] B` such that `f x` commutes with `f y` for all `x, y` defines +an algebra homomorphism from `Aᵐᵒᵖ`. -/ +@[simps {fully_applied := ff}] +def from_opposite (f : A →ₐ[R] B) (hf : ∀ x y, commute (f x) (f y)) : Aᵐᵒᵖ →ₐ[R] B := +{ to_fun := f ∘ unop, + commutes' := λ r, f.commutes r, + .. f.to_ring_hom.from_opposite hf } + +@[simp] lemma to_linear_map_from_opposite (f : A →ₐ[R] B) (hf : ∀ x y, commute (f x) (f y)) : + (f.from_opposite hf).to_linear_map = f.to_linear_map ∘ₗ (op_linear_equiv R).symm.to_linear_map := +rfl + +@[simp] lemma to_ring_hom_from_opposite (f : A →ₐ[R] B) (hf : ∀ x y, commute (f x) (f y)) : + (f.from_opposite hf).to_ring_hom = f.to_ring_hom.from_opposite hf := +rfl + +/-- An algebra homomorphism `f : A →ₐ[R] B` such that `f x` commutes with `f y` for all `x, y` defines +an algebra homomorphism to `Bᵐᵒᵖ`. -/ +@[simps {fully_applied := ff}] +def to_opposite (f : A →ₐ[R] B) (hf : ∀ x y, commute (f x) (f y)) : A →ₐ[R] Bᵐᵒᵖ := +{ to_fun := op ∘ f, + commutes' := λ r, unop_injective $ f.commutes r, + .. f.to_ring_hom.to_opposite hf } + +@[simp] lemma to_linear_map_to_opposite (f : A →ₐ[R] B) (hf : ∀ x y, commute (f x) (f y)) : + (f.to_opposite hf).to_linear_map = (op_linear_equiv R).to_linear_map ∘ₗ f.to_linear_map := rfl + +@[simp] lemma to_ring_hom_to_opposite (f : A →ₐ[R] B) (hf : ∀ x y, commute (f x) (f y)) : + (f.to_opposite hf).to_ring_hom = f.to_ring_hom.to_opposite hf := +rfl + +/-- An algebra hom `A →ₐ[R] B` can equivalently be viewed as an algebra hom `αᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ`. +This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/ +@[simps] +protected def op : (A →ₐ[R] B) ≃ (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) := +{ to_fun := λ f, + { commutes' := λ r, unop_injective $ f.commutes r, + ..f.to_ring_hom.op }, + inv_fun := λ f, + { commutes' := λ r, op_injective $ f.commutes r, + ..f.to_ring_hom.unop}, + left_inv := λ f, alg_hom.ext $ λ a, rfl, + right_inv := λ f, alg_hom.ext $ λ a, rfl } + +/-- The 'unopposite' of an algebra hom `αᵐᵒᵖ →+* Bᵐᵒᵖ`. Inverse to `ring_hom.op`. -/ +@[simp] +protected def unop : (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B) := alg_hom.op.symm + +end alg_hom + +/-- An algebra iso `A ≃ₐ[R] B` can equivalently be viewed as an algebra iso `αᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. +This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/ +@[simps] +def alg_equiv.op : (A ≃ₐ[R] B) ≃ (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) := +{ to_fun := λ f, + { commutes' := λ r, mul_opposite.unop_injective $ f.commutes r, + ..f.to_ring_equiv.op }, + inv_fun := λ f, + { commutes' := λ r, mul_opposite.op_injective $ f.commutes r, + ..f.to_ring_equiv.unop}, + left_inv := λ f, alg_equiv.ext $ λ a, rfl, + right_inv := λ f, alg_equiv.ext $ λ a, rfl } + +/-- The double opposite is isomorphic as an algebra to the original type. -/ +@[simps] +def mul_opposite.op_op_alg_equiv : Aᵐᵒᵖᵐᵒᵖ ≃ₐ[R] A := +alg_equiv.of_linear_equiv + ((mul_opposite.op_linear_equiv _).trans (mul_opposite.op_linear_equiv _)).symm + (λ x y, rfl) + (λ r, rfl) + +@[simps] +def alg_hom.op_comm : (A →ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ →ₐ[R] B) := +(mul_opposite.op_op_alg_equiv.symm.arrow_congr alg_equiv.refl).trans alg_hom.op.symm diff --git a/src/for_mathlib/linear_algebra/tensor_product/opposite.lean b/src/for_mathlib/linear_algebra/tensor_product/opposite.lean new file mode 100644 index 000000000..26b4c09a0 --- /dev/null +++ b/src/for_mathlib/linear_algebra/tensor_product/opposite.lean @@ -0,0 +1,54 @@ +import for_mathlib.ring_theory.tensor_product +import for_mathlib.algebra.algebra.opposite + +/-! # `MulOpposite` commutes with `⊗` + +The main result in this file is: + +* `algebra.tensor_product.op_alg_equiv : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ` +-/ + +variables {R S A B : Type _} +variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] +variables [algebra R S] [algebra R A] [algebra R B] [algebra S A] [smul_comm_class R S A] +variables [is_scalar_tower R S A] + +namespace algebra.tensor_product +open_locale tensor_product + +open mul_opposite + +variables (S) + +/-- `MulOpposite` commutes with `TensorProduct`. -/ +def op_alg_equiv : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ := +alg_equiv.of_alg_hom + (alg_hom_of_linear_map_tensor_product' + (tensor_product.algebra_tensor_module.congr + (op_linear_equiv S).symm + (op_linear_equiv R).symm + ≪≫ₗ op_linear_equiv S).to_linear_map + (λ a₁ a₂ b₁ b₂, unop_injective rfl) + (λ r, unop_injective $ rfl)) + (alg_hom.op_comm $ alg_hom_of_linear_map_tensor_product' + (show A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ, from + tensor_product.algebra_tensor_module.congr + (op_linear_equiv S) + (op_linear_equiv R) ≪≫ₗ op_linear_equiv S).to_linear_map + (λ a₁ a₂ b₁ b₂, unop_injective $ rfl) + (λ r, unop_injective $ rfl)) + (alg_hom.op.symm.injective $ by ext; refl) + (by ext; refl) + +lemma op_alg_equiv_apply (x : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) : + op_alg_equiv S x = + op (tensor_product.map + (op_linear_equiv R).symm.to_linear_map (op_linear_equiv R).symm.to_linear_map x) := rfl + +@[simp] lemma op_alg_equiv_tmul (a : Aᵐᵒᵖ) (b : Bᵐᵒᵖ) : + op_alg_equiv S (a ⊗ₜ[R] b) = op (a.unop ⊗ₜ b.unop) := rfl + +@[simp] lemma op_alg_equiv_symm_tmul (a : A) (b : B) : + (op_alg_equiv S).symm (op $ a ⊗ₜ[R] b) = op a ⊗ₜ op b := rfl + +end algebra.tensor_product From 55110dd53ae81a737489ebf1cc5a3f41f18135e0 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 4 Aug 2023 11:31:53 +0000 Subject: [PATCH 22/23] tweak --- src/for_mathlib/algebra/algebra/opposite.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/for_mathlib/algebra/algebra/opposite.lean b/src/for_mathlib/algebra/algebra/opposite.lean index e9e98a884..53c3086ba 100644 --- a/src/for_mathlib/algebra/algebra/opposite.lean +++ b/src/for_mathlib/algebra/algebra/opposite.lean @@ -66,6 +66,8 @@ protected def unop : (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B) := al end alg_hom +namespace alg_equiv + /-- An algebra iso `A ≃ₐ[R] B` can equivalently be viewed as an algebra iso `αᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/ @[simps] @@ -79,6 +81,12 @@ def alg_equiv.op : (A ≃ₐ[R] B) ≃ (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) := left_inv := λ f, alg_equiv.ext $ λ a, rfl, right_inv := λ f, alg_equiv.ext $ λ a, rfl } +/-- The 'unopposite' of an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. Inverse to `alg_equiv.op`. -/ +@[simp] +protected def unop : (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) ≃ (A ≃ₐ[R] B) := alg_equiv.op.symm + +end alg_equiv + /-- The double opposite is isomorphic as an algebra to the original type. -/ @[simps] def mul_opposite.op_op_alg_equiv : Aᵐᵒᵖᵐᵒᵖ ≃ₐ[R] A := From a7708f1a8aa4a58fd313ea52a101cb92e97d227f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 25 Oct 2023 16:11:17 +0100 Subject: [PATCH 23/23] Add mathlib link --- src/geometric_algebra/from_mathlib/complexification.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean index d587bd39e..b827f8692 100644 --- a/src/geometric_algebra/from_mathlib/complexification.lean +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -27,6 +27,9 @@ We show: * `clifford_algebra.of_complexify_tmul_ι`: the effect of un-complexifying a tensor of pure vectors. * `clifford_algebra.to_complexify_involute`: the effect of complexifying an involution. * `clifford_algebra.to_complexify_reverse`: the effect of complexifying a reversal. + +Note that all the results in this file are already in Mathlib4 due to +https://github.com/leanprover-community/mathlib4/pull/6778. -/ universes uR uA uV