diff --git a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean index 3b511c2156a5d4..ed91c525b15846 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Andreas Swerdlow, Kexing Ying -/ import Mathlib.Algebra.Algebra.Tower +import Mathlib.LinearAlgebra.BilinearMap #align_import linear_algebra.bilinear_form from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9" @@ -43,19 +44,13 @@ In this file we use the following type variables: Bilinear form, -/ +export LinearMap (BilinForm) open BigOperators -universe u v w +open LinearMap (BilinForm) -/-- `BilinForm R M` is the type of `R`-bilinear functions `M → M → R`. -/ -structure BilinForm (R : Type*) (M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] where - bilin : M → M → R - bilin_add_left : ∀ x y z : M, bilin (x + y) z = bilin x z + bilin y z - bilin_smul_left : ∀ (a : R) (x y : M), bilin (a • x) y = a * bilin x y - bilin_add_right : ∀ x y z : M, bilin x (y + z) = bilin x y + bilin x z - bilin_smul_right : ∀ (a : R) (x y : M), bilin x (a • y) = a * bilin x y -#align bilin_form BilinForm +universe u v w variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] variable {S : Type*} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] @@ -63,306 +58,225 @@ variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Modu variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V] variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} -namespace BilinForm - -instance : CoeFun (BilinForm R M) fun _ => M → M → R := - ⟨bilin⟩ +namespace LinearMap -initialize_simps_projections BilinForm (bilin → apply) +namespace BilinForm --- Porting note: removed for simpVarHead @[simp] -theorem coeFn_mk (f : M → M → R) (h₁ h₂ h₃ h₄) : (BilinForm.mk f h₁ h₂ h₃ h₄ : M → M → R) = f := - rfl -#align bilin_form.coe_fn_mk BilinForm.coeFn_mk +#noalign bilin_form.coe_fn_mk theorem coeFn_congr : ∀ {x x' y y' : M}, x = x' → y = y' → B x y = B x' y' | _, _, _, _, rfl, rfl => rfl -#align bilin_form.coe_fn_congr BilinForm.coeFn_congr +#align bilin_form.coe_fn_congr LinearMap.BilinForm.coeFn_congr -@[simp] -theorem add_left (x y z : M) : B (x + y) z = B x z + B y z := - bilin_add_left B x y z -#align bilin_form.add_left BilinForm.add_left +theorem add_left (x y z : M) : B (x + y) z = B x z + B y z := by + simp only [map_add, LinearMap.add_apply] +#align bilin_form.add_left LinearMap.BilinForm.add_left -@[simp] -theorem smul_left (a : R) (x y : M) : B (a • x) y = a * B x y := - bilin_smul_left B a x y -#align bilin_form.smul_left BilinForm.smul_left +theorem smul_left (a : R) (x y : M) : B (a • x) y = a * B x y := by + simp only [map_smul, LinearMap.smul_apply, smul_eq_mul] +#align bilin_form.smul_left LinearMap.BilinForm.smul_left -@[simp] -theorem add_right (x y z : M) : B x (y + z) = B x y + B x z := - bilin_add_right B x y z -#align bilin_form.add_right BilinForm.add_right +theorem add_right (x y z : M) : B x (y + z) = B x y + B x z := map_add _ _ _ +#align bilin_form.add_right LinearMap.BilinForm.add_right -@[simp] -theorem smul_right (a : R) (x y : M) : B x (a • y) = a * B x y := - bilin_smul_right B a x y -#align bilin_form.smul_right BilinForm.smul_right +theorem smul_right (a : R) (x y : M) : B x (a • y) = a * B x y := map_smul _ _ _ +#align bilin_form.smul_right LinearMap.BilinForm.smul_right -@[simp] theorem zero_left (x : M) : B 0 x = 0 := by rw [← @zero_smul R _ _ _ _ (0 : M), smul_left, zero_mul] -#align bilin_form.zero_left BilinForm.zero_left +#align bilin_form.zero_left LinearMap.BilinForm.zero_left -@[simp] theorem zero_right (x : M) : B x 0 = 0 := by rw [← @zero_smul R _ _ _ _ (0 : M), smul_right, zero_mul] -#align bilin_form.zero_right BilinForm.zero_right +#align bilin_form.zero_right LinearMap.BilinForm.zero_right -@[simp] theorem neg_left (x y : M₁) : B₁ (-x) y = -B₁ x y := by rw [← @neg_one_smul R₁ _ _, smul_left, neg_one_mul] -#align bilin_form.neg_left BilinForm.neg_left +#align bilin_form.neg_left LinearMap.BilinForm.neg_left -@[simp] theorem neg_right (x y : M₁) : B₁ x (-y) = -B₁ x y := by rw [← @neg_one_smul R₁ _ _, smul_right, neg_one_mul] -#align bilin_form.neg_right BilinForm.neg_right +#align bilin_form.neg_right LinearMap.BilinForm.neg_right -@[simp] theorem sub_left (x y z : M₁) : B₁ (x - y) z = B₁ x z - B₁ y z := by rw [sub_eq_add_neg, sub_eq_add_neg, add_left, neg_left] -#align bilin_form.sub_left BilinForm.sub_left +#align bilin_form.sub_left LinearMap.BilinForm.sub_left -@[simp] theorem sub_right (x y z : M₁) : B₁ x (y - z) = B₁ x y - B₁ x z := by rw [sub_eq_add_neg, sub_eq_add_neg, add_right, neg_right] -#align bilin_form.sub_right BilinForm.sub_right +#align bilin_form.sub_right LinearMap.BilinForm.sub_right -@[simp] lemma smul_left_of_tower (r : S) (x y : M) : B (r • x) y = r • B x y := by rw [← IsScalarTower.algebraMap_smul R r, smul_left, Algebra.smul_def] -@[simp] lemma smul_right_of_tower (r : S) (x y : M) : B x (r • y) = r • B x y := by rw [← IsScalarTower.algebraMap_smul R r, smul_right, Algebra.smul_def] variable {D : BilinForm R M} {D₁ : BilinForm R₁ M₁} -- TODO: instantiate `FunLike` -theorem coe_injective : Function.Injective ((↑) : BilinForm R M → M → M → R) := fun B D h => by - cases B - cases D - congr -#align bilin_form.coe_injective BilinForm.coe_injective +theorem coe_injective : Function.Injective ((fun B x y => B x y) : BilinForm R M → M → M → R) := + fun B D h => by + ext x y + apply congrFun₂ h +#align bilin_form.coe_injective LinearMap.BilinForm.coe_injective @[ext] theorem ext (H : ∀ x y : M, B x y = D x y) : B = D := coe_injective <| by funext exact H _ _ -#align bilin_form.ext BilinForm.ext +#align bilin_form.ext LinearMap.BilinForm.ext theorem congr_fun (h : B = D) (x y : M) : B x y = D x y := h ▸ rfl -#align bilin_form.congr_fun BilinForm.congr_fun +#align bilin_form.congr_fun LinearMap.BilinForm.congr_fun theorem ext_iff : B = D ↔ ∀ x y, B x y = D x y := - ⟨congr_fun, ext⟩ -#align bilin_form.ext_iff BilinForm.ext_iff + ⟨congr_fun, ext₂⟩ +#align bilin_form.ext_iff LinearMap.BilinForm.ext_iff -instance : Zero (BilinForm R M) where - zero := - { bilin := fun _ _ => 0 - bilin_add_left := fun _ _ _ => (add_zero 0).symm - bilin_smul_left := fun a _ _ => (mul_zero a).symm - bilin_add_right := fun _ _ _ => (zero_add 0).symm - bilin_smul_right := fun a _ _ => (mul_zero a).symm } +instance : Zero (BilinForm R M) := inferInstance -@[simp] theorem coe_zero : ⇑(0 : BilinForm R M) = 0 := rfl -#align bilin_form.coe_zero BilinForm.coe_zero +#align bilin_form.coe_zero LinearMap.BilinForm.coe_zero @[simp] theorem zero_apply (x y : M) : (0 : BilinForm R M) x y = 0 := rfl -#align bilin_form.zero_apply BilinForm.zero_apply +#align bilin_form.zero_apply LinearMap.BilinForm.zero_apply variable (B D B₁ D₁) -instance : Add (BilinForm R M) where - add B D := - { bilin := fun x y => B x y + D x y - bilin_add_left := fun x y z => by simp only [add_left, add_left, add_add_add_comm] - bilin_smul_left := fun a x y => by simp only [smul_left, smul_left, mul_add] - bilin_add_right := fun x y z => by simp only [add_right, add_right, add_add_add_comm] - bilin_smul_right := fun a x y => by simp only [smul_right, smul_right, mul_add] } +instance : Add (BilinForm R M) := inferInstance -@[simp] theorem coe_add : ⇑(B + D) = B + D := rfl -#align bilin_form.coe_add BilinForm.coe_add +#align bilin_form.coe_add LinearMap.BilinForm.coe_add @[simp] theorem add_apply (x y : M) : (B + D) x y = B x y + D x y := rfl -#align bilin_form.add_apply BilinForm.add_apply +#align bilin_form.add_apply LinearMap.BilinForm.add_apply /-- `BilinForm R M` inherits the scalar action by `α` on `R` if this is compatible with multiplication. When `R` itself is commutative, this provides an `R`-action via `Algebra.id`. -/ -instance {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R R] : SMul α (BilinForm R M) where - smul c B := - { bilin := fun x y => c • B x y - bilin_add_left := fun x y z => by simp only [add_left, smul_add] - bilin_smul_left := fun a x y => by simp only [smul_left, mul_smul_comm] - bilin_add_right := fun x y z => by simp only [add_right, smul_add] - bilin_smul_right := fun a x y => by simp only [smul_right, mul_smul_comm] } +instance {α} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] : SMul α (BilinForm R M) := + inferInstance -@[simp] -theorem coe_smul {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R R] (a : α) - (B : BilinForm R M) : ⇑(a • B) = a • ⇑B := - rfl -#align bilin_form.coe_smul BilinForm.coe_smul - -@[simp] -theorem smul_apply {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R R] (a : α) - (B : BilinForm R M) (x y : M) : (a • B) x y = a • B x y := - rfl -#align bilin_form.smul_apply BilinForm.smul_apply +#noalign bilin_form.coe_smul +#noalign bilin_form.smul_apply instance {α β} [Monoid α] [Monoid β] [DistribMulAction α R] [DistribMulAction β R] - [SMulCommClass α R R] [SMulCommClass β R R] [SMulCommClass α β R] : - SMulCommClass α β (BilinForm R M) := - ⟨fun a b B => ext fun x y => smul_comm a b (B x y)⟩ + [SMulCommClass R α R] [SMulCommClass R β R] [SMulCommClass α β R] : + SMulCommClass α β (BilinForm R M) := inferInstance instance {α β} [Monoid α] [Monoid β] [SMul α β] [DistribMulAction α R] [DistribMulAction β R] - [SMulCommClass α R R] [SMulCommClass β R R] [IsScalarTower α β R] : - IsScalarTower α β (BilinForm R M) := - ⟨fun a b B => ext fun x y => smul_assoc a b (B x y)⟩ + [SMulCommClass R α R] [SMulCommClass R β R] [IsScalarTower α β R] : + IsScalarTower α β (BilinForm R M) := inferInstance instance {α} [Monoid α] [DistribMulAction α R] [DistribMulAction αᵐᵒᵖ R] - [SMulCommClass α R R] [IsCentralScalar α R] : - IsCentralScalar α (BilinForm R M) := - ⟨fun a B => ext fun x y => op_smul_eq_smul a (B x y)⟩ + [SMulCommClass R α R] [IsCentralScalar α R] : + IsCentralScalar α (BilinForm R M) := inferInstance -instance : AddCommMonoid (BilinForm R M) := - Function.Injective.addCommMonoid _ coe_injective coe_zero coe_add fun _ _ => coe_smul _ _ +instance : AddCommMonoid (BilinForm R M) := inferInstance -instance : Neg (BilinForm R₁ M₁) where - neg B := - { bilin := fun x y => -B x y - bilin_add_left := fun x y z => by simp only [add_left, neg_add] - bilin_smul_left := fun a x y => by simp only [smul_left, mul_neg] - bilin_add_right := fun x y z => by simp only [add_right, neg_add] - bilin_smul_right := fun a x y => by simp only [smul_right, mul_neg] } +instance : Neg (BilinForm R₁ M₁) := inferInstance -@[simp] theorem coe_neg : ⇑(-B₁) = -B₁ := rfl -#align bilin_form.coe_neg BilinForm.coe_neg +#align bilin_form.coe_neg LinearMap.BilinForm.coe_neg @[simp] theorem neg_apply (x y : M₁) : (-B₁) x y = -B₁ x y := rfl -#align bilin_form.neg_apply BilinForm.neg_apply +#align bilin_form.neg_apply LinearMap.BilinForm.neg_apply -instance : Sub (BilinForm R₁ M₁) where - sub B D := - { bilin := fun x y => B x y - D x y - bilin_add_left := fun x y z => by simp only [add_left, add_left, add_sub_add_comm] - bilin_smul_left := fun a x y => by simp only [smul_left, smul_left, mul_sub] - bilin_add_right := fun x y z => by simp only [add_right, add_right, add_sub_add_comm] - bilin_smul_right := fun a x y => by simp only [smul_right, smul_right, mul_sub] } +instance : Sub (BilinForm R₁ M₁) := inferInstance -@[simp] theorem coe_sub : ⇑(B₁ - D₁) = B₁ - D₁ := rfl -#align bilin_form.coe_sub BilinForm.coe_sub +#align bilin_form.coe_sub LinearMap.BilinForm.coe_sub @[simp] theorem sub_apply (x y : M₁) : (B₁ - D₁) x y = B₁ x y - D₁ x y := rfl -#align bilin_form.sub_apply BilinForm.sub_apply +#align bilin_form.sub_apply LinearMap.BilinForm.sub_apply -instance : AddCommGroup (BilinForm R₁ M₁) := - Function.Injective.addCommGroup _ coe_injective coe_zero coe_add coe_neg coe_sub - (fun _ _ => coe_smul _ _) fun _ _ => coe_smul _ _ +instance : AddCommGroup (BilinForm R₁ M₁) := inferInstance -instance : Inhabited (BilinForm R M) := - ⟨0⟩ +instance : Inhabited (BilinForm R M) := inferInstance /-- `coeFn` as an `AddMonoidHom` -/ def coeFnAddMonoidHom : BilinForm R M →+ M → M → R where - toFun := (↑) - map_zero' := coe_zero - map_add' := coe_add -#align bilin_form.coe_fn_add_monoid_hom BilinForm.coeFnAddMonoidHom + toFun := (fun B x y => B x y) + map_zero' := rfl + map_add' _ _ := rfl +#align bilin_form.coe_fn_add_monoid_hom LinearMap.BilinForm.coeFnAddMonoidHom -instance {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R R] : - DistribMulAction α (BilinForm R M) := - Function.Injective.distribMulAction coeFnAddMonoidHom coe_injective coe_smul +instance {α} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] : + DistribMulAction α (BilinForm R M) := inferInstance -instance {α} [CommSemiring α] [Module α R] [SMulCommClass α R R] : Module α (BilinForm R M) := - Function.Injective.module _ coeFnAddMonoidHom coe_injective coe_smul +instance {α} [CommSemiring α] [Module α R] [SMulCommClass R α R] : Module α (BilinForm R M) := + inferInstance section flip /-- Auxiliary construction for the flip of a bilinear form, obtained by exchanging the left and right arguments. This version is a `LinearMap`; it is later upgraded to a `LinearEquiv` in `flipHom`. -/ -def flipHomAux : BilinForm R M →ₗ[R] BilinForm R M where - toFun A := - { bilin := fun i j => A j i - bilin_add_left := fun x y z => A.bilin_add_right z x y - bilin_smul_left := fun a x y => A.bilin_smul_right a y x - bilin_add_right := fun x y z => A.bilin_add_left y z x - bilin_smul_right := fun a x y => A.bilin_smul_left a y x } +def flipHomAux : (BilinForm R M) →ₗ[R] (BilinForm R M) where + toFun A := A.flip map_add' A₁ A₂ := by ext - simp + simp only [LinearMap.flip_apply, LinearMap.add_apply] map_smul' c A := by ext - simp -#align bilin_form.flip_hom_aux BilinForm.flipHomAux - -variable {R₂} + simp only [LinearMap.flip_apply, LinearMap.smul_apply, RingHom.id_apply] +#align bilin_form.flip_hom_aux LinearMap.BilinForm.flipHomAux theorem flip_flip_aux (A : BilinForm R M) : - (flipHomAux) (flipHomAux A) = A := by + flipHomAux (M := M) (flipHomAux (M := M) A) = A := by ext A simp [flipHomAux] -#align bilin_form.flip_flip_aux BilinForm.flip_flip_aux - -variable (R₂) +#align bilin_form.flip_flip_aux LinearMap.BilinForm.flip_flip_aux /-- The flip of a bilinear form, obtained by exchanging the left and right arguments. -/ def flipHom : BilinForm R M ≃ₗ[R] BilinForm R M := { flipHomAux with - invFun := flipHomAux + invFun := flipHomAux (M := M) left_inv := flip_flip_aux right_inv := flip_flip_aux } -#align bilin_form.flip_hom BilinForm.flipHom +#align bilin_form.flip_hom LinearMap.BilinForm.flipHom @[simp] theorem flip_apply (A : BilinForm R M) (x y : M) : flipHom A x y = A y x := rfl -#align bilin_form.flip_apply BilinForm.flip_apply +#align bilin_form.flip_apply LinearMap.BilinForm.flip_apply theorem flip_flip : flipHom.trans flipHom = LinearEquiv.refl R (BilinForm R M) := by ext A simp -#align bilin_form.flip_flip BilinForm.flip_flip +#align bilin_form.flip_flip LinearMap.BilinForm.flip_flip /-- The `flip` of a bilinear form over a commutative ring, obtained by exchanging the left and right arguments. -/ abbrev flip : BilinForm R M ≃ₗ[R] BilinForm R M := flipHom -#align bilin_form.flip BilinForm.flip +#align bilin_form.flip LinearMap.BilinForm.flip end flip /-- The restriction of a bilinear form on a submodule. -/ -@[simps apply] -def restrict (B : BilinForm R M) (W : Submodule R M) : BilinForm R W where - bilin a b := B a b - bilin_add_left _ _ _ := add_left _ _ _ - bilin_smul_left _ _ _ := smul_left _ _ _ - bilin_add_right _ _ _ := add_right _ _ _ - bilin_smul_right _ _ _ := smul_right _ _ _ -#align bilin_form.restrict BilinForm.restrict +@[simps! apply] +def restrict (B : BilinForm R M) (W : Submodule R M) : BilinForm R W := + LinearMap.domRestrict₁₂ B W W +#align bilin_form.restrict LinearMap.BilinForm.restrict end BilinForm + +end LinearMap diff --git a/Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean b/Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean index 5e6754751671f6..0266a45199c4af 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean @@ -17,9 +17,13 @@ import Mathlib.LinearAlgebra.BilinearForm.Properties Properly develop the material in the context of lattices. -/ +open LinearMap (BilinForm) + variable {R S M} [CommRing R] [Field S] [AddCommGroup M] variable [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] +namespace LinearMap + namespace BilinForm variable (B : BilinForm S M) @@ -31,7 +35,8 @@ def dualSubmodule (N : Submodule R M) : Submodule R M where zero_mem' y _ := by rw [B.zero_left]; exact zero_mem _ smul_mem' r a ha y hy := by convert (1 : Submodule R S).smul_mem r (ha y hy) - rw [← IsScalarTower.algebraMap_smul S r a, bilin_smul_left, Algebra.smul_def] + rw [← IsScalarTower.algebraMap_smul S r a] + simp only [algebraMap_smul, map_smul_of_tower, LinearMap.smul_apply] lemma mem_dualSubmodule {N : Submodule R M} {x} : x ∈ B.dualSubmodule N ↔ ∀ y ∈ N, B x y ∈ (1 : Submodule R S) := Iff.rfl @@ -96,11 +101,12 @@ lemma dualSubmodule_span_of_basis {ι} [Finite ι] [DecidableEq ι] · rw [Submodule.span_le] rintro _ ⟨i, rfl⟩ y hy obtain ⟨f, rfl⟩ := (mem_span_range_iff_exists_fun _).mp hy - simp only [sum_right, bilin_smul_right] + simp only [map_sum, map_smul] apply sum_mem rintro j - - rw [← IsScalarTower.algebraMap_smul S (f j), B.bilin_smul_right, apply_dualBasis_left, - mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite] + rw [← IsScalarTower.algebraMap_smul S (f j), map_smul] + simp_rw [apply_dualBasis_left] + rw [smul_eq_mul, mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite] exact ⟨_, rfl⟩ lemma dualSubmodule_dualSubmodule_flip_of_basis {ι : Type*} [Finite ι] diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index 8704baa0bf4bfc..fc7f9ea65c6e6e 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -6,12 +6,19 @@ Authors: Andreas Swerdlow, Kexing Ying import Mathlib.LinearAlgebra.BilinearMap import Mathlib.LinearAlgebra.BilinearForm.Basic import Mathlib.LinearAlgebra.Basis +import Mathlib.Algebra.Algebra.Bilinear /-! # Bilinear form and linear maps This file describes the relation between bilinear forms and linear maps. +## TODO + +A lot of this file is now redundant following the replacement of the dedicated `_root_.BilinForm` +structure with `LinearMap.BilinForm`, which is just an alias for `M →ₗ[R] M →ₗ[R] R`. For example +`LinearMap.BilinForm.toLinHom` is now just the identity map. This redundant code should be removed. + ## Notations Given any term `B` of type `BilinForm`, due to a coercion, can use @@ -31,9 +38,10 @@ In this file we use the following type variables: Bilinear form, -/ - open BigOperators +open LinearMap (BilinForm) + universe u v w variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] @@ -41,73 +49,42 @@ variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Modu variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V] variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} +namespace LinearMap + namespace BilinForm section ToLin' /-- Auxiliary definition to define `toLinHom`; see below. -/ -def toLinHomAux₁ (A : BilinForm R M) (x : M) : M →ₗ[R] R where - toFun y := A x y - map_add' := A.bilin_add_right x - map_smul' c := A.bilin_smul_right c x -#align bilin_form.to_lin_hom_aux₁ BilinForm.toLinHomAux₁ +def toLinHomAux₁ (A : BilinForm R M) (x : M) : M →ₗ[R] R := A x +#align bilin_form.to_lin_hom_aux₁ LinearMap.BilinForm.toLinHomAux₁ /-- Auxiliary definition to define `toLinHom`; see below. -/ -def toLinHomAux₂ (A : BilinForm R M) : M →ₗ[R] M →ₗ[R] R where - toFun := toLinHomAux₁ A - map_add' x₁ x₂ := - LinearMap.ext fun x => by - simp only [toLinHomAux₁, LinearMap.coe_mk, LinearMap.add_apply, add_left, AddHom.coe_mk] - map_smul' c x := - LinearMap.ext <| by - dsimp [toLinHomAux₁] - intros - -- Porting note: moved out of `simp only` - rw [← algebraMap_smul R c x] - simp only [Algebra.id.map_eq_id, RingHom.id_apply, smul_left] -#align bilin_form.to_lin_hom_aux₂ BilinForm.toLinHomAux₂ +def toLinHomAux₂ (A : BilinForm R M) : M →ₗ[R] M →ₗ[R] R := A +#align bilin_form.to_lin_hom_aux₂ LinearMap.BilinForm.toLinHomAux₂ /-- The linear map obtained from a `BilinForm` by fixing the left co-ordinate and evaluating in the right. -/ -def toLinHom : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R where - toFun := toLinHomAux₂ - map_add' A₁ A₂ := - LinearMap.ext fun x => by - dsimp only [toLinHomAux₁, toLinHomAux₂] - apply LinearMap.ext - intro y - simp only [toLinHomAux₂, toLinHomAux₁, LinearMap.coe_mk, LinearMap.add_apply, add_apply, - AddHom.coe_mk] - map_smul' c A := by - dsimp [toLinHomAux₁, toLinHomAux₂] - apply LinearMap.ext - intro x - apply LinearMap.ext - intro y - simp only [toLinHomAux₂, toLinHomAux₁, LinearMap.coe_mk, LinearMap.smul_apply, smul_apply, - AddHom.coe_mk] -#align bilin_form.to_lin_hom BilinForm.toLinHom +def toLinHom : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R := LinearMap.id +#align bilin_form.to_lin_hom LinearMap.BilinForm.toLinHom -@[simp] -theorem toLin'_apply (A : BilinForm R M) (x : M) : ⇑(toLinHom A x) = A x := +theorem toLin'_apply (A : BilinForm R M) (x : M) : toLinHom (M := M) A x = A x := rfl -#align bilin_form.to_lin'_apply BilinForm.toLin'_apply +#align bilin_form.to_lin'_apply LinearMap.BilinForm.toLin'_apply variable (B) -@[simp] theorem sum_left {α} (t : Finset α) (g : α → M) (w : M) : B (∑ i in t, g i) w = ∑ i in t, B (g i) w := - (BilinForm.toLinHom B).map_sum₂ t g w -#align bilin_form.sum_left BilinForm.sum_left + (BilinForm.toLinHom (M := M) B).map_sum₂ t g w +#align bilin_form.sum_left LinearMap.BilinForm.sum_left + +variable (w : M) -@[simp] theorem sum_right {α} (t : Finset α) (w : M) (g : α → M) : - B w (∑ i in t, g i) = ∑ i in t, B w (g i) := - map_sum (BilinForm.toLinHom B w) _ _ -#align bilin_form.sum_right BilinForm.sum_right + B w (∑ i in t, g i) = ∑ i in t, B w (g i) := map_sum _ _ _ +#align bilin_form.sum_right LinearMap.BilinForm.sum_right -@[simp] theorem sum_apply {α} (t : Finset α) (B : α → BilinForm R M) (v w : M) : (∑ i in t, B i) v w = ∑ i in t, B i v w := by show coeFnAddMonoidHom (∑ i in t, B i) v w = _ @@ -120,44 +97,34 @@ variable {B} the left. -/ def toLinHomFlip : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R := toLinHom.comp flipHom.toLinearMap -#align bilin_form.to_lin_hom_flip BilinForm.toLinHomFlip +#align bilin_form.to_lin_hom_flip LinearMap.BilinForm.toLinHomFlip -@[simp] -theorem toLin'Flip_apply (A : BilinForm R M) (x : M) : ⇑(toLinHomFlip A x) = fun y => A y x := +theorem toLin'Flip_apply (A : BilinForm R M) (x : M) : toLinHomFlip (M := M) A x = fun y => A y x := rfl -#align bilin_form.to_lin'_flip_apply BilinForm.toLin'Flip_apply +#align bilin_form.to_lin'_flip_apply LinearMap.BilinForm.toLin'Flip_apply end ToLin' end BilinForm +end LinearMap + section EquivLin /-- A map with two arguments that is linear in both is a bilinear form. This is an auxiliary definition for the full linear equivalence `LinearMap.toBilin`. -/ -def LinearMap.toBilinAux (f : M →ₗ[R] M →ₗ[R] R) : BilinForm R M where - bilin x y := f x y - bilin_add_left x y z := by - simp only - exact (LinearMap.map_add f x y).symm ▸ LinearMap.add_apply (f x) (f y) z - bilin_smul_left a x y := by simp only [LinearMap.map_smul, LinearMap.smul_apply, smul_eq_mul] - bilin_add_right x y z := LinearMap.map_add (f x) y z - bilin_smul_right a x y := LinearMap.map_smul (f x) a y +def LinearMap.toBilinAux (f : M →ₗ[R] M →ₗ[R] R) : BilinForm R M := f #align linear_map.to_bilin_aux LinearMap.toBilinAux /-- Bilinear forms are linearly equivalent to maps with two arguments that are linear in both. -/ -def BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R] R := +def LinearMap.BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R] R := { BilinForm.toLinHom with invFun := LinearMap.toBilinAux - left_inv := fun B => by - ext - simp [LinearMap.toBilinAux] - right_inv := fun B => by - ext - simp [LinearMap.toBilinAux] } -#align bilin_form.to_lin BilinForm.toLin + left_inv := fun _ => rfl + right_inv := fun _ => rfl } +#align bilin_form.to_lin LinearMap.BilinForm.toLin /-- A map with two arguments that is linear in both is linearly equivalent to bilinear form. -/ def LinearMap.toBilin : (M →ₗ[R] M →ₗ[R] R) ≃ₗ[R] BilinForm R M := @@ -182,13 +149,13 @@ theorem BilinForm.toLin_symm : LinearMap.toBilin.symm_symm #align bilin_form.to_lin_symm BilinForm.toLin_symm -@[simp, norm_cast] +@[simp] theorem LinearMap.toBilin_apply (f : M →ₗ[R] M →ₗ[R] R) (x y : M) : toBilin f x y = f x y := rfl -@[simp, norm_cast] -theorem BilinForm.toLin_apply (x : M) : ⇑(BilinForm.toLin B x) = B x := +@[simp] +theorem BilinForm.toLin_apply (x : M) : BilinForm.toLin B x = B x := rfl #align bilin_form.to_lin_apply BilinForm.toLin_apply @@ -199,23 +166,15 @@ namespace LinearMap variable {R' : Type*} [CommSemiring R'] [Algebra R' R] [Module R' M] [IsScalarTower R' R M] /-- Apply a linear map on the output of a bilinear form. -/ -@[simps] -def compBilinForm (f : R →ₗ[R'] R') (B : BilinForm R M) : BilinForm R' M where - bilin x y := f (B x y) - bilin_add_left x y z := by simp only [BilinForm.add_left, map_add] - bilin_smul_left r x y := by - simp only - rw [← smul_one_smul R r (_ : M), BilinForm.smul_left, smul_one_mul r (_ : R), map_smul, - smul_eq_mul] - bilin_add_right x y z := by simp only [BilinForm.add_right, map_add] - bilin_smul_right r x y := by - simp only - rw [← smul_one_smul R r (_ : M), BilinForm.smul_right, smul_one_mul r (_ : R), map_smul, - smul_eq_mul] +@[simps!] +def compBilinForm (f : R →ₗ[R'] R') (B : BilinForm R M) : BilinForm R' M := + compr₂ (restrictScalars₁₂ R' R' B) f #align linear_map.comp_bilin_form LinearMap.compBilinForm end LinearMap +namespace LinearMap + namespace BilinForm section Comp @@ -223,82 +182,77 @@ section Comp variable {M' : Type w} [AddCommMonoid M'] [Module R M'] /-- Apply a linear map on the left and right argument of a bilinear form. -/ -def comp (B : BilinForm R M') (l r : M →ₗ[R] M') : BilinForm R M where - bilin x y := B (l x) (r y) - bilin_add_left x y z := by simp only [LinearMap.map_add, add_left] - bilin_smul_left x y z := by simp only [LinearMap.map_smul, smul_left] - bilin_add_right x y z := by simp only [LinearMap.map_add, add_right] - bilin_smul_right x y z := by simp only [LinearMap.map_smul, smul_right] -#align bilin_form.comp BilinForm.comp +def comp (B : BilinForm R M') (l r : M →ₗ[R] M') : BilinForm R M := B.compl₁₂ l r +#align bilin_form.comp LinearMap.BilinForm.comp /-- Apply a linear map to the left argument of a bilinear form. -/ def compLeft (B : BilinForm R M) (f : M →ₗ[R] M) : BilinForm R M := B.comp f LinearMap.id -#align bilin_form.comp_left BilinForm.compLeft +#align bilin_form.comp_left LinearMap.BilinForm.compLeft /-- Apply a linear map to the right argument of a bilinear form. -/ def compRight (B : BilinForm R M) (f : M →ₗ[R] M) : BilinForm R M := B.comp LinearMap.id f -#align bilin_form.comp_right BilinForm.compRight +#align bilin_form.comp_right LinearMap.BilinForm.compRight theorem comp_comp {M'' : Type*} [AddCommMonoid M''] [Module R M''] (B : BilinForm R M'') (l r : M →ₗ[R] M') (l' r' : M' →ₗ[R] M'') : (B.comp l' r').comp l r = B.comp (l'.comp l) (r'.comp r) := rfl -#align bilin_form.comp_comp BilinForm.comp_comp +#align bilin_form.comp_comp LinearMap.BilinForm.comp_comp @[simp] theorem compLeft_compRight (B : BilinForm R M) (l r : M →ₗ[R] M) : (B.compLeft l).compRight r = B.comp l r := rfl -#align bilin_form.comp_left_comp_right BilinForm.compLeft_compRight +#align bilin_form.comp_left_comp_right LinearMap.BilinForm.compLeft_compRight @[simp] theorem compRight_compLeft (B : BilinForm R M) (l r : M →ₗ[R] M) : (B.compRight r).compLeft l = B.comp l r := rfl -#align bilin_form.comp_right_comp_left BilinForm.compRight_compLeft +#align bilin_form.comp_right_comp_left LinearMap.BilinForm.compRight_compLeft @[simp] theorem comp_apply (B : BilinForm R M') (l r : M →ₗ[R] M') (v w) : B.comp l r v w = B (l v) (r w) := rfl -#align bilin_form.comp_apply BilinForm.comp_apply +#align bilin_form.comp_apply LinearMap.BilinForm.comp_apply @[simp] theorem compLeft_apply (B : BilinForm R M) (f : M →ₗ[R] M) (v w) : B.compLeft f v w = B (f v) w := rfl -#align bilin_form.comp_left_apply BilinForm.compLeft_apply +#align bilin_form.comp_left_apply LinearMap.BilinForm.compLeft_apply @[simp] theorem compRight_apply (B : BilinForm R M) (f : M →ₗ[R] M) (v w) : B.compRight f v w = B v (f w) := rfl -#align bilin_form.comp_right_apply BilinForm.compRight_apply +#align bilin_form.comp_right_apply LinearMap.BilinForm.compRight_apply @[simp] theorem comp_id_left (B : BilinForm R M) (r : M →ₗ[R] M) : B.comp LinearMap.id r = B.compRight r := by ext rfl -#align bilin_form.comp_id_left BilinForm.comp_id_left +#align bilin_form.comp_id_left LinearMap.BilinForm.comp_id_left @[simp] theorem comp_id_right (B : BilinForm R M) (l : M →ₗ[R] M) : B.comp l LinearMap.id = B.compLeft l := by ext rfl -#align bilin_form.comp_id_right BilinForm.comp_id_right +#align bilin_form.comp_id_right LinearMap.BilinForm.comp_id_right @[simp] theorem compLeft_id (B : BilinForm R M) : B.compLeft LinearMap.id = B := by ext rfl -#align bilin_form.comp_left_id BilinForm.compLeft_id +#align bilin_form.comp_left_id LinearMap.BilinForm.compLeft_id @[simp] theorem compRight_id (B : BilinForm R M) : B.compRight LinearMap.id = B := by ext rfl -#align bilin_form.comp_right_id BilinForm.compRight_id +#align bilin_form.comp_right_id LinearMap.BilinForm.compRight_id -- Shortcut for `comp_id_{left,right}` followed by `comp{Right,Left}_id`, -- Needs higher priority to be applied @@ -306,7 +260,7 @@ theorem compRight_id (B : BilinForm R M) : B.compRight LinearMap.id = B := by theorem comp_id_id (B : BilinForm R M) : B.comp LinearMap.id LinearMap.id = B := by ext rfl -#align bilin_form.comp_id_id BilinForm.comp_id_id +#align bilin_form.comp_id_id LinearMap.BilinForm.comp_id_id theorem comp_inj (B₁ B₂ : BilinForm 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₂ := by @@ -320,7 +274,7 @@ theorem comp_inj (B₁ B₂ : BilinForm R M') {l r : M →ₗ[R] M'} (hₗ : Fun rw [← comp_apply, ← comp_apply, h] · -- B₁ = B₂ → B₁.comp l r = B₂.comp l r rw [h] -#align bilin_form.comp_inj BilinForm.comp_inj +#align bilin_form.comp_inj LinearMap.BilinForm.comp_inj end Comp @@ -333,90 +287,87 @@ section congr def congr (e : M ≃ₗ[R] M') : BilinForm R M ≃ₗ[R] BilinForm R M' where toFun B := B.comp e.symm e.symm invFun B := B.comp e e - left_inv B := ext fun x y => by simp only [comp_apply, LinearEquiv.coe_coe, e.symm_apply_apply] - right_inv B := ext fun x y => by simp only [comp_apply, LinearEquiv.coe_coe, e.apply_symm_apply] - map_add' B B' := ext fun x y => by simp only [comp_apply, add_apply] - map_smul' B B' := ext fun x y => by simp [comp_apply, smul_apply] -#align bilin_form.congr BilinForm.congr + left_inv B := ext₂ fun x => by + simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, forall_const] + right_inv B := ext₂ fun x => by + simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, forall_const] + map_add' B B' := ext₂ fun x y => rfl + map_smul' B B' := ext₂ fun x y => rfl +#align bilin_form.congr LinearMap.BilinForm.congr @[simp] theorem congr_apply (e : M ≃ₗ[R] M') (B : BilinForm R M) (x y : M') : congr e B x y = B (e.symm x) (e.symm y) := rfl -#align bilin_form.congr_apply BilinForm.congr_apply +#align bilin_form.congr_apply LinearMap.BilinForm.congr_apply @[simp] theorem congr_symm (e : M ≃ₗ[R] M') : (congr e).symm = congr e.symm := by ext simp only [congr_apply, LinearEquiv.symm_symm] rfl -#align bilin_form.congr_symm BilinForm.congr_symm +#align bilin_form.congr_symm LinearMap.BilinForm.congr_symm @[simp] theorem congr_refl : congr (LinearEquiv.refl R M) = LinearEquiv.refl R _ := - LinearEquiv.ext fun _ => ext fun _ _ => rfl -#align bilin_form.congr_refl BilinForm.congr_refl + LinearEquiv.ext fun _ => ext₂ fun _ _ => rfl +#align bilin_form.congr_refl LinearMap.BilinForm.congr_refl theorem congr_trans (e : M ≃ₗ[R] M') (f : M' ≃ₗ[R] M'') : (congr e).trans (congr f) = congr (e.trans f) := rfl -#align bilin_form.congr_trans BilinForm.congr_trans +#align bilin_form.congr_trans LinearMap.BilinForm.congr_trans theorem congr_congr (e : M' ≃ₗ[R] M'') (f : M ≃ₗ[R] M') (B : BilinForm R M) : congr e (congr f B) = congr (f.trans e) B := rfl -#align bilin_form.congr_congr BilinForm.congr_congr +#align bilin_form.congr_congr LinearMap.BilinForm.congr_congr theorem congr_comp (e : M ≃ₗ[R] M') (B : BilinForm R M) (l r : M'' →ₗ[R] M') : (congr e B).comp l r = B.comp (LinearMap.comp (e.symm : M' →ₗ[R] M) l) (LinearMap.comp (e.symm : M' →ₗ[R] M) r) := rfl -#align bilin_form.congr_comp BilinForm.congr_comp +#align bilin_form.congr_comp LinearMap.BilinForm.congr_comp theorem comp_congr (e : M' ≃ₗ[R] M'') (B : BilinForm R M) (l r : M' →ₗ[R] M) : congr e (B.comp l r) = B.comp (l.comp (e.symm : M'' →ₗ[R] M')) (r.comp (e.symm : M'' →ₗ[R] M')) := rfl -#align bilin_form.comp_congr BilinForm.comp_congr +#align bilin_form.comp_congr LinearMap.BilinForm.comp_congr end congr section LinMulLin /-- `linMulLin f g` is the bilinear form mapping `x` and `y` to `f x * g y` -/ -def linMulLin (f g : M →ₗ[R] R) : BilinForm R M where - bilin x y := f x * g y - bilin_add_left x y z := by simp only [LinearMap.map_add, add_mul] - bilin_smul_left x y z := by simp only [LinearMap.map_smul, smul_eq_mul, mul_assoc] - bilin_add_right x y z := by simp only [LinearMap.map_add, mul_add] - bilin_smul_right x y z := by simp only [LinearMap.map_smul, smul_eq_mul, mul_left_comm] -#align bilin_form.lin_mul_lin BilinForm.linMulLin +def linMulLin (f g : M →ₗ[R] R) : BilinForm R M := (LinearMap.mul R R).compl₁₂ f g +#align bilin_form.lin_mul_lin LinearMap.BilinForm.linMulLin variable {f g : M →ₗ[R] R} @[simp] theorem linMulLin_apply (x y) : linMulLin f g x y = f x * g y := rfl -#align bilin_form.lin_mul_lin_apply BilinForm.linMulLin_apply +#align bilin_form.lin_mul_lin_apply LinearMap.BilinForm.linMulLin_apply @[simp] theorem linMulLin_comp (l r : M' →ₗ[R] M) : (linMulLin f g).comp l r = linMulLin (f.comp l) (g.comp r) := rfl -#align bilin_form.lin_mul_lin_comp BilinForm.linMulLin_comp +#align bilin_form.lin_mul_lin_comp LinearMap.BilinForm.linMulLin_comp @[simp] theorem linMulLin_compLeft (l : M →ₗ[R] M) : (linMulLin f g).compLeft l = linMulLin (f.comp l) g := rfl -#align bilin_form.lin_mul_lin_comp_left BilinForm.linMulLin_compLeft +#align bilin_form.lin_mul_lin_comp_left LinearMap.BilinForm.linMulLin_compLeft @[simp] theorem linMulLin_compRight (r : M →ₗ[R] M) : (linMulLin f g).compRight r = linMulLin f (g.comp r) := rfl -#align bilin_form.lin_mul_lin_comp_right BilinForm.linMulLin_compRight +#align bilin_form.lin_mul_lin_comp_right LinearMap.BilinForm.linMulLin_compRight end LinMulLin @@ -427,8 +378,8 @@ variable {ι : Type*} (b : Basis ι R M) /-- Two bilinear forms are equal when they are equal on all basis vectors. -/ theorem ext_basis (h : ∀ i j, B (b i) (b j) = F₂ (b i) (b j)) : B = F₂ := - toLin.injective <| b.ext fun i => b.ext fun j => h i j -#align bilin_form.ext_basis BilinForm.ext_basis + b.ext fun i => b.ext fun j => h i j +#align bilin_form.ext_basis LinearMap.BilinForm.ext_basis /-- Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis. -/ theorem sum_repr_mul_repr_mul (x y : M) : @@ -436,8 +387,10 @@ theorem sum_repr_mul_repr_mul (x y : M) : conv_rhs => rw [← b.total_repr x, ← b.total_repr y] simp_rw [Finsupp.total_apply, Finsupp.sum, sum_left, sum_right, smul_left, smul_right, smul_eq_mul] -#align bilin_form.sum_repr_mul_repr_mul BilinForm.sum_repr_mul_repr_mul +#align bilin_form.sum_repr_mul_repr_mul LinearMap.BilinForm.sum_repr_mul_repr_mul end Basis end BilinForm + +end LinearMap diff --git a/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean b/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean index c24b80c12f4c50..8e0abc9a27a53f 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean @@ -33,6 +33,8 @@ Bilinear form, open BigOperators +open LinearMap (BilinForm) + universe u v w variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] @@ -40,41 +42,42 @@ variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Modu variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V] variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} +namespace LinearMap + namespace BilinForm /-- The proposition that two elements of a bilinear form space are orthogonal. For orthogonality of an indexed set of elements, use `BilinForm.iIsOrtho`. -/ def IsOrtho (B : BilinForm R M) (x y : M) : Prop := B x y = 0 -#align bilin_form.is_ortho BilinForm.IsOrtho +#align bilin_form.is_ortho LinearMap.BilinForm.IsOrtho theorem isOrtho_def {B : BilinForm R M} {x y : M} : B.IsOrtho x y ↔ B x y = 0 := Iff.rfl -#align bilin_form.is_ortho_def BilinForm.isOrtho_def +#align bilin_form.is_ortho_def LinearMap.BilinForm.isOrtho_def -theorem isOrtho_zero_left (x : M) : IsOrtho B (0 : M) x := - zero_left x -#align bilin_form.is_ortho_zero_left BilinForm.isOrtho_zero_left +theorem isOrtho_zero_left (x : M) : IsOrtho B (0 : M) x := LinearMap.isOrtho_zero_left B x +#align bilin_form.is_ortho_zero_left LinearMap.BilinForm.isOrtho_zero_left theorem isOrtho_zero_right (x : M) : IsOrtho B x (0 : M) := zero_right x -#align bilin_form.is_ortho_zero_right BilinForm.isOrtho_zero_right +#align bilin_form.is_ortho_zero_right LinearMap.BilinForm.isOrtho_zero_right theorem ne_zero_of_not_isOrtho_self {B : BilinForm K V} (x : V) (hx₁ : ¬B.IsOrtho x x) : x ≠ 0 := fun hx₂ => hx₁ (hx₂.symm ▸ isOrtho_zero_left _) -#align bilin_form.ne_zero_of_not_is_ortho_self BilinForm.ne_zero_of_not_isOrtho_self +#align bilin_form.ne_zero_of_not_is_ortho_self LinearMap.BilinForm.ne_zero_of_not_isOrtho_self theorem IsRefl.ortho_comm (H : B.IsRefl) {x y : M} : IsOrtho B x y ↔ IsOrtho B y x := ⟨eq_zero H, eq_zero H⟩ -#align bilin_form.is_refl.ortho_comm BilinForm.IsRefl.ortho_comm +#align bilin_form.is_refl.ortho_comm LinearMap.BilinForm.IsRefl.ortho_comm theorem IsAlt.ortho_comm (H : B₁.IsAlt) {x y : M₁} : IsOrtho B₁ x y ↔ IsOrtho B₁ y x := H.isRefl.ortho_comm -#align bilin_form.is_alt.ortho_comm BilinForm.IsAlt.ortho_comm +#align bilin_form.is_alt.ortho_comm LinearMap.BilinForm.IsAlt.ortho_comm theorem IsSymm.ortho_comm (H : B.IsSymm) {x y : M} : IsOrtho B x y ↔ IsOrtho B y x := H.isRefl.ortho_comm -#align bilin_form.is_symm.ortho_comm BilinForm.IsSymm.ortho_comm +#align bilin_form.is_symm.ortho_comm LinearMap.BilinForm.IsSymm.ortho_comm /-- A set of vectors `v` is orthogonal with respect to some bilinear form `B` if and only if for all `i ≠ j`, `B (v i) (v j) = 0`. For orthogonality between two elements, use @@ -82,13 +85,13 @@ if for all `i ≠ j`, `B (v i) (v j) = 0`. For orthogonality between two element def iIsOrtho {n : Type w} (B : BilinForm R M) (v : n → M) : Prop := Pairwise (B.IsOrtho on v) set_option linter.uppercaseLean3 false in -#align bilin_form.is_Ortho BilinForm.iIsOrtho +#align bilin_form.is_Ortho LinearMap.BilinForm.iIsOrtho theorem iIsOrtho_def {n : Type w} {B : BilinForm R M} {v : n → M} : B.iIsOrtho v ↔ ∀ i j : n, i ≠ j → B (v i) (v j) = 0 := Iff.rfl set_option linter.uppercaseLean3 false in -#align bilin_form.is_Ortho_def BilinForm.iIsOrtho_def +#align bilin_form.is_Ortho_def LinearMap.BilinForm.iIsOrtho_def section @@ -99,15 +102,19 @@ variable [AddCommGroup M₄] [Module R₄ M₄] {G : BilinForm R₄ M₄} theorem isOrtho_smul_left {x y : M₄} {a : R₄} (ha : a ≠ 0) : IsOrtho G (a • x) y ↔ IsOrtho G x y := by dsimp only [IsOrtho] - rw [smul_left, mul_eq_zero, or_iff_right ha] -#align bilin_form.is_ortho_smul_left BilinForm.isOrtho_smul_left + rw [map_smul] + simp only [LinearMap.smul_apply, smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp] + exact fun a ↦ (ha a).elim +#align bilin_form.is_ortho_smul_left LinearMap.BilinForm.isOrtho_smul_left @[simp] theorem isOrtho_smul_right {x y : M₄} {a : R₄} (ha : a ≠ 0) : IsOrtho G x (a • y) ↔ IsOrtho G x y := by dsimp only [IsOrtho] - rw [smul_right, mul_eq_zero, or_iff_right ha] -#align bilin_form.is_ortho_smul_right BilinForm.isOrtho_smul_right + rw [map_smul] + simp only [smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp] + exact fun a ↦ (ha a).elim +#align bilin_form.is_ortho_smul_right LinearMap.BilinForm.isOrtho_smul_right /-- A set of orthogonal vectors `v` with respect to some bilinear form `B` is linearly independent if for all `i`, `B (v i) (v i) ≠ 0`. -/ @@ -124,14 +131,10 @@ theorem linearIndependent_of_iIsOrtho {n : Type w} {B : BilinForm K V} {v : n simp_rw [sum_left, smul_left, hsum] at this exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this set_option linter.uppercaseLean3 false in -#align bilin_form.linear_independent_of_is_Ortho BilinForm.linearIndependent_of_iIsOrtho +#align bilin_form.linear_independent_of_is_Ortho LinearMap.BilinForm.linearIndependent_of_iIsOrtho end -end BilinForm - -namespace BilinForm - section Orthogonal /-- The orthogonal complement of a submodule `N` with respect to some bilinear form is the set of @@ -148,7 +151,7 @@ def orthogonal (B : BilinForm R M) (N : Submodule R M) : Submodule R M where rw [IsOrtho, add_right, show B n x = 0 from hx n hn, show B n y = 0 from hy n hn, zero_add] smul_mem' c x hx n hn := by rw [IsOrtho, smul_right, show B n x = 0 from hx n hn, mul_zero] -#align bilin_form.orthogonal BilinForm.orthogonal +#align bilin_form.orthogonal LinearMap.BilinForm.orthogonal variable {N L : Submodule R M} @@ -156,14 +159,14 @@ variable {N L : Submodule R M} theorem mem_orthogonal_iff {N : Submodule R M} {m : M} : m ∈ B.orthogonal N ↔ ∀ n ∈ N, IsOrtho B n m := Iff.rfl -#align bilin_form.mem_orthogonal_iff BilinForm.mem_orthogonal_iff +#align bilin_form.mem_orthogonal_iff LinearMap.BilinForm.mem_orthogonal_iff theorem orthogonal_le (h : N ≤ L) : B.orthogonal L ≤ B.orthogonal N := fun _ hn l hl => hn l (h hl) -#align bilin_form.orthogonal_le BilinForm.orthogonal_le +#align bilin_form.orthogonal_le LinearMap.BilinForm.orthogonal_le theorem le_orthogonal_orthogonal (b : B.IsRefl) : N ≤ B.orthogonal (B.orthogonal N) := fun n hn _ hm => b _ _ (hm n hn) -#align bilin_form.le_orthogonal_orthogonal BilinForm.le_orthogonal_orthogonal +#align bilin_form.le_orthogonal_orthogonal LinearMap.BilinForm.le_orthogonal_orthogonal -- ↓ This lemma only applies in fields as we require `a * b = 0 → a = 0 ∨ b = 0` theorem span_singleton_inf_orthogonal_eq_bot {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) : @@ -179,11 +182,11 @@ theorem span_singleton_inf_orthogonal_eq_bot {B : BilinForm K V} {x : V} (hx : exact eq_zero_of_ne_zero_of_mul_right_eq_zero hx this · rw [Submodule.mem_span] exact fun _ hp => hp <| Finset.mem_singleton_self _ -#align bilin_form.span_singleton_inf_orthogonal_eq_bot BilinForm.span_singleton_inf_orthogonal_eq_bot +#align bilin_form.span_singleton_inf_orthogonal_eq_bot LinearMap.BilinForm.span_singleton_inf_orthogonal_eq_bot -- ↓ This lemma only applies in fields since we use the `mul_eq_zero` theorem orthogonal_span_singleton_eq_toLin_ker {B : BilinForm K V} (x : V) : - B.orthogonal (K ∙ x) = LinearMap.ker (BilinForm.toLin B x) := by + B.orthogonal (K ∙ x) = LinearMap.ker (LinearMap.BilinForm.toLinHomAux₁ B x) := by ext y simp_rw [mem_orthogonal_iff, LinearMap.mem_ker, Submodule.mem_span_singleton] constructor @@ -191,13 +194,13 @@ theorem orthogonal_span_singleton_eq_toLin_ker {B : BilinForm K V} (x : V) : · rintro h _ ⟨z, rfl⟩ rw [IsOrtho, smul_left, mul_eq_zero] exact Or.intro_right _ h -#align bilin_form.orthogonal_span_singleton_eq_to_lin_ker BilinForm.orthogonal_span_singleton_eq_toLin_ker +#align bilin_form.orthogonal_span_singleton_eq_to_lin_ker LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker theorem span_singleton_sup_orthogonal_eq_top {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) : (K ∙ x) ⊔ B.orthogonal (K ∙ x) = ⊤ := by rw [orthogonal_span_singleton_eq_toLin_ker] exact LinearMap.span_singleton_sup_ker_eq_top _ hx -#align bilin_form.span_singleton_sup_orthogonal_eq_top BilinForm.span_singleton_sup_orthogonal_eq_top +#align bilin_form.span_singleton_sup_orthogonal_eq_top LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top /-- Given a bilinear form `B` and some `x` such that `B x x ≠ 0`, the span of the singleton of `x` is complement to its orthogonal complement. -/ @@ -205,7 +208,7 @@ theorem isCompl_span_singleton_orthogonal {B : BilinForm K V} {x : V} (hx : ¬B. IsCompl (K ∙ x) (B.orthogonal <| K ∙ x) := { disjoint := disjoint_iff.2 <| span_singleton_inf_orthogonal_eq_bot hx codisjoint := codisjoint_iff.2 <| span_singleton_sup_orthogonal_eq_top hx } -#align bilin_form.is_compl_span_singleton_orthogonal BilinForm.isCompl_span_singleton_orthogonal +#align bilin_form.is_compl_span_singleton_orthogonal LinearMap.BilinForm.isCompl_span_singleton_orthogonal end Orthogonal @@ -220,9 +223,9 @@ theorem nondegenerateRestrictOfDisjointOrthogonal (B : BilinForm R₁ M₁) (b : rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R₁] refine' hW.le_bot ⟨hx, fun y hy => _⟩ specialize b₁ ⟨y, hy⟩ - rw [restrict_apply, Submodule.coe_mk, Submodule.coe_mk] at b₁ + simp only [restrict_apply, domRestrict_apply] at b₁ exact isOrtho_def.mpr (b x y b₁) -#align bilin_form.nondegenerate_restrict_of_disjoint_orthogonal BilinForm.nondegenerateRestrictOfDisjointOrthogonal +#align bilin_form.nondegenerate_restrict_of_disjoint_orthogonal LinearMap.BilinForm.nondegenerateRestrictOfDisjointOrthogonal /-- An orthogonal basis with respect to a nondegenerate bilinear form has no self-orthogonal elements. -/ @@ -241,7 +244,7 @@ theorem iIsOrtho.not_isOrtho_basis_self_of_nondegenerate {n : Type w} [Nontrivia · exact ho · exact h hij set_option linter.uppercaseLean3 false in -#align bilin_form.is_Ortho.not_is_ortho_basis_self_of_nondegenerate BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate +#align bilin_form.is_Ortho.not_is_ortho_basis_self_of_nondegenerate LinearMap.BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate /-- Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate iff the basis has no elements which are self-orthogonal. -/ @@ -264,12 +267,12 @@ theorem iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {n : Type w} [Nontrivi convert zero_mul (M₀ := R) _ using 2 exact Finsupp.not_mem_support_iff.mp hi set_option linter.uppercaseLean3 false in -#align bilin_form.is_Ortho.nondegenerate_iff_not_is_ortho_basis_self BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self +#align bilin_form.is_Ortho.nondegenerate_iff_not_is_ortho_basis_self LinearMap.BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self section theorem toLin_restrict_ker_eq_inf_orthogonal (B : BilinForm K V) (W : Subspace K V) (b : B.IsRefl) : - (B.toLin.domRestrict W).ker.map W.subtype = (W ⊓ B.orthogonal ⊤ : Subspace K V) := by + (B.domRestrict W).ker.map W.subtype = (W ⊓ B.orthogonal ⊤ : Subspace K V) := by ext x; constructor <;> intro hx · rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩ erw [LinearMap.mem_ker] at hker @@ -277,7 +280,7 @@ theorem toLin_restrict_ker_eq_inf_orthogonal (B : BilinForm K V) (W : Subspace K · simp [hx] · intro y _ rw [IsOrtho, b] - change (B.toLin.domRestrict W) ⟨x, hx⟩ y = 0 + change (B.domRestrict W) ⟨x, hx⟩ y = 0 rw [hker] rfl · simp_rw [Submodule.mem_map, LinearMap.mem_ker] @@ -286,18 +289,18 @@ theorem toLin_restrict_ker_eq_inf_orthogonal (B : BilinForm K V) (W : Subspace K change B x y = 0 rw [b] exact hx.2 _ Submodule.mem_top -#align bilin_form.to_lin_restrict_ker_eq_inf_orthogonal BilinForm.toLin_restrict_ker_eq_inf_orthogonal +#align bilin_form.to_lin_restrict_ker_eq_inf_orthogonal LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal theorem toLin_restrict_range_dualCoannihilator_eq_orthogonal (B : BilinForm K V) - (W : Subspace K V) : (B.toLin.domRestrict W).range.dualCoannihilator = B.orthogonal W := by + (W : Subspace K V) : (B.domRestrict W).range.dualCoannihilator = B.orthogonal W := by ext x; constructor <;> rw [mem_orthogonal_iff] <;> intro hx · intro y hy rw [Submodule.mem_dualCoannihilator] at hx - exact hx (B.toLin.domRestrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩ + exact hx (B.domRestrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩ · rw [Submodule.mem_dualCoannihilator] rintro _ ⟨⟨w, hw⟩, rfl⟩ exact hx w hw -#align bilin_form.to_lin_restrict_range_dual_coannihilator_eq_orthogonal BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal +#align bilin_form.to_lin_restrict_range_dual_coannihilator_eq_orthogonal LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal variable [FiniteDimensional K V] @@ -310,10 +313,10 @@ theorem finrank_add_finrank_orthogonal {B : BilinForm K V} {W : Subspace K V} (b toLin_restrict_range_dualCoannihilator_eq_orthogonal _ _, finrank_map_subtype_eq] conv_rhs => rw [← @Subspace.finrank_add_finrank_dualCoannihilator_eq K V _ _ _ _ - (LinearMap.range (B.toLin.domRestrict W)), - add_comm, ← add_assoc, add_comm (finrank K (LinearMap.ker (B.toLin.domRestrict W))), + (LinearMap.range (B.domRestrict W)), + add_comm, ← add_assoc, add_comm (finrank K (LinearMap.ker (B.domRestrict W))), LinearMap.finrank_range_add_finrank_ker] -#align bilin_form.finrank_add_finrank_orthogonal BilinForm.finrank_add_finrank_orthogonal +#align bilin_form.finrank_add_finrank_orthogonal LinearMap.BilinForm.finrank_add_finrank_orthogonal /-- A subspace is complement to its orthogonal complement with respect to some reflexive bilinear form if that bilinear form restricted on to the subspace is nondegenerate. -/ @@ -325,14 +328,14 @@ theorem restrict_nondegenerate_of_isCompl_orthogonal {B : BilinForm K V} {W : Su obtain ⟨hx₁, hx₂⟩ := mem_inf.1 hx refine' Subtype.mk_eq_mk.1 (b₂ ⟨x, hx₁⟩ _) rintro ⟨n, hn⟩ - rw [restrict_apply, coe_mk, coe_mk, b₁] - exact hx₂ n hn + simp only [restrict_apply, domRestrict_apply] + exact b₁ n x (b₁ x n (b₁ n x (hx₂ n hn))) refine' IsCompl.of_eq this (eq_top_of_finrank_eq <| (finrank_le _).antisymm _) conv_rhs => rw [← add_zero (finrank K _)] rw [← finrank_bot K V, ← this, finrank_sup_add_finrank_inf_eq, finrank_add_finrank_orthogonal b₁] exact le_self_add -#align bilin_form.restrict_nondegenerate_of_is_compl_orthogonal BilinForm.restrict_nondegenerate_of_isCompl_orthogonal +#align bilin_form.restrict_nondegenerate_of_is_compl_orthogonal LinearMap.BilinForm.restrict_nondegenerate_of_isCompl_orthogonal /-- A subspace is complement to its orthogonal complement with respect to some reflexive bilinear form if and only if that bilinear form restricted on to the subspace is nondegenerate. -/ @@ -340,7 +343,7 @@ theorem restrict_nondegenerate_iff_isCompl_orthogonal {B : BilinForm K V} {W : S (b₁ : B.IsRefl) : (B.restrict W).Nondegenerate ↔ IsCompl W (B.orthogonal W) := ⟨fun b₂ => restrict_nondegenerate_of_isCompl_orthogonal b₁ b₂, fun h => B.nondegenerateRestrictOfDisjointOrthogonal b₁ h.1⟩ -#align bilin_form.restrict_nondegenerate_iff_is_compl_orthogonal BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal +#align bilin_form.restrict_nondegenerate_iff_is_compl_orthogonal LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal end @@ -362,6 +365,6 @@ theorem restrictOrthogonalSpanSingletonNondegenerate (B : BilinForm K V) (b₁ : specialize hm ⟨z, hz⟩ rw [restrict] at hm erw [add_right, show B m.1 y = 0 by rw [b₂]; exact m.2 y hy, hm, add_zero] -#align bilin_form.restrict_orthogonal_span_singleton_nondegenerate BilinForm.restrictOrthogonalSpanSingletonNondegenerate +#align bilin_form.restrict_orthogonal_span_singleton_nondegenerate LinearMap.BilinForm.restrictOrthogonalSpanSingletonNondegenerate end BilinForm diff --git a/Mathlib/LinearAlgebra/BilinearForm/Properties.lean b/Mathlib/LinearAlgebra/BilinearForm/Properties.lean index 6df88d8c59bdd2..1608da83a02f1b 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Properties.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Properties.lean @@ -35,6 +35,8 @@ Bilinear form, open BigOperators +open LinearMap (BilinForm) + universe u v w variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] @@ -45,6 +47,8 @@ variable [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} +namespace LinearMap + namespace BilinForm /-! ### Reflexivity, symmetry, and alternativity -/ @@ -53,46 +57,46 @@ namespace BilinForm /-- The proposition that a bilinear form is reflexive -/ def IsRefl (B : BilinForm R M) : Prop := ∀ x y : M, B x y = 0 → B y x = 0 -#align bilin_form.is_refl BilinForm.IsRefl +#align bilin_form.is_refl LinearMap.BilinForm.IsRefl namespace IsRefl variable (H : B.IsRefl) theorem eq_zero : ∀ {x y : M}, B x y = 0 → B y x = 0 := fun {x y} => H x y -#align bilin_form.is_refl.eq_zero BilinForm.IsRefl.eq_zero +#align bilin_form.is_refl.eq_zero LinearMap.BilinForm.IsRefl.eq_zero protected theorem neg {B : BilinForm R₁ M₁} (hB : B.IsRefl) : (-B).IsRefl := fun x y => neg_eq_zero.mpr ∘ hB x y ∘ neg_eq_zero.mp -#align bilin_form.is_refl.neg BilinForm.IsRefl.neg +#align bilin_form.is_refl.neg LinearMap.BilinForm.IsRefl.neg -protected theorem smul {α} [CommSemiring α] [Module α R] [SMulCommClass α R R] +protected theorem smul {α} [CommSemiring α] [Module α R] [SMulCommClass R α R] [NoZeroSMulDivisors α R] (a : α) {B : BilinForm R M} (hB : B.IsRefl) : (a • B).IsRefl := fun _ _ h => (smul_eq_zero.mp h).elim (fun ha => smul_eq_zero_of_left ha _) fun hBz => smul_eq_zero_of_right _ (hB _ _ hBz) -#align bilin_form.is_refl.smul BilinForm.IsRefl.smul +#align bilin_form.is_refl.smul LinearMap.BilinForm.IsRefl.smul -protected theorem groupSMul {α} [Group α] [DistribMulAction α R] [SMulCommClass α R R] (a : α) +protected theorem groupSMul {α} [Group α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : BilinForm R M} (hB : B.IsRefl) : (a • B).IsRefl := fun x y => (smul_eq_zero_iff_eq _).mpr ∘ hB x y ∘ (smul_eq_zero_iff_eq _).mp -#align bilin_form.is_refl.group_smul BilinForm.IsRefl.groupSMul +#align bilin_form.is_refl.group_smul LinearMap.BilinForm.IsRefl.groupSMul end IsRefl @[simp] theorem isRefl_zero : (0 : BilinForm R M).IsRefl := fun _ _ _ => rfl -#align bilin_form.is_refl_zero BilinForm.isRefl_zero +#align bilin_form.is_refl_zero LinearMap.BilinForm.isRefl_zero @[simp] theorem isRefl_neg {B : BilinForm R₁ M₁} : (-B).IsRefl ↔ B.IsRefl := ⟨fun h => neg_neg B ▸ h.neg, IsRefl.neg⟩ -#align bilin_form.is_refl_neg BilinForm.isRefl_neg +#align bilin_form.is_refl_neg LinearMap.BilinForm.isRefl_neg /-- The proposition that a bilinear form is symmetric -/ def IsSymm (B : BilinForm R M) : Prop := ∀ x y : M, B x y = B y x -#align bilin_form.is_symm BilinForm.IsSymm +#align bilin_form.is_symm LinearMap.BilinForm.IsSymm namespace IsSymm @@ -100,99 +104,99 @@ variable (H : B.IsSymm) protected theorem eq (x y : M) : B x y = B y x := H x y -#align bilin_form.is_symm.eq BilinForm.IsSymm.eq +#align bilin_form.is_symm.eq LinearMap.BilinForm.IsSymm.eq theorem isRefl : B.IsRefl := fun x y H1 => H x y ▸ H1 -#align bilin_form.is_symm.is_refl BilinForm.IsSymm.isRefl +#align bilin_form.is_symm.is_refl LinearMap.BilinForm.IsSymm.isRefl protected theorem add {B₁ B₂ : BilinForm R M} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁ + B₂).IsSymm := fun x y => (congr_arg₂ (· + ·) (hB₁ x y) (hB₂ x y) : _) -#align bilin_form.is_symm.add BilinForm.IsSymm.add +#align bilin_form.is_symm.add LinearMap.BilinForm.IsSymm.add protected theorem sub {B₁ B₂ : BilinForm R₁ M₁} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁ - B₂).IsSymm := fun x y => (congr_arg₂ Sub.sub (hB₁ x y) (hB₂ x y) : _) -#align bilin_form.is_symm.sub BilinForm.IsSymm.sub +#align bilin_form.is_symm.sub LinearMap.BilinForm.IsSymm.sub protected theorem neg {B : BilinForm R₁ M₁} (hB : B.IsSymm) : (-B).IsSymm := fun x y => congr_arg Neg.neg (hB x y) -#align bilin_form.is_symm.neg BilinForm.IsSymm.neg +#align bilin_form.is_symm.neg LinearMap.BilinForm.IsSymm.neg -protected theorem smul {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R R] (a : α) +protected theorem smul {α} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : BilinForm R M} (hB : B.IsSymm) : (a • B).IsSymm := fun x y => congr_arg (a • ·) (hB x y) -#align bilin_form.is_symm.smul BilinForm.IsSymm.smul +#align bilin_form.is_symm.smul LinearMap.BilinForm.IsSymm.smul /-- The restriction of a symmetric bilinear form on a submodule is also symmetric. -/ theorem restrict {B : BilinForm R M} (b : B.IsSymm) (W : Submodule R M) : (B.restrict W).IsSymm := fun x y => b x y -#align bilin_form.restrict_symm BilinForm.IsSymm.restrict +#align bilin_form.restrict_symm LinearMap.BilinForm.IsSymm.restrict end IsSymm @[simp] theorem isSymm_zero : (0 : BilinForm R M).IsSymm := fun _ _ => rfl -#align bilin_form.is_symm_zero BilinForm.isSymm_zero +#align bilin_form.is_symm_zero LinearMap.BilinForm.isSymm_zero @[simp] theorem isSymm_neg {B : BilinForm R₁ M₁} : (-B).IsSymm ↔ B.IsSymm := ⟨fun h => neg_neg B ▸ h.neg, IsSymm.neg⟩ -#align bilin_form.is_symm_neg BilinForm.isSymm_neg +#align bilin_form.is_symm_neg LinearMap.BilinForm.isSymm_neg variable (R₂) in theorem isSymm_iff_flip : B.IsSymm ↔ flipHom B = B := (forall₂_congr fun _ _ => by exact eq_comm).trans ext_iff.symm -#align bilin_form.is_symm_iff_flip' BilinForm.isSymm_iff_flip +#align bilin_form.is_symm_iff_flip' LinearMap.BilinForm.isSymm_iff_flip /-- The proposition that a bilinear form is alternating -/ def IsAlt (B : BilinForm R M) : Prop := ∀ x : M, B x x = 0 -#align bilin_form.is_alt BilinForm.IsAlt +#align bilin_form.is_alt LinearMap.BilinForm.IsAlt namespace IsAlt theorem self_eq_zero (H : B.IsAlt) (x : M) : B x x = 0 := H x -#align bilin_form.is_alt.self_eq_zero BilinForm.IsAlt.self_eq_zero +#align bilin_form.is_alt.self_eq_zero LinearMap.BilinForm.IsAlt.self_eq_zero theorem neg_eq (H : B₁.IsAlt) (x y : M₁) : -B₁ x y = B₁ y x := by have H1 : B₁ (x + y) (x + y) = 0 := self_eq_zero H (x + y) rw [add_left, add_right, add_right, self_eq_zero H, self_eq_zero H, zero_add, add_zero, add_eq_zero_iff_neg_eq] at H1 exact H1 -#align bilin_form.is_alt.neg_eq BilinForm.IsAlt.neg_eq +#align bilin_form.is_alt.neg_eq LinearMap.BilinForm.IsAlt.neg_eq theorem isRefl (H : B₁.IsAlt) : B₁.IsRefl := by intro x y h rw [← neg_eq H, h, neg_zero] -#align bilin_form.is_alt.is_refl BilinForm.IsAlt.isRefl +#align bilin_form.is_alt.is_refl LinearMap.BilinForm.IsAlt.isRefl protected theorem add {B₁ B₂ : BilinForm R M} (hB₁ : B₁.IsAlt) (hB₂ : B₂.IsAlt) : (B₁ + B₂).IsAlt := fun x => (congr_arg₂ (· + ·) (hB₁ x) (hB₂ x) : _).trans <| add_zero _ -#align bilin_form.is_alt.add BilinForm.IsAlt.add +#align bilin_form.is_alt.add LinearMap.BilinForm.IsAlt.add protected theorem sub {B₁ B₂ : BilinForm R₁ M₁} (hB₁ : B₁.IsAlt) (hB₂ : B₂.IsAlt) : (B₁ - B₂).IsAlt := fun x => (congr_arg₂ Sub.sub (hB₁ x) (hB₂ x)).trans <| sub_zero _ -#align bilin_form.is_alt.sub BilinForm.IsAlt.sub +#align bilin_form.is_alt.sub LinearMap.BilinForm.IsAlt.sub protected theorem neg {B : BilinForm R₁ M₁} (hB : B.IsAlt) : (-B).IsAlt := fun x => neg_eq_zero.mpr <| hB x -#align bilin_form.is_alt.neg BilinForm.IsAlt.neg +#align bilin_form.is_alt.neg LinearMap.BilinForm.IsAlt.neg -protected theorem smul {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R R] (a : α) +protected theorem smul {α} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : BilinForm R M} (hB : B.IsAlt) : (a • B).IsAlt := fun x => (congr_arg (a • ·) (hB x)).trans <| smul_zero _ -#align bilin_form.is_alt.smul BilinForm.IsAlt.smul +#align bilin_form.is_alt.smul LinearMap.BilinForm.IsAlt.smul end IsAlt @[simp] theorem isAlt_zero : (0 : BilinForm R M).IsAlt := fun _ => rfl -#align bilin_form.is_alt_zero BilinForm.isAlt_zero +#align bilin_form.is_alt_zero LinearMap.BilinForm.isAlt_zero @[simp] theorem isAlt_neg {B : BilinForm R₁ M₁} : (-B).IsAlt ↔ B.IsAlt := ⟨fun h => neg_neg B ▸ h.neg, IsAlt.neg⟩ -#align bilin_form.is_alt_neg BilinForm.isAlt_neg +#align bilin_form.is_alt_neg LinearMap.BilinForm.isAlt_neg /-! ### Linear adjoints -/ @@ -207,13 +211,13 @@ variable (B' : BilinForm R M') (f f' : M →ₗ[R] M') (g g' : M' →ₗ[R] M) maps between them to be mutually adjoint. -/ def IsAdjointPair := ∀ ⦃x y⦄, B' (f x) y = B x (g y) -#align bilin_form.is_adjoint_pair BilinForm.IsAdjointPair +#align bilin_form.is_adjoint_pair LinearMap.BilinForm.IsAdjointPair variable {B B' f f' g g'} theorem IsAdjointPair.eq (h : IsAdjointPair B B' f g) : ∀ {x y}, B' (f x) y = B x (g y) := @h -#align bilin_form.is_adjoint_pair.eq BilinForm.IsAdjointPair.eq +#align bilin_form.is_adjoint_pair.eq LinearMap.BilinForm.IsAdjointPair.eq theorem isAdjointPair_iff_compLeft_eq_compRight (f g : Module.End R M) : IsAdjointPair B F f g ↔ F.compLeft f = B.compRight g := by @@ -224,19 +228,19 @@ theorem isAdjointPair_iff_compLeft_eq_compRight (f g : Module.End R M) : · intro x y rw [← compLeft_apply, ← compRight_apply] rw [h] -#align bilin_form.is_adjoint_pair_iff_comp_left_eq_comp_right BilinForm.isAdjointPair_iff_compLeft_eq_compRight +#align bilin_form.is_adjoint_pair_iff_comp_left_eq_comp_right LinearMap.BilinForm.isAdjointPair_iff_compLeft_eq_compRight theorem isAdjointPair_zero : IsAdjointPair B B' 0 0 := fun x y => by simp only [BilinForm.zero_left, BilinForm.zero_right, LinearMap.zero_apply] -#align bilin_form.is_adjoint_pair_zero BilinForm.isAdjointPair_zero +#align bilin_form.is_adjoint_pair_zero LinearMap.BilinForm.isAdjointPair_zero theorem isAdjointPair_id : IsAdjointPair B B 1 1 := fun _ _ => rfl -#align bilin_form.is_adjoint_pair_id BilinForm.isAdjointPair_id +#align bilin_form.is_adjoint_pair_id LinearMap.BilinForm.isAdjointPair_id theorem IsAdjointPair.add (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B B' f' g') : IsAdjointPair B B' (f + f') (g + g') := fun x y => by rw [LinearMap.add_apply, LinearMap.add_apply, add_left, add_right, h, h'] -#align bilin_form.is_adjoint_pair.add BilinForm.IsAdjointPair.add +#align bilin_form.is_adjoint_pair.add LinearMap.BilinForm.IsAdjointPair.add variable {M₁' : Type*} [AddCommGroup M₁'] [Module R₁ M₁'] variable {B₁' : BilinForm R₁ M₁'} {f₁ f₁' : M₁ →ₗ[R₁] M₁'} {g₁ g₁' : M₁' →ₗ[R₁] M₁} @@ -244,14 +248,14 @@ variable {B₁' : BilinForm R₁ M₁'} {f₁ f₁' : M₁ →ₗ[R₁] M₁'} { theorem IsAdjointPair.sub (h : IsAdjointPair B₁ B₁' f₁ g₁) (h' : IsAdjointPair B₁ B₁' f₁' g₁') : IsAdjointPair B₁ B₁' (f₁ - f₁') (g₁ - g₁') := fun x y => by rw [LinearMap.sub_apply, LinearMap.sub_apply, sub_left, sub_right, h, h'] -#align bilin_form.is_adjoint_pair.sub BilinForm.IsAdjointPair.sub +#align bilin_form.is_adjoint_pair.sub LinearMap.BilinForm.IsAdjointPair.sub variable {B₂' : BilinForm R M'} {f₂ f₂' : M →ₗ[R] M'} {g₂ g₂' : M' →ₗ[R] M} theorem IsAdjointPair.smul (c : R) (h : IsAdjointPair B B₂' f₂ g₂) : IsAdjointPair B B₂' (c • f₂) (c • g₂) := fun x y => by rw [LinearMap.smul_apply, LinearMap.smul_apply, smul_left, smul_right, h] -#align bilin_form.is_adjoint_pair.smul BilinForm.IsAdjointPair.smul +#align bilin_form.is_adjoint_pair.smul LinearMap.BilinForm.IsAdjointPair.smul variable {M'' : Type*} [AddCommMonoid M''] [Module R M''] variable (B'' : BilinForm R M'') @@ -259,12 +263,12 @@ variable (B'' : BilinForm R M'') theorem IsAdjointPair.comp {f' : M' →ₗ[R] M''} {g' : M'' →ₗ[R] M'} (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B' B'' f' g') : IsAdjointPair B B'' (f'.comp f) (g.comp g') := fun x y => by rw [LinearMap.comp_apply, LinearMap.comp_apply, h', h] -#align bilin_form.is_adjoint_pair.comp BilinForm.IsAdjointPair.comp +#align bilin_form.is_adjoint_pair.comp LinearMap.BilinForm.IsAdjointPair.comp theorem IsAdjointPair.mul {f g f' g' : Module.End R M} (h : IsAdjointPair B B f g) (h' : IsAdjointPair B B f' g') : IsAdjointPair B B (f * f') (g' * g) := fun x y => by rw [LinearMap.mul_apply, LinearMap.mul_apply, h, h'] -#align bilin_form.is_adjoint_pair.mul BilinForm.IsAdjointPair.mul +#align bilin_form.is_adjoint_pair.mul LinearMap.BilinForm.IsAdjointPair.mul variable (B B' B₁ B₂) (F₂ : BilinForm R M) @@ -274,7 +278,7 @@ of self adjointness. In the case that one of the forms is the negation of the ot usual concept of skew adjointness. -/ def IsPairSelfAdjoint (f : Module.End R M) := IsAdjointPair B F f f -#align bilin_form.is_pair_self_adjoint BilinForm.IsPairSelfAdjoint +#align bilin_form.is_pair_self_adjoint LinearMap.BilinForm.IsPairSelfAdjoint /-- The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms. -/ def isPairSelfAdjointSubmodule : Submodule R (Module.End R M) where @@ -282,12 +286,12 @@ def isPairSelfAdjointSubmodule : Submodule R (Module.End R M) where zero_mem' := isAdjointPair_zero add_mem' hf hg := hf.add hg smul_mem' c _ h := h.smul c -#align bilin_form.is_pair_self_adjoint_submodule BilinForm.isPairSelfAdjointSubmodule +#align bilin_form.is_pair_self_adjoint_submodule LinearMap.BilinForm.isPairSelfAdjointSubmodule @[simp] theorem mem_isPairSelfAdjointSubmodule (f : Module.End R M) : f ∈ isPairSelfAdjointSubmodule B₂ F₂ ↔ IsPairSelfAdjoint B₂ F₂ f := Iff.rfl -#align bilin_form.mem_is_pair_self_adjoint_submodule BilinForm.mem_isPairSelfAdjointSubmodule +#align bilin_form.mem_is_pair_self_adjoint_submodule LinearMap.BilinForm.mem_isPairSelfAdjointSubmodule theorem isPairSelfAdjoint_equiv (e : M' ≃ₗ[R] M) (f : Module.End R M) : IsPairSelfAdjoint B₂ F₂ f ↔ @@ -302,50 +306,50 @@ theorem isPairSelfAdjoint_equiv (e : M' ≃ₗ[R] M) (f : Module.End R M) : show BilinForm.IsAdjointPair _ _ _ _ ↔ BilinForm.IsAdjointPair _ _ _ _ rw [isAdjointPair_iff_compLeft_eq_compRight, isAdjointPair_iff_compLeft_eq_compRight, hᵣ, hₗ, comp_inj _ _ he he] -#align bilin_form.is_pair_self_adjoint_equiv BilinForm.isPairSelfAdjoint_equiv +#align bilin_form.is_pair_self_adjoint_equiv LinearMap.BilinForm.isPairSelfAdjoint_equiv /-- An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an adjoint for itself. -/ def IsSelfAdjoint (f : Module.End R M) := IsAdjointPair B B f f -#align bilin_form.is_self_adjoint BilinForm.IsSelfAdjoint +#align bilin_form.is_self_adjoint LinearMap.BilinForm.IsSelfAdjoint /-- An endomorphism of a module is skew-adjoint with respect to a bilinear form if its negation serves as an adjoint. -/ def IsSkewAdjoint (f : Module.End R₁ M₁) := IsAdjointPair B₁ B₁ f (-f) -#align bilin_form.is_skew_adjoint BilinForm.IsSkewAdjoint +#align bilin_form.is_skew_adjoint LinearMap.BilinForm.IsSkewAdjoint theorem isSkewAdjoint_iff_neg_self_adjoint (f : Module.End R₁ M₁) : B₁.IsSkewAdjoint f ↔ IsAdjointPair (-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 only [LinearMap.neg_apply, BilinForm.neg_apply, BilinForm.neg_right] -#align bilin_form.is_skew_adjoint_iff_neg_self_adjoint BilinForm.isSkewAdjoint_iff_neg_self_adjoint +#align bilin_form.is_skew_adjoint_iff_neg_self_adjoint LinearMap.BilinForm.isSkewAdjoint_iff_neg_self_adjoint /-- The set of self-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Jordan subalgebra.) -/ def selfAdjointSubmodule := isPairSelfAdjointSubmodule B B -#align bilin_form.self_adjoint_submodule BilinForm.selfAdjointSubmodule +#align bilin_form.self_adjoint_submodule LinearMap.BilinForm.selfAdjointSubmodule @[simp] theorem mem_selfAdjointSubmodule (f : Module.End R M) : f ∈ B.selfAdjointSubmodule ↔ B.IsSelfAdjoint f := Iff.rfl -#align bilin_form.mem_self_adjoint_submodule BilinForm.mem_selfAdjointSubmodule +#align bilin_form.mem_self_adjoint_submodule LinearMap.BilinForm.mem_selfAdjointSubmodule /-- The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Lie subalgebra.) -/ def skewAdjointSubmodule := isPairSelfAdjointSubmodule (-B₁) B₁ -#align bilin_form.skew_adjoint_submodule BilinForm.skewAdjointSubmodule +#align bilin_form.skew_adjoint_submodule LinearMap.BilinForm.skewAdjointSubmodule @[simp] theorem mem_skewAdjointSubmodule (f : Module.End R₁ M₁) : f ∈ B₁.skewAdjointSubmodule ↔ B₁.IsSkewAdjoint f := by rw [isSkewAdjoint_iff_neg_self_adjoint] exact Iff.rfl -#align bilin_form.mem_skew_adjoint_submodule BilinForm.mem_skewAdjointSubmodule +#align bilin_form.mem_skew_adjoint_submodule LinearMap.BilinForm.mem_skewAdjointSubmodule end LinearAdjoints @@ -363,7 +367,7 @@ nondegeneracy condition that in the situation described, `B n m ≠ 0`. This va not currently provided in mathlib. In finite dimension either definition implies the other. -/ def Nondegenerate (B : BilinForm R M) : Prop := ∀ m : M, (∀ n : M, B m n = 0) → m = 0 -#align bilin_form.nondegenerate BilinForm.Nondegenerate +#align bilin_form.nondegenerate LinearMap.BilinForm.Nondegenerate section @@ -373,7 +377,7 @@ variable (R M) theorem not_nondegenerate_zero [Nontrivial M] : ¬(0 : BilinForm R M).Nondegenerate := let ⟨m, hm⟩ := exists_ne (0 : M) fun h => hm (h m fun _ => rfl) -#align bilin_form.not_nondegenerate_zero BilinForm.not_nondegenerate_zero +#align bilin_form.not_nondegenerate_zero LinearMap.BilinForm.not_nondegenerate_zero end @@ -382,13 +386,13 @@ variable [AddCommMonoid M'] [Module R M'] theorem Nondegenerate.ne_zero [Nontrivial M] {B : BilinForm R M} (h : B.Nondegenerate) : B ≠ 0 := fun h0 => not_nondegenerate_zero R M <| h0 ▸ h -#align bilin_form.nondegenerate.ne_zero BilinForm.Nondegenerate.ne_zero +#align bilin_form.nondegenerate.ne_zero LinearMap.BilinForm.Nondegenerate.ne_zero theorem Nondegenerate.congr {B : BilinForm R M} (e : M ≃ₗ[R] M') (h : B.Nondegenerate) : (congr e B).Nondegenerate := fun m hm => e.symm.map_eq_zero_iff.1 <| h (e.symm m) fun n => (congr_arg _ (e.symm_apply_apply n).symm).trans (hm (e n)) -#align bilin_form.nondegenerate.congr BilinForm.Nondegenerate.congr +#align bilin_form.nondegenerate.congr LinearMap.BilinForm.Nondegenerate.congr @[simp] theorem nondegenerate_congr_iff {B : BilinForm R M} (e : M ≃ₗ[R] M') : @@ -396,26 +400,26 @@ theorem nondegenerate_congr_iff {B : BilinForm R M} (e : M ≃ₗ[R] M') : ⟨fun h => by convert h.congr e.symm rw [congr_congr, e.self_trans_symm, congr_refl, LinearEquiv.refl_apply], Nondegenerate.congr e⟩ -#align bilin_form.nondegenerate_congr_iff BilinForm.nondegenerate_congr_iff +#align bilin_form.nondegenerate_congr_iff LinearMap.BilinForm.nondegenerate_congr_iff /-- A bilinear form is nondegenerate if and only if it has a trivial kernel. -/ theorem nondegenerate_iff_ker_eq_bot {B : BilinForm R M} : - B.Nondegenerate ↔ LinearMap.ker (BilinForm.toLin B) = ⊥ := by + B.Nondegenerate ↔ LinearMap.ker B = ⊥ := by rw [LinearMap.ker_eq_bot'] constructor <;> intro h · refine' fun m hm => h _ fun x => _ - rw [← toLin_apply, hm] + rw [hm] rfl · intro m hm apply h ext x exact hm x -#align bilin_form.nondegenerate_iff_ker_eq_bot BilinForm.nondegenerate_iff_ker_eq_bot +#align bilin_form.nondegenerate_iff_ker_eq_bot LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot theorem Nondegenerate.ker_eq_bot {B : BilinForm R M} (h : B.Nondegenerate) : LinearMap.ker (BilinForm.toLin B) = ⊥ := nondegenerate_iff_ker_eq_bot.mp h -#align bilin_form.nondegenerate.ker_eq_bot BilinForm.Nondegenerate.ker_eq_bot +#align bilin_form.nondegenerate.ker_eq_bot LinearMap.BilinForm.Nondegenerate.ker_eq_bot theorem compLeft_injective (B : BilinForm R₁ M₁) (b : B.Nondegenerate) : Function.Injective B.compLeft := fun φ ψ h => by @@ -423,13 +427,13 @@ theorem compLeft_injective (B : BilinForm R₁ M₁) (b : B.Nondegenerate) : refine' eq_of_sub_eq_zero (b _ _) intro v rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self] -#align bilin_form.comp_left_injective BilinForm.compLeft_injective +#align bilin_form.comp_left_injective LinearMap.BilinForm.compLeft_injective theorem isAdjointPair_unique_of_nondegenerate (B : BilinForm R₁ M₁) (b : B.Nondegenerate) (φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁) (hψ₁ : IsAdjointPair B B ψ₁ φ) (hψ₂ : IsAdjointPair B B ψ₂ φ) : ψ₁ = ψ₂ := B.compLeft_injective b <| ext fun v w => by rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂] -#align bilin_form.is_adjoint_pair_unique_of_nondegenerate BilinForm.isAdjointPair_unique_of_nondegenerate +#align bilin_form.is_adjoint_pair_unique_of_nondegenerate LinearMap.BilinForm.isAdjointPair_unique_of_nondegenerate section FiniteDimensional @@ -439,13 +443,13 @@ variable [FiniteDimensional K V] the linear equivalence between a vector space and its dual with the underlying linear map `B.toLin`. -/ noncomputable def toDual (B : BilinForm K V) (b : B.Nondegenerate) : V ≃ₗ[K] Module.Dual K V := - B.toLin.linearEquivOfInjective (LinearMap.ker_eq_bot.mp <| b.ker_eq_bot) + B.linearEquivOfInjective (LinearMap.ker_eq_bot.mp <| b.ker_eq_bot) Subspace.dual_finrank_eq.symm -#align bilin_form.to_dual BilinForm.toDual +#align bilin_form.to_dual LinearMap.BilinForm.toDual -theorem toDual_def {B : BilinForm K V} (b : B.Nondegenerate) {m n : V} : B.toDual b m n = B m n := +theorem toDual_def {B : BilinForm K V} (b : B.SeparatingLeft) {m n : V} : B.toDual b m n = B m n := rfl -#align bilin_form.to_dual_def BilinForm.toDual_def +#align bilin_form.to_dual_def LinearMap.BilinForm.toDual_def lemma Nondegenerate.flip {B : BilinForm K V} (hB : B.Nondegenerate) : B.flip.Nondegenerate := by @@ -469,26 +473,26 @@ noncomputable def dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basi Basis ι K V := haveI := FiniteDimensional.of_fintype_basis b b.dualBasis.map (B.toDual hB).symm -#align bilin_form.dual_basis BilinForm.dualBasis +#align bilin_form.dual_basis LinearMap.BilinForm.dualBasis @[simp] theorem dualBasis_repr_apply (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) (x i) : (B.dualBasis hB b).repr x i = B x (b i) := by rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply, Basis.dualBasis_repr, toDual_def] -#align bilin_form.dual_basis_repr_apply BilinForm.dualBasis_repr_apply +#align bilin_form.dual_basis_repr_apply LinearMap.BilinForm.dualBasis_repr_apply theorem apply_dualBasis_left (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) (i j) : B (B.dualBasis hB b i) (b j) = if j = i then 1 else 0 := by have := FiniteDimensional.of_fintype_basis b rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB, LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply] -#align bilin_form.apply_dual_basis_left BilinForm.apply_dualBasis_left +#align bilin_form.apply_dual_basis_left LinearMap.BilinForm.apply_dualBasis_left theorem apply_dualBasis_right (B : BilinForm K V) (hB : B.Nondegenerate) (sym : B.IsSymm) (b : Basis ι K V) (i j) : B (b i) (B.dualBasis hB b j) = if i = j then 1 else 0 := by rw [sym, apply_dualBasis_left] -#align bilin_form.apply_dual_basis_right BilinForm.apply_dualBasis_right +#align bilin_form.apply_dual_basis_right LinearMap.BilinForm.apply_dualBasis_right @[simp] lemma dualBasis_dualBasis_flip (B : BilinForm K V) (hB : B.Nondegenerate) {ι} @@ -496,9 +500,8 @@ lemma dualBasis_dualBasis_flip (B : BilinForm K V) (hB : B.Nondegenerate) {ι} B.dualBasis hB (B.flip.dualBasis hB.flip b) = b := by ext i refine LinearMap.ker_eq_bot.mp hB.ker_eq_bot ((B.flip.dualBasis hB.flip b).ext (fun j ↦ ?_)) - rw [toLin_apply, apply_dualBasis_left, toLin_apply, ← B.flip_apply, - apply_dualBasis_left] - simp_rw [@eq_comm _ i j] + simp_rw [BilinForm.toLin_apply, apply_dualBasis_left, ← B.flip_apply, + apply_dualBasis_left, @eq_comm _ i j] @[simp] lemma dualBasis_flip_dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) {ι} @@ -522,19 +525,22 @@ is the linear map `B₂.toLin⁻¹ ∘ B₁.toLin`. -/ noncomputable def symmCompOfNondegenerate (B₁ B₂ : BilinForm K V) (b₂ : B₂.Nondegenerate) : V →ₗ[K] V := (B₂.toDual b₂).symm.toLinearMap.comp (BilinForm.toLin B₁) -#align bilin_form.symm_comp_of_nondegenerate BilinForm.symmCompOfNondegenerate +#align bilin_form.symm_comp_of_nondegenerate LinearMap.BilinForm.symmCompOfNondegenerate theorem comp_symmCompOfNondegenerate_apply (B₁ : BilinForm K V) {B₂ : BilinForm K V} (b₂ : B₂.Nondegenerate) (v : V) : - toLin B₂ (B₁.symmCompOfNondegenerate B₂ b₂ v) = toLin B₁ v := by - erw [symmCompOfNondegenerate, LinearEquiv.apply_symm_apply (B₂.toDual b₂) _] -#align bilin_form.comp_symm_comp_of_nondegenerate_apply BilinForm.comp_symmCompOfNondegenerate_apply + B₂ (B₁.symmCompOfNondegenerate B₂ b₂ v) = B₁ v := by + erw [symmCompOfNondegenerate] + simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, DFunLike.coe_fn_eq] + erw [LinearEquiv.apply_symm_apply (B₂.toDual b₂)] + rfl +#align bilin_form.comp_symm_comp_of_nondegenerate_apply LinearMap.BilinForm.comp_symmCompOfNondegenerate_apply @[simp] theorem symmCompOfNondegenerate_left_apply (B₁ : BilinForm K V) {B₂ : BilinForm K V} (b₂ : B₂.Nondegenerate) (v w : V) : B₂ (symmCompOfNondegenerate B₁ B₂ b₂ w) v = B₁ w v := by - conv_lhs => rw [← BilinForm.toLin_apply, comp_symmCompOfNondegenerate_apply] -#align bilin_form.symm_comp_of_nondegenerate_left_apply BilinForm.symmCompOfNondegenerate_left_apply + conv_lhs => rw [comp_symmCompOfNondegenerate_apply] +#align bilin_form.symm_comp_of_nondegenerate_left_apply LinearMap.BilinForm.symmCompOfNondegenerate_left_apply /-- Given the nondegenerate bilinear form `B` and the linear map `φ`, `leftAdjointOfNondegenerate` provides the left adjoint of `φ` with respect to `B`. @@ -542,12 +548,12 @@ The lemma proving this property is `BilinForm.isAdjointPairLeftAdjointOfNondegen noncomputable def leftAdjointOfNondegenerate (B : BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V) : V →ₗ[K] V := symmCompOfNondegenerate (B.compRight φ) B b -#align bilin_form.left_adjoint_of_nondegenerate BilinForm.leftAdjointOfNondegenerate +#align bilin_form.left_adjoint_of_nondegenerate LinearMap.BilinForm.leftAdjointOfNondegenerate theorem isAdjointPairLeftAdjointOfNondegenerate (B : BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V) : IsAdjointPair B B (B.leftAdjointOfNondegenerate b φ) φ := fun x y => (B.compRight φ).symmCompOfNondegenerate_left_apply b y x -#align bilin_form.is_adjoint_pair_left_adjoint_of_nondegenerate BilinForm.isAdjointPairLeftAdjointOfNondegenerate +#align bilin_form.is_adjoint_pair_left_adjoint_of_nondegenerate LinearMap.BilinForm.isAdjointPairLeftAdjointOfNondegenerate /-- Given the nondegenerate bilinear form `B`, the linear map `φ` has a unique left adjoint given by `BilinForm.leftAdjointOfNondegenerate`. -/ @@ -557,10 +563,12 @@ theorem isAdjointPair_iff_eq_of_nondegenerate (B : BilinForm K V) (b : B.Nondege B.isAdjointPair_unique_of_nondegenerate b φ ψ _ h (isAdjointPairLeftAdjointOfNondegenerate _ _ _), fun h => h.symm ▸ isAdjointPairLeftAdjointOfNondegenerate _ _ _⟩ -#align bilin_form.is_adjoint_pair_iff_eq_of_nondegenerate BilinForm.isAdjointPair_iff_eq_of_nondegenerate +#align bilin_form.is_adjoint_pair_iff_eq_of_nondegenerate LinearMap.BilinForm.isAdjointPair_iff_eq_of_nondegenerate end LinearAdjoints end FiniteDimensional end BilinForm + +end LinearMap diff --git a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean index 79d3c20d7c17ce..1d6478eb0937d1 100644 --- a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean +++ b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean @@ -39,6 +39,7 @@ bilinear form, bilin form, BilinearForm, matrix, basis -/ +open LinearMap (BilinForm) variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] @@ -53,7 +54,7 @@ variable {n o : Type*} open BigOperators -open BilinForm Finset LinearMap Matrix +open Finset LinearMap Matrix open Matrix @@ -78,11 +79,11 @@ def BilinForm.toMatrixAux (b : n → M₂) : BilinForm R₂ M₂ →ₗ[R₂] Ma #align bilin_form.to_matrix_aux BilinForm.toMatrixAux @[simp] -theorem BilinForm.toMatrixAux_apply (B : BilinForm R₂ M₂) (b : n → M₂) (i j : n) : +theorem LinearMap.BilinForm.toMatrixAux_apply (B : BilinForm R₂ M₂) (b : n → M₂) (i j : n) : -- Porting note: had to hint the base ring even though it should be clear from context... BilinForm.toMatrixAux (R₂ := R₂) b B i j = B (b i) (b j) := - LinearMap.toMatrix₂Aux_apply (toLin B) _ _ _ _ -#align bilin_form.to_matrix_aux_apply BilinForm.toMatrixAux_apply + LinearMap.toMatrix₂Aux_apply B _ _ _ _ +#align bilin_form.to_matrix_aux_apply LinearMap.BilinForm.toMatrixAux_apply variable [Fintype n] [Fintype o] @@ -93,7 +94,8 @@ theorem toBilin'Aux_toMatrixAux [DecidableEq n] (B₂ : BilinForm R₂ (n → R rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux, coe_comp, Function.comp_apply, toLinearMap₂'Aux_toMatrix₂Aux] ext x y - simp only [toBilin_apply, BilinForm.toLin'_apply] + simp only [coe_comp, coe_single, Function.comp_apply, toBilin_apply] + rfl #align to_bilin'_aux_to_matrix_aux toBilin'Aux_toMatrixAux section ToMatrix' @@ -107,17 +109,17 @@ This section deals with the conversion between matrices and bilinear forms on `n variable [DecidableEq n] [DecidableEq o] /-- The linear equivalence between bilinear forms on `n → R` and `n × n` matrices -/ -def BilinForm.toMatrix' : BilinForm R₂ (n → R₂) ≃ₗ[R₂] Matrix n n R₂ := - BilinForm.toLin ≪≫ₗ LinearMap.toMatrix₂' -#align bilin_form.to_matrix' BilinForm.toMatrix' +def LinearMap.BilinForm.toMatrix' : BilinForm R₂ (n → R₂) ≃ₗ[R₂] Matrix n n R₂ := + LinearMap.toMatrix₂' +#align bilin_form.to_matrix' LinearMap.BilinForm.toMatrix' @[simp] -theorem BilinForm.toMatrixAux_stdBasis (B : BilinForm R₂ (n → R₂)) : +theorem LinearMap.BilinForm.toMatrixAux_stdBasis (B : BilinForm R₂ (n → R₂)) : -- Porting note: had to hint the base ring even though it should be clear from context... BilinForm.toMatrixAux (R₂ := R₂) (fun j => stdBasis R₂ (fun _ => R₂) j 1) B = BilinForm.toMatrix' B := rfl -#align bilin_form.to_matrix_aux_std_basis BilinForm.toMatrixAux_stdBasis +#align bilin_form.to_matrix_aux_std_basis LinearMap.BilinForm.toMatrixAux_stdBasis /-- The linear equivalence between `n × n` matrices and bilinear forms on `n → R` -/ def Matrix.toBilin' : Matrix n n R₂ ≃ₗ[R₂] BilinForm R₂ (n → R₂) := @@ -145,10 +147,10 @@ theorem Matrix.toBilin'_stdBasis (M : Matrix n n R₂) (i j : n) : #align matrix.to_bilin'_std_basis Matrix.toBilin'_stdBasis @[simp] -theorem BilinForm.toMatrix'_symm : +theorem LinearMap.BilinForm.toMatrix'_symm : (BilinForm.toMatrix'.symm : Matrix n n R₂ ≃ₗ[R₂] _) = Matrix.toBilin' := rfl -#align bilin_form.to_matrix'_symm BilinForm.toMatrix'_symm +#align bilin_form.to_matrix'_symm LinearMap.BilinForm.toMatrix'_symm @[simp] theorem Matrix.toBilin'_symm : @@ -162,51 +164,55 @@ theorem Matrix.toBilin'_toMatrix' (B : BilinForm R₂ (n → R₂)) : Matrix.toBilin'.apply_symm_apply B #align matrix.to_bilin'_to_matrix' Matrix.toBilin'_toMatrix' +namespace LinearMap + @[simp] theorem BilinForm.toMatrix'_toBilin' (M : Matrix n n R₂) : BilinForm.toMatrix' (Matrix.toBilin' M) = M := LinearMap.toMatrix₂'.apply_symm_apply M -#align bilin_form.to_matrix'_to_bilin' BilinForm.toMatrix'_toBilin' +#align bilin_form.to_matrix'_to_bilin' LinearMap.BilinForm.toMatrix'_toBilin' @[simp] theorem BilinForm.toMatrix'_apply (B : BilinForm R₂ (n → R₂)) (i j : n) : BilinForm.toMatrix' B i j = B (stdBasis R₂ (fun _ => R₂) i 1) (stdBasis R₂ (fun _ => R₂) j 1) := LinearMap.toMatrix₂'_apply _ _ _ -#align bilin_form.to_matrix'_apply BilinForm.toMatrix'_apply +#align bilin_form.to_matrix'_apply LinearMap.BilinForm.toMatrix'_apply -- Porting note: dot notation for bundled maps doesn't work in the rest of this section @[simp] theorem BilinForm.toMatrix'_comp (B : BilinForm R₂ (n → R₂)) (l r : (o → R₂) →ₗ[R₂] n → R₂) : BilinForm.toMatrix' (B.comp l r) = (LinearMap.toMatrix' l)ᵀ * BilinForm.toMatrix' B * LinearMap.toMatrix' r := - LinearMap.toMatrix₂'_compl₁₂ (toLin B) _ _ -#align bilin_form.to_matrix'_comp BilinForm.toMatrix'_comp + LinearMap.toMatrix₂'_compl₁₂ B _ _ +#align bilin_form.to_matrix'_comp LinearMap.BilinForm.toMatrix'_comp theorem BilinForm.toMatrix'_compLeft (B : BilinForm R₂ (n → R₂)) (f : (n → R₂) →ₗ[R₂] n → R₂) : BilinForm.toMatrix' (B.compLeft f) = (LinearMap.toMatrix' f)ᵀ * BilinForm.toMatrix' B := - LinearMap.toMatrix₂'_comp (toLin B) _ -#align bilin_form.to_matrix'_comp_left BilinForm.toMatrix'_compLeft + LinearMap.toMatrix₂'_comp B _ +#align bilin_form.to_matrix'_comp_left LinearMap.BilinForm.toMatrix'_compLeft theorem BilinForm.toMatrix'_compRight (B : BilinForm R₂ (n → R₂)) (f : (n → R₂) →ₗ[R₂] n → R₂) : BilinForm.toMatrix' (B.compRight f) = BilinForm.toMatrix' B * LinearMap.toMatrix' f := - LinearMap.toMatrix₂'_compl₂ (toLin B) _ -#align bilin_form.to_matrix'_comp_right BilinForm.toMatrix'_compRight + LinearMap.toMatrix₂'_compl₂ B _ +#align bilin_form.to_matrix'_comp_right LinearMap.BilinForm.toMatrix'_compRight theorem BilinForm.mul_toMatrix'_mul (B : BilinForm R₂ (n → R₂)) (M : Matrix o n R₂) (N : Matrix n o R₂) : M * BilinForm.toMatrix' B * N = BilinForm.toMatrix' (B.comp (Matrix.toLin' Mᵀ) (Matrix.toLin' N)) := - LinearMap.mul_toMatrix₂'_mul (toLin B) _ _ -#align bilin_form.mul_to_matrix'_mul BilinForm.mul_toMatrix'_mul + LinearMap.mul_toMatrix₂'_mul B _ _ +#align bilin_form.mul_to_matrix'_mul LinearMap.BilinForm.mul_toMatrix'_mul theorem BilinForm.mul_toMatrix' (B : BilinForm R₂ (n → R₂)) (M : Matrix n n R₂) : M * BilinForm.toMatrix' B = BilinForm.toMatrix' (B.compLeft (Matrix.toLin' Mᵀ)) := - LinearMap.mul_toMatrix' (toLin B) _ -#align bilin_form.mul_to_matrix' BilinForm.mul_toMatrix' + LinearMap.mul_toMatrix' B _ +#align bilin_form.mul_to_matrix' LinearMap.BilinForm.mul_toMatrix' theorem BilinForm.toMatrix'_mul (B : BilinForm R₂ (n → R₂)) (M : Matrix n n R₂) : BilinForm.toMatrix' B * M = BilinForm.toMatrix' (B.compRight (Matrix.toLin' M)) := - LinearMap.toMatrix₂'_mul (toLin B) _ -#align bilin_form.to_matrix'_mul BilinForm.toMatrix'_mul + LinearMap.toMatrix₂'_mul B _ +#align bilin_form.to_matrix'_mul LinearMap.BilinForm.toMatrix'_mul + +end LinearMap theorem Matrix.toBilin'_comp (M : Matrix n n R₂) (P Q : Matrix n o R₂) : M.toBilin'.comp (Matrix.toLin' P) (Matrix.toLin' Q) = Matrix.toBilin' (Pᵀ * M * Q) := @@ -242,7 +248,7 @@ noncomputable def Matrix.toBilin : Matrix n n R₂ ≃ₗ[R₂] BilinForm R₂ M @[simp] theorem BilinForm.toMatrix_apply (B : BilinForm R₂ M₂) (i j : n) : BilinForm.toMatrix b B i j = B (b i) (b j) := - LinearMap.toMatrix₂_apply _ _ (toLin B) _ _ + LinearMap.toMatrix₂_apply _ _ B _ _ #align bilin_form.to_matrix_apply BilinForm.toMatrix_apply @[simp] @@ -254,7 +260,7 @@ theorem Matrix.toBilin_apply (M : Matrix n n R₂) (x y : M₂) : -- Not a `simp` lemma since `BilinForm.toMatrix` needs an extra argument theorem BilinearForm.toMatrixAux_eq (B : BilinForm R₂ M₂) : BilinForm.toMatrixAux (R₂ := R₂) b B = BilinForm.toMatrix b B := - LinearMap.toMatrix₂Aux_eq _ _ (toLin B) + LinearMap.toMatrix₂Aux_eq _ _ B #align bilinear_form.to_matrix_aux_eq BilinearForm.toMatrixAux_eq @[simp] @@ -269,12 +275,14 @@ theorem Matrix.toBilin_symm : (Matrix.toBilin b).symm = BilinForm.toMatrix b := theorem Matrix.toBilin_basisFun : Matrix.toBilin (Pi.basisFun R₂ n) = Matrix.toBilin' := by ext M - simp only [Matrix.toBilin_apply, Matrix.toBilin'_apply, Pi.basisFun_repr] + simp only [coe_comp, coe_single, Function.comp_apply, toBilin_apply, Pi.basisFun_repr, + toBilin'_apply] #align matrix.to_bilin_basis_fun Matrix.toBilin_basisFun theorem BilinForm.toMatrix_basisFun : BilinForm.toMatrix (Pi.basisFun R₂ n) = BilinForm.toMatrix' := by rw [BilinForm.toMatrix, BilinForm.toMatrix', LinearMap.toMatrix₂_basisFun] + rfl #align bilin_form.to_matrix_basis_fun BilinForm.toMatrix_basisFun @[simp] @@ -297,39 +305,39 @@ variable [DecidableEq o] theorem BilinForm.toMatrix_comp (B : BilinForm R₂ M₂) (l r : M₂' →ₗ[R₂] M₂) : BilinForm.toMatrix c (B.comp l r) = (LinearMap.toMatrix c b l)ᵀ * BilinForm.toMatrix b B * LinearMap.toMatrix c b r := - LinearMap.toMatrix₂_compl₁₂ _ _ _ _ (toLin B) _ _ + LinearMap.toMatrix₂_compl₁₂ _ _ _ _ B _ _ #align bilin_form.to_matrix_comp BilinForm.toMatrix_comp theorem BilinForm.toMatrix_compLeft (B : BilinForm R₂ M₂) (f : M₂ →ₗ[R₂] M₂) : BilinForm.toMatrix b (B.compLeft f) = (LinearMap.toMatrix b b f)ᵀ * BilinForm.toMatrix b B := - LinearMap.toMatrix₂_comp _ _ _ (toLin B) _ + LinearMap.toMatrix₂_comp _ _ _ B _ #align bilin_form.to_matrix_comp_left BilinForm.toMatrix_compLeft theorem BilinForm.toMatrix_compRight (B : BilinForm R₂ M₂) (f : M₂ →ₗ[R₂] M₂) : BilinForm.toMatrix b (B.compRight f) = BilinForm.toMatrix b B * LinearMap.toMatrix b b f := - LinearMap.toMatrix₂_compl₂ _ _ _ (toLin B) _ + LinearMap.toMatrix₂_compl₂ _ _ _ B _ #align bilin_form.to_matrix_comp_right BilinForm.toMatrix_compRight @[simp] theorem BilinForm.toMatrix_mul_basis_toMatrix (c : Basis o R₂ M₂) (B : BilinForm R₂ M₂) : (b.toMatrix c)ᵀ * BilinForm.toMatrix b B * b.toMatrix c = BilinForm.toMatrix c B := - LinearMap.toMatrix₂_mul_basis_toMatrix _ _ _ _ (toLin B) + LinearMap.toMatrix₂_mul_basis_toMatrix _ _ _ _ B #align bilin_form.to_matrix_mul_basis_to_matrix BilinForm.toMatrix_mul_basis_toMatrix theorem BilinForm.mul_toMatrix_mul (B : BilinForm R₂ M₂) (M : Matrix o n R₂) (N : Matrix n o R₂) : M * BilinForm.toMatrix b B * N = BilinForm.toMatrix c (B.comp (Matrix.toLin c b Mᵀ) (Matrix.toLin c b N)) := - LinearMap.mul_toMatrix₂_mul _ _ _ _ (toLin B) _ _ + LinearMap.mul_toMatrix₂_mul _ _ _ _ B _ _ #align bilin_form.mul_to_matrix_mul BilinForm.mul_toMatrix_mul theorem BilinForm.mul_toMatrix (B : BilinForm R₂ M₂) (M : Matrix n n R₂) : M * BilinForm.toMatrix b B = BilinForm.toMatrix b (B.compLeft (Matrix.toLin b b Mᵀ)) := - LinearMap.mul_toMatrix₂ _ _ _ (toLin B) _ + LinearMap.mul_toMatrix₂ _ _ _ B _ #align bilin_form.mul_to_matrix BilinForm.mul_toMatrix theorem BilinForm.toMatrix_mul (B : BilinForm R₂ M₂) (M : Matrix n n R₂) : BilinForm.toMatrix b B * M = BilinForm.toMatrix b (B.compRight (Matrix.toLin b b M)) := - LinearMap.toMatrix₂_mul _ _ _ (toLin B) _ + LinearMap.toMatrix₂_mul _ _ _ B _ #align bilin_form.to_matrix_mul BilinForm.toMatrix_mul theorem Matrix.toBilin_comp (M : Matrix n n R₂) (P Q : Matrix n o R₂) : @@ -416,6 +424,8 @@ theorem mem_skewAdjointMatricesSubmodule' : end MatrixAdjoints +namespace LinearMap + namespace BilinForm section Det @@ -443,13 +453,13 @@ theorem _root_.Matrix.nondegenerate_toBilin'_iff {M : Matrix ι ι R₃} : #align matrix.nondegenerate_to_bilin'_iff Matrix.nondegenerate_toBilin'_iff theorem _root_.Matrix.Nondegenerate.toBilin {M : Matrix ι ι R₃} (h : M.Nondegenerate) - (b : Basis ι R₃ M₃) : (toBilin b M).Nondegenerate := + (b : Basis ι R₃ M₃) : (Matrix.toBilin b M).Nondegenerate := (Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin b).mp h.toBilin' #align matrix.nondegenerate.to_bilin Matrix.Nondegenerate.toBilin @[simp] theorem _root_.Matrix.nondegenerate_toBilin_iff {M : Matrix ι ι R₃} (b : Basis ι R₃ M₃) : - (toBilin b M).Nondegenerate ↔ M.Nondegenerate := by + (Matrix.toBilin b M).Nondegenerate ↔ M.Nondegenerate := by rw [← Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin, Matrix.nondegenerate_toBilin'_iff] #align matrix.nondegenerate_to_bilin_iff Matrix.nondegenerate_toBilin_iff @@ -457,47 +467,47 @@ theorem _root_.Matrix.nondegenerate_toBilin_iff {M : Matrix ι ι R₃} (b : Bas @[simp] theorem nondegenerate_toMatrix'_iff {B : BilinForm R₃ (ι → R₃)} : - B.toMatrix'.Nondegenerate ↔ B.Nondegenerate := + B.toMatrix'.Nondegenerate (R := R₃) (m := ι) ↔ B.Nondegenerate := Matrix.nondegenerate_toBilin'_iff.symm.trans <| (Matrix.toBilin'_toMatrix' B).symm ▸ Iff.rfl -#align bilin_form.nondegenerate_to_matrix'_iff BilinForm.nondegenerate_toMatrix'_iff +#align bilin_form.nondegenerate_to_matrix'_iff LinearMap.BilinForm.nondegenerate_toMatrix'_iff theorem Nondegenerate.toMatrix' {B : BilinForm R₃ (ι → R₃)} (h : B.Nondegenerate) : B.toMatrix'.Nondegenerate := nondegenerate_toMatrix'_iff.mpr h -#align bilin_form.nondegenerate.to_matrix' BilinForm.Nondegenerate.toMatrix' +#align bilin_form.nondegenerate.to_matrix' LinearMap.BilinForm.Nondegenerate.toMatrix' @[simp] theorem nondegenerate_toMatrix_iff {B : BilinForm R₃ M₃} (b : Basis ι R₃ M₃) : - (toMatrix b B).Nondegenerate ↔ B.Nondegenerate := + (BilinForm.toMatrix b B).Nondegenerate ↔ B.Nondegenerate := (Matrix.nondegenerate_toBilin_iff b).symm.trans <| (Matrix.toBilin_toMatrix b B).symm ▸ Iff.rfl -#align bilin_form.nondegenerate_to_matrix_iff BilinForm.nondegenerate_toMatrix_iff +#align bilin_form.nondegenerate_to_matrix_iff LinearMap.BilinForm.nondegenerate_toMatrix_iff theorem Nondegenerate.toMatrix {B : BilinForm R₃ M₃} (h : B.Nondegenerate) (b : Basis ι R₃ M₃) : - (toMatrix b B).Nondegenerate := + (BilinForm.toMatrix b B).Nondegenerate := (nondegenerate_toMatrix_iff b).mpr h -#align bilin_form.nondegenerate.to_matrix BilinForm.Nondegenerate.toMatrix +#align bilin_form.nondegenerate.to_matrix LinearMap.BilinForm.Nondegenerate.toMatrix /-! Some shorthands for combining the above with `Matrix.nondegenerate_of_det_ne_zero` -/ theorem nondegenerate_toBilin'_iff_det_ne_zero {M : Matrix ι ι A} : M.toBilin'.Nondegenerate ↔ M.det ≠ 0 := by rw [Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero] -#align bilin_form.nondegenerate_to_bilin'_iff_det_ne_zero BilinForm.nondegenerate_toBilin'_iff_det_ne_zero +#align bilin_form.nondegenerate_to_bilin'_iff_det_ne_zero LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero theorem nondegenerate_toBilin'_of_det_ne_zero' (M : Matrix ι ι A) (h : M.det ≠ 0) : M.toBilin'.Nondegenerate := nondegenerate_toBilin'_iff_det_ne_zero.mpr h -#align bilin_form.nondegenerate_to_bilin'_of_det_ne_zero' BilinForm.nondegenerate_toBilin'_of_det_ne_zero' +#align bilin_form.nondegenerate_to_bilin'_of_det_ne_zero' LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero' theorem nondegenerate_iff_det_ne_zero {B : BilinForm A M₃} (b : Basis ι A M₃) : - B.Nondegenerate ↔ (toMatrix b B).det ≠ 0 := by + B.Nondegenerate ↔ (BilinForm.toMatrix b B).det ≠ 0 := by rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix_iff] -#align bilin_form.nondegenerate_iff_det_ne_zero BilinForm.nondegenerate_iff_det_ne_zero +#align bilin_form.nondegenerate_iff_det_ne_zero LinearMap.BilinForm.nondegenerate_iff_det_ne_zero -theorem nondegenerate_of_det_ne_zero (b : Basis ι A M₃) (h : (toMatrix b B₃).det ≠ 0) : +theorem nondegenerate_of_det_ne_zero (b : Basis ι A M₃) (h : (BilinForm.toMatrix b B₃).det ≠ 0) : B₃.Nondegenerate := (nondegenerate_iff_det_ne_zero b).mpr h -#align bilin_form.nondegenerate_of_det_ne_zero BilinForm.nondegenerate_of_det_ne_zero +#align bilin_form.nondegenerate_of_det_ne_zero LinearMap.BilinForm.nondegenerate_of_det_ne_zero end Det diff --git a/Mathlib/RingTheory/DedekindDomain/Different.lean b/Mathlib/RingTheory/DedekindDomain/Different.lean index 2d833750535871..5cfc21b0b89557 100644 --- a/Mathlib/RingTheory/DedekindDomain/Different.lean +++ b/Mathlib/RingTheory/DedekindDomain/Different.lean @@ -455,7 +455,7 @@ lemma traceForm_dualSubmodule_adjoin let pb := (Algebra.adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq _ _ hx).trans (Subalgebra.topEquiv)) have pbgen : pb.gen = x := by simp [pb] - have hpb : ⇑(BilinForm.dualBasis (traceForm K L) _ pb.basis) = _ := + have hpb : ⇑(LinearMap.BilinForm.dualBasis (traceForm K L) _ pb.basis) = _ := _root_.funext (traceForm_dualBasis_powerBasis_eq pb) have : (Subalgebra.toSubmodule (Algebra.adjoin A {x})) = Submodule.span A (Set.range pb.basis) := by @@ -469,7 +469,7 @@ lemma traceForm_dualSubmodule_adjoin exact ⟨fun ⟨a, b, c⟩ ↦ ⟨⟨a, b⟩, c⟩, fun ⟨⟨a, b⟩, c⟩ ↦ ⟨a, b, c⟩⟩ clear_value pb conv_lhs => rw [this] - rw [← span_coeff_minpolyDiv hAx, BilinForm.dualSubmodule_span_of_basis, + rw [← span_coeff_minpolyDiv hAx, LinearMap.BilinForm.dualSubmodule_span_of_basis, Submodule.smul_span, hpb] show _ = Submodule.span A (_ '' _) simp only [← Set.range_comp, smul_eq_mul, div_eq_inv_mul, pbgen, @@ -516,7 +516,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] simp_rw [← Subalgebra.mem_toSubmodule, ← Submodule.mul_mem_smul_iff (y := y * _) (mem_nonZeroDivisors_of_ne_zero hne₂)] rw [← traceForm_dualSubmodule_adjoin A K hx this] - simp only [BilinForm.mem_dualSubmodule, traceForm_apply, Subalgebra.mem_toSubmodule, + simp only [LinearMap.BilinForm.mem_dualSubmodule, traceForm_apply, Subalgebra.mem_toSubmodule, minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map, aeval_map_algebraMap, aeval_algebraMap_apply, mul_assoc, FractionalIdeal.mem_one_iff, forall_exists_index, forall_apply_eq_imp_iff] diff --git a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean index 4252a6516c7ce2..c368581f2ed332 100644 --- a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean +++ b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean @@ -95,10 +95,11 @@ theorem IsIntegralClosure.range_le_span_dualBasis [IsSeparable K L] {ι : Type*} [DecidableEq ι] (b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A] : LinearMap.range ((Algebra.linearMap C L).restrictScalars A) ≤ Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_nondegenerate K L) b) := by - rw [← BilinForm.dualSubmodule_span_of_basis, ← BilinForm.le_flip_dualSubmodule, - Submodule.span_le] + rw [← LinearMap.BilinForm.dualSubmodule_span_of_basis, + ← LinearMap.BilinForm.le_flip_dualSubmodule, Submodule.span_le] rintro _ ⟨i, rfl⟩ _ ⟨y, rfl⟩ - simp only [LinearMap.coe_restrictScalars, linearMap_apply, BilinForm.flip_apply, traceForm_apply] + simp only [LinearMap.coe_restrictScalars, linearMap_apply, LinearMap.BilinForm.flip_apply, + traceForm_apply] refine IsIntegrallyClosed.isIntegral_iff.mp ?_ exact isIntegral_trace ((IsIntegralClosure.isIntegral A L y).algebraMap.mul (hb_int i)) #align is_integral_closure.range_le_span_dual_basis IsIntegralClosure.range_le_span_dualBasis diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean index 63844ce66e6ac8..1518e943f11b6f 100644 --- a/Mathlib/RingTheory/Discriminant.lean +++ b/Mathlib/RingTheory/Discriminant.lean @@ -135,7 +135,7 @@ variable [Module.Finite K L] [IsAlgClosed E] /-- If `b` is a basis of a finite separable field extension `L/K`, then `Algebra.discr K b ≠ 0`. -/ theorem discr_not_zero_of_basis [IsSeparable K L] (b : Basis ι K L) : discr K b ≠ 0 := by - rw [discr_def, traceMatrix_of_basis, ← BilinForm.nondegenerate_iff_det_ne_zero] + rw [discr_def, traceMatrix_of_basis, ← LinearMap.BilinForm.nondegenerate_iff_det_ne_zero] exact traceForm_nondegenerate _ _ #align algebra.discr_not_zero_of_basis Algebra.discr_not_zero_of_basis diff --git a/Mathlib/RingTheory/Trace.lean b/Mathlib/RingTheory/Trace.lean index 2cfa563e3ed4b0..47e1aadde68201 100644 --- a/Mathlib/RingTheory/Trace.lean +++ b/Mathlib/RingTheory/Trace.lean @@ -73,6 +73,7 @@ variable {ι κ : Type w} [Fintype ι] open FiniteDimensional +open LinearMap (BilinForm) open LinearMap open Matrix @@ -673,8 +674,9 @@ lemma traceForm_dualBasis_powerBasis_eq [FiniteDimensional K L] [IsSeparable K L simp only [AlgEquiv.toAlgHom_eq_coe, Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, AlgHom.coe_coe, finset_sum_coeff, coeff_smul, coeff_map, smul_eq_mul, coeff_X_pow, ← Fin.ext_iff, @eq_comm _ i] at this - rw [PowerBasis.coe_basis, Algebra.traceForm_apply, RingHom.map_ite_one_zero, - ← this, trace_eq_sum_embeddings (E := AlgebraicClosure K)] + rw [PowerBasis.coe_basis] + simp only [RingHom.map_ite_one_zero, traceForm_apply] + rw [← this, trace_eq_sum_embeddings (E := AlgebraicClosure K)] apply Finset.sum_congr rfl intro σ _ simp only [_root_.map_mul, map_div₀, map_pow] diff --git a/docs/overview.yaml b/docs/overview.yaml index d57349b961277e..595b2f79759419 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -185,9 +185,9 @@ Linear algebra: eigenvector: 'Module.End.HasEigenvector' existence of an eigenvalue: 'Module.End.exists_eigenvalue' Bilinear and quadratic forms: - bilinear form: 'BilinForm' - alternating bilinear form: 'BilinForm.IsAlt' - symmetric bilinear form: 'BilinForm.IsSymm' + bilinear form: 'LinearMap.BilinForm' + alternating bilinear form: 'LinearMap.BilinForm.IsAlt' + symmetric bilinear form: 'LinearMap.BilinForm.IsSymm' matrix representation: 'BilinForm.toMatrix' quadratic form: 'QuadraticForm' polar form of a quadratic: 'QuadraticForm.polar' diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml index 46b8f7b45d44a2..7cbaaaaef9e89e 100644 --- a/docs/undergrad.yaml +++ b/docs/undergrad.yaml @@ -193,10 +193,10 @@ Ring Theory: # 4. Bilinear and Quadratic Forms Over a Vector Space: Bilinear forms: - bilinear forms: 'BilinForm' - alternating bilinear forms: 'BilinForm.IsAlt' - symmetric bilinear forms: 'BilinForm.IsSymm' - nondegenerate forms: 'BilinForm.Nondegenerate' + bilinear forms: 'LinearMap.BilinForm' + alternating bilinear forms: 'LinearMap.BilinForm.IsAlt' + symmetric bilinear forms: 'LinearMap.BilinForm.IsSymm' + nondegenerate forms: 'LinearMap.BilinForm.Nondegenerate' matrix representation: 'BilinForm.toMatrix' change of coordinates: 'BilinForm.toMatrix_comp' rank of a bilinear form: '' @@ -204,8 +204,8 @@ Bilinear and Quadratic Forms Over a Vector Space: quadratic form: 'QuadraticForm' polar form of a quadratic: 'QuadraticForm.polar' Orthogonality: - orthogonal elements: 'BilinForm.IsOrtho' - adjoint endomorphism: 'BilinForm.leftAdjointOfNondegenerate' + orthogonal elements: 'LinearMap.BilinForm.IsOrtho' + adjoint endomorphism: 'LinearMap.BilinForm.leftAdjointOfNondegenerate' Sylvester's law of inertia: 'https://en.wikipedia.org/wiki/Sylvester%27s_law_of_inertia' real classification: 'https://en.wikipedia.org/wiki/Sylvester%27s_law_of_inertia' complex classification: ''