feat(linear_algebra): add adjoint_pair from bilinear_form (#13203)

Copying the definition and theorem about adjoint pairs from `bilinear_form` to `sesquilinear_form`.
Defines the composition of two linear maps with a bilinear map to form a new bilinear map, which was missing from the `bilinear_map` API.

We also use the new definition of adjoint pairs in `analysis/inner_product_space/adjoint`.

src/analysis/inner_product_space/adjoint.lean

@@ -178,11 +178,12 @@ section real
 variables {E' : Type*} {F' : Type*} [inner_product_space ℝ E'] [inner_product_space ℝ F']
 variables [complete_space E'] [complete_space F']
 
-lemma is_adjoint_pair (A : E' →L[ℝ] F') :
-  bilin_form.is_adjoint_pair (bilin_form_of_real_inner : bilin_form ℝ E')
-  (bilin_form_of_real_inner : bilin_form ℝ F') A (A†) :=
-λ x y, by simp only [adjoint_inner_right, to_linear_map_eq_coe,
-                     bilin_form_of_real_inner_apply, coe_coe]
+-- Todo: Generalize this to `is_R_or_C`.
+lemma is_adjoint_pair_inner (A : E' →L[ℝ] F') :
+  linear_map.is_adjoint_pair (sesq_form_of_inner : E' →ₗ[ℝ] E' →ₗ[ℝ] ℝ)
+  (sesq_form_of_inner : F' →ₗ[ℝ] F' →ₗ[ℝ] ℝ) A (A†) :=
+λ x y, by simp only [sesq_form_of_inner_apply_apply, adjoint_inner_left, to_linear_map_eq_coe,
+  coe_coe]
 
 end real
 
@@ -291,10 +292,11 @@ section real
 variables {E' : Type*} {F' : Type*} [inner_product_space ℝ E'] [inner_product_space ℝ F']
 variables [finite_dimensional ℝ E'] [finite_dimensional ℝ F']
 
-lemma is_adjoint_pair (A : E' →ₗ[ℝ] F') :
-  bilin_form.is_adjoint_pair (bilin_form_of_real_inner : bilin_form ℝ E')
-  (bilin_form_of_real_inner : bilin_form ℝ F') A A.adjoint :=
-λ x y, by simp only [adjoint_inner_right, bilin_form_of_real_inner_apply]
+-- Todo: Generalize this to `is_R_or_C`.
+lemma is_adjoint_pair_inner (A : E' →ₗ[ℝ] F') :
+  is_adjoint_pair (sesq_form_of_inner : E' →ₗ[ℝ] E' →ₗ[ℝ] ℝ)
+  (sesq_form_of_inner : F' →ₗ[ℝ] F' →ₗ[ℝ] ℝ) A A.adjoint :=
+λ x y, by simp only [sesq_form_of_inner_apply_apply, adjoint_inner_left]
 
 end real
 

src/linear_algebra/bilinear_form.lean

@@ -444,7 +444,7 @@ by { ext, refl }
   B.comp linear_map.id linear_map.id = B :=
 by { ext, refl }
 
-lemma comp_injective (B₁ B₂ : bilin_form R M') {l r : M →ₗ[R] M'}
+lemma comp_inj (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
@@ -795,7 +795,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 _ _ he he],
+      hᵣ, hₗ, comp_inj _ _ 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/bilinear_map.lean

@@ -168,12 +168,13 @@ section comm_semiring
 variables {R : Type*} [comm_semiring R] {R₂ : Type*} [comm_semiring R₂]
 variables {R₃ : Type*} [comm_semiring R₃] {R₄ : Type*} [comm_semiring R₄]
 variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*}
-variables {Nₗ : Type*} {Pₗ : Type*} {Qₗ : Type*}
+variables {Mₗ : Type*} {Nₗ : Type*} {Pₗ : Type*} {Qₗ Qₗ': Type*}
 
 variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q]
-variables [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [add_comm_monoid Qₗ]
+variables [add_comm_monoid Mₗ] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ]
+variables [add_comm_monoid Qₗ] [add_comm_monoid Qₗ']
 variables [module R M] [module R₂ N] [module R₃ P] [module R₄ Q]
-variables [module R Nₗ] [module R Pₗ] [module R Qₗ]
+variables [module R Mₗ] [module R Nₗ] [module R Pₗ] [module R Qₗ] [module R Qₗ']
 variables {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃}
 variables {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃}
 variables [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₄₂ σ₂₃ σ₄₃]
@@ -249,6 +250,29 @@ include σ₄₃
   f.compl₂ g m q = f m (g q) := rfl
 omit σ₄₃
 
+/-- Composing linear maps `Q → M` and `Q' → N` with a bilinear map `M → N → P` to
+form a bilinear map `Q → Q' → P`. -/
+def compl₁₂ (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ) :
+  Qₗ →ₗ[R] Qₗ' →ₗ[R] Pₗ :=
+(f.comp g).compl₂ g'
+
+@[simp] theorem compl₁₂_apply (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ)
+  (x : Qₗ) (y : Qₗ') : f.compl₁₂ g g' x y = f (g x) (g' y) := rfl
+
+lemma compl₁₂_inj {f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {g : Qₗ →ₗ[R] Mₗ} {g' : Qₗ' →ₗ[R] Nₗ}
+  (hₗ : function.surjective g) (hᵣ : function.surjective g') :
+  f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂ :=
+begin
+  split; intros h,
+  { -- B₁.comp l r = B₂.comp l r → B₁ = B₂
+    ext x y,
+    cases hₗ x with x' hx, subst hx,
+    cases hᵣ y with y' hy, subst hy,
+    convert linear_map.congr_fun₂ h x' y' },
+  { -- B₁ = B₂ → B₁.comp l r = B₂.comp l r
+    subst h },
+end
+
 /-- Composing a linear map `P → Q` and a bilinear map `M → N → P` to
 form a bilinear map `M → N → Q`. -/
 def compr₂ (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) : M →ₗ[R] Nₗ →ₗ[R] Qₗ :=

src/linear_algebra/sesquilinear_form.lean

@@ -378,6 +378,163 @@ lemma is_compl_span_singleton_orthogonal {B : V →ₗ[K] V →ₗ[K] K}
 
 end orthogonal
 
+/-! ### Adjoint pairs -/
+
+section adjoint_pair
+
+section add_comm_monoid
+
+variables [comm_semiring R]
+variables [add_comm_monoid M] [module R M]
+variables [add_comm_monoid M₁] [module R M₁]
+variables [add_comm_monoid M₂] [module R M₂]
+variables {B F : M →ₗ[R] M →ₗ[R] R} {B' : M₁ →ₗ[R] M₁ →ₗ[R] R} {B'' : M₂ →ₗ[R] M₂ →ₗ[R] R}
+variables {f f' : M →ₗ[R] M₁} {g g' : M₁ →ₗ[R] M}
+
+variables (B B' f g)
+
+/-- Given a pair of modules equipped with bilinear forms, this is the condition for a pair of
+maps between them to be mutually adjoint. -/
+def is_adjoint_pair := ∀ x y, B' (f x) y = B x (g y)
+
+variables {B B' f g}
+
+lemma is_adjoint_pair_iff_comp_eq_compl₂ :
+  is_adjoint_pair B B' f g ↔ B'.comp f = B.compl₂ g :=
+begin
+  split; intros h,
+  { ext x y, rw [comp_apply, compl₂_apply], exact h x y },
+  { intros _ _, rw [←compl₂_apply, ←comp_apply, h] },
+end
+
+lemma is_adjoint_pair_zero : is_adjoint_pair B B' 0 0 :=
+λ _ _, by simp only [zero_apply, map_zero]
+
+lemma is_adjoint_pair_id : is_adjoint_pair B B 1 1 := λ x y, rfl
+
+lemma is_adjoint_pair.add (h : is_adjoint_pair B B' f g) (h' : is_adjoint_pair B B' f' g') :
+  is_adjoint_pair B B' (f + f') (g + g') :=
+λ x _, by rw [f.add_apply, g.add_apply, B'.map_add₂, (B x).map_add, h, h']
+
+lemma is_adjoint_pair.comp {f' : M₁ →ₗ[R] M₂} {g' : M₂ →ₗ[R] M₁}
+  (h : is_adjoint_pair B B' f g) (h' : is_adjoint_pair B' B'' f' g') :
+  is_adjoint_pair B B'' (f'.comp f) (g.comp g') :=
+λ _ _, by rw [linear_map.comp_apply, linear_map.comp_apply, h', h]
+
+lemma is_adjoint_pair.mul
+  {f g f' g' : module.End R M} (h : is_adjoint_pair B B f g) (h' : is_adjoint_pair B B f' g') :
+  is_adjoint_pair B B (f * f') (g' * g) :=
+h'.comp h
+
+end add_comm_monoid
+
+section add_comm_group
+
+variables [comm_ring R]
+variables [add_comm_group M] [module R M]
+variables [add_comm_group M₁] [module R M₁]
+variables {B F : M →ₗ[R] M →ₗ[R] R} {B' : M₁ →ₗ[R] M₁ →ₗ[R] R}
+variables {f f' : M →ₗ[R] M₁} {g g' : M₁ →ₗ[R] M}
+
+lemma is_adjoint_pair.sub (h : is_adjoint_pair B B' f g) (h' : is_adjoint_pair B B' f' g') :
+  is_adjoint_pair B B' (f - f') (g - g') :=
+λ x _, by rw [f.sub_apply, g.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
+
+lemma is_adjoint_pair.smul (c : R) (h : is_adjoint_pair B B' f g) :
+  is_adjoint_pair B B' (c • f) (c • g) :=
+λ _ _, by simp only [smul_apply, map_smul, smul_eq_mul, h _ _]
+
+end add_comm_group
+
+end adjoint_pair
+
+/-! ### Self-adjoint pairs-/
+
+section selfadjoint_pair
+
+section add_comm_monoid
+
+variables [comm_semiring R]
+variables [add_comm_monoid M] [module R M]
+variables (B F : M →ₗ[R] M →ₗ[R] R)
+
+/-- The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms
+on the underlying module. In the case that these two forms are identical, this is the usual concept
+of self adjointness. In the case that one of the forms is the negation of the other, this is the
+usual concept of skew adjointness. -/
+def is_pair_self_adjoint (f : module.End R M) := is_adjoint_pair B F f f
+
+/-- An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an
+adjoint for itself. -/
+protected def is_self_adjoint (f : module.End R M) := is_adjoint_pair B B f f
+
+end add_comm_monoid
+
+section add_comm_group
+
+variables [comm_ring R]
+variables [add_comm_group M] [module R M]
+variables [add_comm_group M₁] [module R M₁]
+(B F : M →ₗ[R] M →ₗ[R] R)
+
+/-- The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms. -/
+def is_pair_self_adjoint_submodule : submodule R (module.End R M) :=
+{ carrier   := { f | is_pair_self_adjoint B F f },
+  zero_mem' := is_adjoint_pair_zero,
+  add_mem'  := λ f g hf hg, hf.add hg,
+  smul_mem' := λ c f h, h.smul c, }
+
+/-- An endomorphism of a module is skew-adjoint with respect to a bilinear form if its negation
+serves as an adjoint. -/
+def is_skew_adjoint (f : module.End R M) := is_adjoint_pair B B f (-f)
+
+/-- The set of self-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact
+it is a Jordan subalgebra.) -/
+def self_adjoint_submodule := is_pair_self_adjoint_submodule B B
+
+/-- The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact
+it is a Lie subalgebra.) -/
+def skew_adjoint_submodule := is_pair_self_adjoint_submodule (-B) B
+
+variables {B F}
+
+@[simp] lemma mem_is_pair_self_adjoint_submodule (f : module.End R M) :
+  f ∈ is_pair_self_adjoint_submodule B F ↔ is_pair_self_adjoint B F f :=
+iff.rfl
+
+lemma is_pair_self_adjoint_equiv (e : M₁ ≃ₗ[R] M) (f : module.End R M) :
+  is_pair_self_adjoint B F f ↔
+    is_pair_self_adjoint (B.compl₁₂ ↑e ↑e) (F.compl₁₂ ↑e ↑e) (e.symm.conj f) :=
+begin
+  have hₗ : (F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).comp (e.symm.conj f) =
+    (F.comp f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) :=
+  by { ext, simp only [linear_equiv.symm_conj_apply, coe_comp, linear_equiv.coe_coe, compl₁₂_apply,
+    linear_equiv.apply_symm_apply], },
+  have hᵣ : (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (e.symm.conj f) =
+    (B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) :=
+  by { ext, simp only [linear_equiv.symm_conj_apply, compl₂_apply, coe_comp, linear_equiv.coe_coe,
+      compl₁₂_apply, linear_equiv.apply_symm_apply] },
+  have he : function.surjective (⇑(↑e : M₁ →ₗ[R] M) : M₁ → M) := e.surjective,
+  simp_rw [is_pair_self_adjoint, is_adjoint_pair_iff_comp_eq_compl₂, hₗ, hᵣ,
+    compl₁₂_inj he he],
+end
+
+lemma is_skew_adjoint_iff_neg_self_adjoint (f : module.End R M) :
+  B.is_skew_adjoint f ↔ is_adjoint_pair (-B) B f f :=
+show (∀ x y, B (f x) y = B x ((-f) y)) ↔ ∀ x y, B (f x) y = (-B) x (f y),
+by simp
+
+@[simp] lemma mem_self_adjoint_submodule (f : module.End R M) :
+  f ∈ B.self_adjoint_submodule ↔ B.is_self_adjoint f := iff.rfl
+
+@[simp] lemma mem_skew_adjoint_submodule (f : module.End R M) :
+  f ∈ B.skew_adjoint_submodule ↔ B.is_skew_adjoint f :=
+by { rw is_skew_adjoint_iff_neg_self_adjoint, exact iff.rfl }
+
+end add_comm_group
+
+end selfadjoint_pair
+
 /-! ### Nondegenerate bilinear forms -/
 
 section nondegenerate