feat(linear_algebra/sesquilinear_form): add composition between sesqu…

…ilinear forms and linear maps (#5729)

Add composition lemmas for sesquilinear forms, that is, given a sesquilinear form and linear maps, a new sesquilinear form is induced by applying the arguments with the linear map.

src/linear_algebra/bilinear_form.lean

@@ -270,7 +270,7 @@ lemma comp_comp {M'' : Type*} [add_comm_monoid M''] [semimodule R M'']
 @[simp] lemma comp_right_apply (B : bilin_form R M) (f : M →ₗ[R] M) (v w) :
   B.comp_right f v w = B v (f w) := rfl
 
-lemma comp_injective (B₁ B₂ : bilin_form R M') (l r : M →ₗ[R] M')
+lemma comp_injective (B₁ B₂ : bilin_form R M') {l r : M →ₗ[R] M'}
   (hₗ : function.surjective l) (hᵣ : function.surjective r) :
   B₁.comp l r = B₂.comp l r ↔ B₁ = B₂ :=
 begin
@@ -863,7 +863,7 @@ begin
   have he : function.surjective (⇑(↑e : M₃' →ₗ[R₃] M₃) : M₃' → M₃) := e.surjective,
   show bilin_form.is_adjoint_pair _ _ _ _  ↔ bilin_form.is_adjoint_pair _ _ _ _,
   rw [is_adjoint_pair_iff_comp_left_eq_comp_right, is_adjoint_pair_iff_comp_left_eq_comp_right,
-      hᵣ, hₗ, comp_injective _ _ ↑e ↑e he he],
+      hᵣ, hₗ, comp_injective _ _ he he],
 end
 
 /-- An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an

src/linear_algebra/sesquilinear_form.lean

@@ -3,8 +3,8 @@ Copyright (c) 2018 Andreas Swerdlow. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Andreas Swerdlow
 -/
-import algebra.module.basic
 import ring_theory.ring_invo
+import algebra.module.linear_map
 
 /-!
 # Sesquilinear form
@@ -33,7 +33,7 @@ Sesquilinear form,
 
 open_locale big_operators
 
-universes u v
+universes u v w
 
 /-- A sesquilinear form over a module  -/
 structure sesq_form (R : Type u) (M : Type v) [ring R] (I : R ≃+* Rᵒᵖ)
@@ -133,6 +133,57 @@ lemma map_sum_right {α : Type*} (S : sesq_form R M I) (t : finset α) (g : α 
   S w (∑ i in t, g i) = ∑ i in t, S w (g i) :=
 by haveI s_inst := is_add_monoid_hom_right S w; exact (finset.sum_hom t (λ z, S w z)).symm
 
+variables {M₂ : Type w} [add_comm_group M₂] [module R M₂]
+
+/-- Apply the linear maps `f` and `g` to the left and right arguments of the sesquilinear form. -/
+def comp (S : sesq_form R M I) (f g : M₂ →ₗ[R] M) : sesq_form R M₂ I :=
+{ sesq := λ x y, S (f x) (g y),
+  sesq_add_left := by simp [add_left],
+  sesq_smul_left := by simp [smul_left],
+  sesq_add_right := by simp [add_right],
+  sesq_smul_right := by simp [smul_right] }
+
+/-- Apply the linear map `f` to the left argument of the sesquilinear form. -/
+def comp_left (S : sesq_form R M I) (f : M →ₗ[R] M) : sesq_form R M I :=
+  S.comp f linear_map.id
+
+/-- Apply the linear map `f` to the right argument of the sesquilinear form. -/
+def comp_right (S : sesq_form R M I) (f : M →ₗ[R] M) : sesq_form R M I :=
+  S.comp linear_map.id f
+
+lemma comp_left_comp_right (S : sesq_form R M I) (f g : M →ₗ[R] M) :
+  (S.comp_left f).comp_right g = S.comp f g := rfl
+
+lemma comp_right_comp_left (S : sesq_form R M I) (f g : M →ₗ[R] M) :
+  (S.comp_right g).comp_left f = S.comp f g := rfl
+
+lemma comp_comp {M₃ : Type*} [add_comm_group M₃] [module R M₃]
+  (S : sesq_form R M₃ I) (l r : M →ₗ[R] M₂) (l' r' : M₂ →ₗ[R] M₃) :
+  (S.comp l' r').comp l r = S.comp (l'.comp l) (r'.comp r) := rfl
+
+@[simp] lemma comp_apply (S : sesq_form R M₂ I) (l r : M →ₗ[R] M₂) (v w : M) :
+  S.comp l r v w = S (l v) (r w) := rfl
+
+@[simp] lemma comp_left_apply (S : sesq_form R M I) (f : M →ₗ[R] M) (v w : M) :
+  S.comp_left f v w = S (f v) w := rfl
+
+@[simp] lemma comp_right_apply (S : sesq_form R M I) (f : M →ₗ[R] M) (v w : M) :
+  S.comp_right f v w = S v (f w) := rfl
+
+/-- Let `l`, `r` be surjective linear maps, then two sesquilinear forms are equal if and only if
+  the sesquilinear forms resulting from composition with `l` and `r` are equal. -/
+lemma comp_injective (S₁ S₂ : sesq_form R M₂ I) {l r : M →ₗ[R] M₂}
+  (hl : function.surjective l) (hr : function.surjective r) :
+  S₁.comp l r = S₂.comp l r ↔ S₁ = S₂ :=
+begin
+  split; intros h,
+  { ext,
+    rcases hl x with ⟨x', rfl⟩,
+    rcases hr y with ⟨y', rfl⟩,
+    rw [← comp_apply, ← comp_apply, h], },
+  { rw h },
+end
+
 end general_ring
 
 section comm_ring