From 60ccf8f7474e5d46505efa8534bd98eb3a243b1c Mon Sep 17 00:00:00 2001 From: mcdoll Date: Sun, 10 Apr 2022 20:28:46 +0000 Subject: [PATCH] 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 | 20 ++- src/linear_algebra/bilinear_form.lean | 4 +- src/linear_algebra/bilinear_map.lean | 30 +++- src/linear_algebra/sesquilinear_form.lean | 157 ++++++++++++++++++ 4 files changed, 197 insertions(+), 14 deletions(-) diff --git a/src/analysis/inner_product_space/adjoint.lean b/src/analysis/inner_product_space/adjoint.lean index 630d4ca19f4b6..8660c23653d90 100644 --- a/src/analysis/inner_product_space/adjoint.lean +++ b/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 diff --git a/src/linear_algebra/bilinear_form.lean b/src/linear_algebra/bilinear_form.lean index f8a208107bc4f..153cdf854b69e 100644 --- a/src/linear_algebra/bilinear_form.lean +++ b/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 diff --git a/src/linear_algebra/bilinear_map.lean b/src/linear_algebra/bilinear_map.lean index 9becda7004fad..de7cccddacdca 100644 --- a/src/linear_algebra/bilinear_map.lean +++ b/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ₗ := diff --git a/src/linear_algebra/sesquilinear_form.lean b/src/linear_algebra/sesquilinear_form.lean index 3f2fe1e5787ad..2c505cca3a049 100644 --- a/src/linear_algebra/sesquilinear_form.lean +++ b/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