Base change (and complexification) of quadratic forms

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

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' : _)⟩

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

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₂]

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

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