diff --git a/src/for_mathlib/algebra/algebra/opposite.lean b/src/for_mathlib/algebra/algebra/opposite.lean new file mode 100644 index 000000000..53c3086ba --- /dev/null +++ b/src/for_mathlib/algebra/algebra/opposite.lean @@ -0,0 +1,100 @@ + +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 + +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] +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 '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 := +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/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/linear_algebra/bilinear_form/basic.lean b/src/for_mathlib/linear_algebra/bilinear_form/basic.lean new file mode 100644 index 000000000..67da16651 --- /dev/null +++ b/src/for_mathlib/linear_algebra/bilinear_form/basic.lean @@ -0,0 +1,28 @@ +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] + +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 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 361c111e4..652a4d98a 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,48 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ import linear_algebra.bilinear_form.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 : 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 A] +variables [add_comm_monoid M₁] [add_comm_monoid 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₂] + +/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/ +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 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₂) + (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₂') := +rfl + +/-- 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₂) + +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/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 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..ff0f7e227 --- /dev/null +++ b/src/for_mathlib/ring_theory/tensor_product.lean @@ -0,0 +1,303 @@ +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 +open tensor_product + +namespace tensor_product + +variables {R A B C M N P Q P' Q' : Type*} + +/-! +### The `A`-module structure on `A ⊗[R] M` +-/ + +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] +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 := +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 + +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, + 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 _ _ _, } + +/-- 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]) + (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) + +/- 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.flip.restrict_scalars R ∘ₗ algebra.linear_map R A) + ((mk R A A R).flip 1) + (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 + +/-- 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₃) + +/- 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 + +@[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 + refine _ ∘ₗ hom_tensor_hom_map R A M N A R, + 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) + +/-- 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] } + +/-- 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 } + +/-- 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 _ _ _ _) + (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)) + +/-- 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 $ 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) _ _, + { 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`. -/ +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 + +end comm_semiring + +end algebra_tensor_module + +end tensor_product + +namespace algebra.tensor_product +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] [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] + +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) + (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]) + +@[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 := +{ 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') + (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/basic.lean b/src/geometric_algebra/from_mathlib/basic.lean index 1fe51804f..a94a4c65a 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,15 +18,38 @@ 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) } -instance {A : Type*} [ring A] [algebra R A] : +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 + +instance [ring A] [algebra R A] : has_zero (clifford_hom (0 : quadratic_form R M) A) := { zero := ⟨0, λ m, by simp⟩ } -instance has_zero_of_subsingleton {A : Type*} [ring A] [algebra R A] [subsingleton A] : +instance has_zero_of_subsingleton [ring A] [algebra R A] [subsingleton A] : has_zero (clifford_hom Q A) := { zero := ⟨0, λ m, subsingleton.elim _ _⟩ } diff --git a/src/geometric_algebra/from_mathlib/complexification.lean b/src/geometric_algebra/from_mathlib/complexification.lean new file mode 100644 index 000000000..b827f8692 --- /dev/null +++ b/src/geometric_algebra/from_mathlib/complexification.lean @@ -0,0 +1,290 @@ +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 + +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)`, 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. + +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 +variables {R : Type uR} {A : Type uA} {V : Type uV} + +open_locale tensor_product + +namespace quadratic_form + +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 ⊗_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) + +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 + +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.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 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 + +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 + +namespace clifford_algebra +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) : + clifford_algebra Q →ₐ[ℝ] clifford_algebra Q.complexify := +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 [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) : + 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' + (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) + (λ 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 ⊗ₜ ι Q v) = ι _ (z ⊗ₜ v) := +begin + 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 + +@[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 + +/-- 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 + let φ := tensor_product.algebra_tensor_module.map (linear_map.id : ℂ →ₗ[ℂ] ℂ) (ι Q), + refine ⟨φ, _⟩, + 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.base_change_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 (ι _ (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 + +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 + +/-- `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) : + (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 ⊗ₜ[ℝ] ι Q v)) + = 1 ⊗ₜ[ℝ] ι 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 (ι Q.complexify (1 ⊗ₜ[ℝ] x))) + = ι 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 + +/-- Complexifying the vector space of a clifford algebra is isomorphic as a ℂ-algebra to +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] +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) + +end clifford_algebra 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