From f6d1a101ba1e934d4ed4731f957695986eec8cb6 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 18 Mar 2024 23:55:30 +0000 Subject: [PATCH] refactor(LinearAlgebra/BilinearForm/Basic): descope `BilinForm` to modules over commutative semirings (#11280) Require the module in the definition of the `BilinForm` structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: https://github.com/leanprover-community/mathlib4/issues/10553#issuecomment-1944434170 Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like https://github.com/leanprover-community/mathlib4/pull/9334#pullrequestreview-1880856848). Co-authored-by: @Vierkantor Co-authored-by: Christopher Hoskin Co-authored-by: Christopher Hoskin Co-authored-by: Eric Wieser --- Mathlib/LinearAlgebra/BilinearForm/Basic.lean | 54 +++---- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 132 +++++++----------- .../BilinearForm/Orthogonal.lean | 20 +-- .../BilinearForm/Properties.lean | 70 +++++----- .../LinearAlgebra/Matrix/BilinearForm.lean | 10 +- 5 files changed, 113 insertions(+), 173 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean index 22735d95e9109f..3b511c2156a5d4 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean @@ -30,10 +30,8 @@ Given any term `B` of type `BilinForm`, due to a coercion, can use the notation `B x y` to refer to the function field, ie. `B x y = B.bilin x y`. In this file we use the following type variables: - - `M`, `M'`, ... are modules over the semiring `R`, - - `M₁`, `M₁'`, ... are modules over the ring `R₁`, - - `M₂`, `M₂'`, ... are modules over the commutative semiring `R₂`, - - `M₃`, `M₃'`, ... are modules over the commutative ring `R₃`, + - `M`, `M'`, ... are modules over the commutative semiring `R`, + - `M₁`, `M₁'`, ... are modules over the commutative ring `R₁`, - `V`, ... is a vector space over the field `K`. ## References @@ -51,7 +49,7 @@ open BigOperators universe u v w /-- `BilinForm R M` is the type of `R`-bilinear functions `M → M → R`. -/ -structure BilinForm (R : Type*) (M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] where +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 @@ -59,13 +57,11 @@ structure BilinForm (R : Type*) (M : Type*) [Semiring R] [AddCommMonoid M] [Modu bilin_smul_right : ∀ (a : R) (x y : M), bilin x (a • y) = a * bilin x y #align bilin_form BilinForm -variable {R : Type*} {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] +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] -variable {R₁ : Type*} {M₁ : Type*} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] -variable {R₂ : Type*} {M₂ : Type*} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] -variable {R₃ : Type*} {M₃ : Type*} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] +variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V] -variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} {B₂ : BilinForm R₂ M₂} +variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} namespace BilinForm @@ -299,17 +295,15 @@ instance {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R R] : DistribMulAction α (BilinForm R M) := Function.Injective.distribMulAction coeFnAddMonoidHom coe_injective coe_smul -instance {α} [Semiring α] [Module α R] [SMulCommClass α R R] : Module α (BilinForm R M) := +instance {α} [CommSemiring α] [Module α R] [SMulCommClass α R R] : Module α (BilinForm R M) := Function.Injective.module _ coeFnAddMonoidHom coe_injective coe_smul section flip -variable (R₂) - /-- 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 [Algebra R₂ R] : BilinForm R M →ₗ[R₂] BilinForm R M where +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 @@ -326,47 +320,37 @@ def flipHomAux [Algebra R₂ R] : BilinForm R M →ₗ[R₂] BilinForm R M where variable {R₂} -theorem flip_flip_aux [Algebra R₂ R] (A : BilinForm R M) : - (flipHomAux R₂) (flipHomAux R₂ A) = A := by +theorem flip_flip_aux (A : BilinForm R M) : + (flipHomAux) (flipHomAux A) = A := by ext A simp [flipHomAux] #align bilin_form.flip_flip_aux BilinForm.flip_flip_aux variable (R₂) -/-- The flip of a bilinear form, obtained by exchanging the left and right arguments. This is a -less structured version of the equiv which applies to general (noncommutative) rings `R` with a -distinguished commutative subring `R₂`; over a commutative ring use `flip`. -/ -def flipHom [Algebra R₂ R] : BilinForm R M ≃ₗ[R₂] BilinForm R M := - { flipHomAux R₂ with - invFun := flipHomAux R₂ +/-- 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 left_inv := flip_flip_aux right_inv := flip_flip_aux } #align bilin_form.flip_hom BilinForm.flipHom -variable {R₂} - @[simp] -theorem flip_apply [Algebra R₂ R] (A : BilinForm R M) (x y : M) : flipHom R₂ A x y = A y x := +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 -theorem flip_flip [Algebra R₂ R] : - (flipHom R₂).trans (flipHom R₂) = LinearEquiv.refl R₂ (BilinForm R M) := by +theorem flip_flip : + flipHom.trans flipHom = LinearEquiv.refl R (BilinForm R M) := by ext A simp #align bilin_form.flip_flip BilinForm.flip_flip -/-- The flip of a bilinear form over a ring, obtained by exchanging the left and right arguments, -here considered as an `ℕ`-linear equivalence, i.e. an additive equivalence. -/ -abbrev flip' : BilinForm R M ≃ₗ[ℕ] BilinForm R M := - flipHom ℕ -#align bilin_form.flip' BilinForm.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 R₂ +abbrev flip : BilinForm R M ≃ₗ[R] BilinForm R M := + flipHom #align bilin_form.flip BilinForm.flip end flip diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index 7b3821fa321883..8704baa0bf4bfc 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -18,10 +18,8 @@ Given any term `B` of type `BilinForm`, due to a coercion, can use the notation `B x y` to refer to the function field, ie. `B x y = B.bilin x y`. In this file we use the following type variables: - - `M`, `M'`, ... are modules over the semiring `R`, - - `M₁`, `M₁'`, ... are modules over the ring `R₁`, - - `M₂`, `M₂'`, ... are modules over the commutative semiring `R₂`, - - `M₃`, `M₃'`, ... are modules over the commutative ring `R₃`, + - `M`, `M'`, ... are modules over the commutative semiring `R`, + - `M₁`, `M₁'`, ... are modules over the commutative ring `R₁`, - `V`, ... is a vector space over the field `K`. ## References @@ -38,19 +36,15 @@ open BigOperators universe u v w -variable {R : Type*} {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] -variable {R₁ : Type*} {M₁ : Type*} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] -variable {R₂ : Type*} {M₂ : Type*} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] -variable {R₃ : Type*} {M₃ : Type*} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] +variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] +variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V] -variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} {B₂ : BilinForm R₂ M₂} +variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} namespace BilinForm section ToLin' -variable [Algebra R₂ R] [Module R₂ M] [IsScalarTower R₂ R M] - /-- Auxiliary definition to define `toLinHom`; see below. -/ def toLinHomAux₁ (A : BilinForm R M) (x : M) : M →ₗ[R] R where toFun y := A x y @@ -59,7 +53,7 @@ def toLinHomAux₁ (A : BilinForm R M) (x : M) : M →ₗ[R] R where #align bilin_form.to_lin_hom_aux₁ BilinForm.toLinHomAux₁ /-- Auxiliary definition to define `toLinHom`; see below. -/ -def toLinHomAux₂ (A : BilinForm R M) : M →ₗ[R₂] M →ₗ[R] R where +def toLinHomAux₂ (A : BilinForm R M) : M →ₗ[R] M →ₗ[R] R where toFun := toLinHomAux₁ A map_add' x₁ x₂ := LinearMap.ext fun x => by @@ -70,18 +64,12 @@ def toLinHomAux₂ (A : BilinForm R M) : M →ₗ[R₂] M →ₗ[R] R where intros -- Porting note: moved out of `simp only` rw [← algebraMap_smul R c x] - simp only [Algebra.smul_def, LinearMap.coe_mk, LinearMap.smul_apply, smul_left] + simp only [Algebra.id.map_eq_id, RingHom.id_apply, smul_left] #align bilin_form.to_lin_hom_aux₂ BilinForm.toLinHomAux₂ -variable (R₂) - /-- The linear map obtained from a `BilinForm` by fixing the left co-ordinate and evaluating in -the right. -This is the most general version of the construction; it is `R₂`-linear for some distinguished -commutative subsemiring `R₂` of the scalar ring. Over a semiring with no particular distinguished -such subsemiring, use `toLin'`, which is `ℕ`-linear. Over a commutative semiring, use `toLin`, -which is linear. -/ -def toLinHom : BilinForm R M →ₗ[R₂] M →ₗ[R₂] M →ₗ[R] R where +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 @@ -100,32 +88,23 @@ def toLinHom : BilinForm R M →ₗ[R₂] M →ₗ[R₂] M →ₗ[R] R where AddHom.coe_mk] #align bilin_form.to_lin_hom BilinForm.toLinHom -variable {R₂} - @[simp] -theorem toLin'_apply (A : BilinForm R M) (x : M) : ⇑(toLinHom R₂ A x) = A x := +theorem toLin'_apply (A : BilinForm R M) (x : M) : ⇑(toLinHom A x) = A x := rfl #align bilin_form.to_lin'_apply BilinForm.toLin'_apply -/-- The linear map obtained from a `BilinForm` by fixing the left co-ordinate and evaluating in -the right. -Over a commutative semiring, use `toLin`, which is linear rather than `ℕ`-linear. -/ -abbrev toLin' : BilinForm R M →ₗ[ℕ] M →ₗ[ℕ] M →ₗ[R] R := - toLinHom ℕ -#align bilin_form.to_lin' BilinForm.toLin' - 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.toLin' B).map_sum₂ t g w + (BilinForm.toLinHom B).map_sum₂ t g w #align bilin_form.sum_left BilinForm.sum_left @[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.toLin' B w) _ _ + map_sum (BilinForm.toLinHom B w) _ _ #align bilin_form.sum_right BilinForm.sum_right @[simp] @@ -135,32 +114,19 @@ theorem sum_apply {α} (t : Finset α) (B : α → BilinForm R M) (v w : M) : rw [map_sum, Finset.sum_apply, Finset.sum_apply] rfl -variable {B} (R₂) +variable {B} /-- The linear map obtained from a `BilinForm` by fixing the right co-ordinate and evaluating in -the left. -This is the most general version of the construction; it is `R₂`-linear for some distinguished -commutative subsemiring `R₂` of the scalar ring. Over semiring with no particular distinguished -such subsemiring, use `toLin'Flip`, which is `ℕ`-linear. Over a commutative semiring, use -`toLinFlip`, which is linear. -/ -def toLinHomFlip : BilinForm R M →ₗ[R₂] M →ₗ[R₂] M →ₗ[R] R := - (toLinHom R₂).comp (flipHom R₂).toLinearMap +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 -variable {R₂} - @[simp] -theorem toLin'Flip_apply (A : BilinForm R M) (x : M) : ⇑(toLinHomFlip R₂ A x) = fun y => A y x := +theorem toLin'Flip_apply (A : BilinForm R M) (x : M) : ⇑(toLinHomFlip A x) = fun y => A y x := rfl #align bilin_form.to_lin'_flip_apply BilinForm.toLin'Flip_apply -/-- The linear map obtained from a `BilinForm` by fixing the right co-ordinate and evaluating in -the left. -Over a commutative semiring, use `toLinFlip`, which is linear rather than `ℕ`-linear. -/ -abbrev toLin'Flip : BilinForm R M →ₗ[ℕ] M →ₗ[ℕ] M →ₗ[R] R := - toLinHomFlip ℕ -#align bilin_form.to_lin'_flip BilinForm.toLin'Flip - end ToLin' end BilinForm @@ -171,7 +137,7 @@ section EquivLin 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 +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 @@ -182,8 +148,8 @@ def LinearMap.toBilinAux (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) : BilinF #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₂ := - { BilinForm.toLinHom R₂ with +def BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R] R := + { BilinForm.toLinHom with invFun := LinearMap.toBilinAux left_inv := fun B => by ext @@ -194,35 +160,35 @@ def BilinForm.toLin : BilinForm R₂ M₂ ≃ₗ[R₂] M₂ →ₗ[R₂] M₂ #align bilin_form.to_lin 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₂ := +def LinearMap.toBilin : (M →ₗ[R] M →ₗ[R] R) ≃ₗ[R] BilinForm R M := BilinForm.toLin.symm #align linear_map.to_bilin LinearMap.toBilin @[simp] -theorem LinearMap.toBilinAux_eq (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) : +theorem LinearMap.toBilinAux_eq (f : M →ₗ[R] M →ₗ[R] R) : LinearMap.toBilinAux f = LinearMap.toBilin f := rfl #align linear_map.to_bilin_aux_eq LinearMap.toBilinAux_eq @[simp] theorem LinearMap.toBilin_symm : - (LinearMap.toBilin.symm : BilinForm R₂ M₂ ≃ₗ[R₂] _) = BilinForm.toLin := + (LinearMap.toBilin.symm : BilinForm R M ≃ₗ[R] _) = BilinForm.toLin := rfl #align linear_map.to_bilin_symm LinearMap.toBilin_symm @[simp] theorem BilinForm.toLin_symm : - (BilinForm.toLin.symm : _ ≃ₗ[R₂] BilinForm R₂ M₂) = LinearMap.toBilin := + (BilinForm.toLin.symm : _ ≃ₗ[R] BilinForm R M) = LinearMap.toBilin := LinearMap.toBilin.symm_symm #align bilin_form.to_lin_symm BilinForm.toLin_symm @[simp, norm_cast] -theorem LinearMap.toBilin_apply (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) (x y : M₂) : +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 := +theorem BilinForm.toLin_apply (x : M) : ⇑(BilinForm.toLin B x) = B x := rfl #align bilin_form.to_lin_apply BilinForm.toLin_apply @@ -358,13 +324,13 @@ theorem comp_inj (B₁ B₂ : BilinForm R M') {l r : M →ₗ[R] M'} (hₗ : Fun end Comp -variable {M₂' M₂'' : Type*} -variable [AddCommMonoid M₂'] [AddCommMonoid M₂''] [Module R₂ M₂'] [Module R₂ M₂''] +variable {M' M'' : Type*} +variable [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] section congr /-- Apply a linear equivalence on the arguments of a bilinear form. -/ -def congr (e : M₂ ≃ₗ[R₂] M₂') : BilinForm R₂ M₂ ≃ₗ[R₂] BilinForm R₂ M₂' where +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] @@ -374,43 +340,43 @@ def congr (e : M₂ ≃ₗ[R₂] M₂') : BilinForm R₂ M₂ ≃ₗ[R₂] Bilin #align bilin_form.congr BilinForm.congr @[simp] -theorem congr_apply (e : M₂ ≃ₗ[R₂] M₂') (B : BilinForm R₂ M₂) (x y : M₂') : +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 @[simp] -theorem congr_symm (e : M₂ ≃ₗ[R₂] M₂') : (congr e).symm = congr e.symm := by +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 @[simp] -theorem congr_refl : congr (LinearEquiv.refl R₂ M₂) = LinearEquiv.refl R₂ _ := +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 -theorem congr_trans (e : M₂ ≃ₗ[R₂] M₂') (f : M₂' ≃ₗ[R₂] M₂'') : +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 -theorem congr_congr (e : M₂' ≃ₗ[R₂] M₂'') (f : M₂ ≃ₗ[R₂] M₂') (B : BilinForm R₂ M₂) : +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 -theorem congr_comp (e : M₂ ≃ₗ[R₂] M₂') (B : BilinForm R₂ M₂) (l r : M₂'' →ₗ[R₂] M₂') : +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) := + 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 -theorem comp_congr (e : M₂' ≃ₗ[R₂] M₂'') (B : BilinForm R₂ M₂) (l r : M₂' →ₗ[R₂] M₂) : +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₂')) := + 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 @@ -419,7 +385,7 @@ 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 +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] @@ -427,7 +393,7 @@ def linMulLin (f g : M₂ →ₗ[R₂] R₂) : BilinForm R₂ M₂ where 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 -variable {f g : M₂ →ₗ[R₂] R₂} +variable {f g : M →ₗ[R] R} @[simp] theorem linMulLin_apply (x y) : linMulLin f g x y = f x * g y := @@ -435,19 +401,19 @@ theorem linMulLin_apply (x y) : linMulLin f g x y = f x * g y := #align bilin_form.lin_mul_lin_apply BilinForm.linMulLin_apply @[simp] -theorem linMulLin_comp (l r : M₂' →ₗ[R₂] M₂) : +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 @[simp] -theorem linMulLin_compLeft (l : M₂ →ₗ[R₂] M₂) : +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 @[simp] -theorem linMulLin_compRight (r : M₂ →ₗ[R₂] M₂) : +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 @@ -456,17 +422,17 @@ end LinMulLin section Basis -variable {F₂ : BilinForm R₂ M₂} -variable {ι : Type*} (b : Basis ι R₂ M₂) +variable {F₂ : BilinForm R M} +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₂ := +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 /-- 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₂) : - ((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • B₂ (b i) (b j)) = B₂ x y := by +theorem sum_repr_mul_repr_mul (x y : M) : + ((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • B (b i) (b j)) = B x y := by 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] diff --git a/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean b/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean index 8ded8d8286372e..c24b80c12f4c50 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean @@ -17,10 +17,8 @@ Given any term `B` of type `BilinForm`, due to a coercion, can use the notation `B x y` to refer to the function field, ie. `B x y = B.bilin x y`. In this file we use the following type variables: - - `M`, `M'`, ... are modules over the semiring `R`, - - `M₁`, `M₁'`, ... are modules over the ring `R₁`, - - `M₂`, `M₂'`, ... are modules over the commutative semiring `R₂`, - - `M₃`, `M₃'`, ... are modules over the commutative ring `R₃`, + - `M`, `M'`, ... are modules over the commutative semiring `R`, + - `M₁`, `M₁'`, ... are modules over the commutative ring `R₁`, - `V`, ... is a vector space over the field `K`. ## References @@ -37,14 +35,10 @@ open BigOperators universe u v w -variable {R : Type*} {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] -variable {R₁ : Type*} {M₁ : Type*} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] -variable {R₂ : Type*} {M₂ : Type*} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] -variable {R₃ : Type*} {M₃ : Type*} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] +variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] +variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V] -variable {M₂' M₂'' : Type*} -variable [AddCommMonoid M₂'] [AddCommMonoid M₂''] [Module R₂ M₂'] [Module R₂ M₂''] -variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} {B₂ : BilinForm R₂ M₂} +variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} namespace BilinForm @@ -98,7 +92,7 @@ set_option linter.uppercaseLean3 false in section -variable {R₄ M₄ : Type*} [Ring R₄] [IsDomain R₄] +variable {R₄ M₄ : Type*} [CommRing R₄] [IsDomain R₄] variable [AddCommGroup M₄] [Module R₄ M₄] {G : BilinForm R₄ M₄} @[simp] @@ -216,7 +210,7 @@ theorem isCompl_span_singleton_orthogonal {B : BilinForm K V} {x : V} (hx : ¬B. end Orthogonal variable {M₂' : Type*} -variable [AddCommMonoid M₂'] [Module R₂ M₂'] +variable [AddCommMonoid M₂'] [Module R M₂'] /-- The restriction of a reflexive bilinear form `B` onto a submodule `W` is nondegenerate if `Disjoint W (B.orthogonal W)`. -/ diff --git a/Mathlib/LinearAlgebra/BilinearForm/Properties.lean b/Mathlib/LinearAlgebra/BilinearForm/Properties.lean index 13e037841a44ea..6df88d8c59bdd2 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Properties.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Properties.lean @@ -19,10 +19,8 @@ Given any term `B` of type `BilinForm`, due to a coercion, can use the notation `B x y` to refer to the function field, ie. `B x y = B.bilin x y`. In this file we use the following type variables: - - `M`, `M'`, ... are modules over the semiring `R`, - - `M₁`, `M₁'`, ... are modules over the ring `R₁`, - - `M₂`, `M₂'`, ... are modules over the commutative semiring `R₂`, - - `M₃`, `M₃'`, ... are modules over the commutative ring `R₃`, + - `M`, `M'`, ... are modules over the commutative semiring `R`, + - `M₁`, `M₁'`, ... are modules over the commutative ring `R₁`, - `V`, ... is a vector space over the field `K`. ## References @@ -39,14 +37,13 @@ open BigOperators universe u v w -variable {R : Type*} {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] -variable {R₁ : Type*} {M₁ : Type*} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] -variable {R₂ : Type*} {M₂ : Type*} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] -variable {R₃ : Type*} {M₃ : Type*} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] +variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] +variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V] -variable {M₂' M₂'' : Type*} -variable [AddCommMonoid M₂'] [AddCommMonoid M₂''] [Module R₂ M₂'] [Module R₂ M₂''] -variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} {B₂ : BilinForm R₂ M₂} +variable {M' M'' : Type*} +variable [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] + +variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁} namespace BilinForm @@ -69,8 +66,9 @@ protected theorem neg {B : BilinForm R₁ M₁} (hB : B.IsRefl) : (-B).IsRefl := neg_eq_zero.mpr ∘ hB x y ∘ neg_eq_zero.mp #align bilin_form.is_refl.neg BilinForm.IsRefl.neg -protected theorem smul {α} [Semiring α] [Module α R] [SMulCommClass α R R] [NoZeroSMulDivisors α R] - (a : α) {B : BilinForm R M} (hB : B.IsRefl) : (a • B).IsRefl := fun _ _ h => +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 @@ -141,7 +139,7 @@ theorem isSymm_neg {B : BilinForm R₁ M₁} : (-B).IsSymm ↔ B.IsSymm := #align bilin_form.is_symm_neg BilinForm.isSymm_neg variable (R₂) in -theorem isSymm_iff_flip [Algebra R₂ R] : B.IsSymm ↔ flipHom R₂ B = B := +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 @@ -248,10 +246,10 @@ theorem IsAdjointPair.sub (h : IsAdjointPair B₁ B₁' f₁ g₁) (h' : IsAdjoi rw [LinearMap.sub_apply, LinearMap.sub_apply, sub_left, sub_right, h, h'] #align bilin_form.is_adjoint_pair.sub BilinForm.IsAdjointPair.sub -variable {B₂' : BilinForm R₂ M₂'} {f₂ f₂' : M₂ →ₗ[R₂] M₂'} {g₂ g₂' : M₂' →ₗ[R₂] M₂} +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 +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 @@ -268,7 +266,7 @@ theorem IsAdjointPair.mul {f g f' g' : Module.End R M} (h : IsAdjointPair B B f rw [LinearMap.mul_apply, LinearMap.mul_apply, h, h'] #align bilin_form.is_adjoint_pair.mul BilinForm.IsAdjointPair.mul -variable (B B' B₁ B₂) (F₂ : BilinForm R₂ M₂) +variable (B B' B₁ B₂) (F₂ : BilinForm R M) /-- The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms on the underlying module. In the case that these two forms are identical, this is the usual concept @@ -279,7 +277,7 @@ def IsPairSelfAdjoint (f : Module.End R M) := #align bilin_form.is_pair_self_adjoint 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 +def isPairSelfAdjointSubmodule : Submodule R (Module.End R M) where carrier := { f | IsPairSelfAdjoint B₂ F₂ f } zero_mem' := isAdjointPair_zero add_mem' hf hg := hf.add hg @@ -287,11 +285,11 @@ def isPairSelfAdjointSubmodule : Submodule R₂ (Module.End R₂ M₂) where #align bilin_form.is_pair_self_adjoint_submodule BilinForm.isPairSelfAdjointSubmodule @[simp] -theorem mem_isPairSelfAdjointSubmodule (f : Module.End R₂ M₂) : +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 -theorem isPairSelfAdjoint_equiv (e : M₂' ≃ₗ[R₂] M₂) (f : Module.End R₂ M₂) : +theorem isPairSelfAdjoint_equiv (e : M' ≃ₗ[R] M) (f : Module.End R M) : IsPairSelfAdjoint B₂ F₂ f ↔ IsPairSelfAdjoint (B₂.comp ↑e ↑e) (F₂.comp ↑e ↑e) (e.symm.conj f) := by have hₗ : (F₂.comp ↑e ↑e).compLeft (e.symm.conj f) = (F₂.compLeft f).comp ↑e ↑e := by @@ -300,7 +298,7 @@ theorem isPairSelfAdjoint_equiv (e : M₂' ≃ₗ[R₂] M₂) (f : Module.End R have hᵣ : (B₂.comp ↑e ↑e).compRight (e.symm.conj f) = (B₂.compRight f).comp ↑e ↑e := by ext simp [LinearEquiv.conj_apply] - have he : Function.Surjective (⇑(↑e : M₂' →ₗ[R₂] M₂) : M₂' → M₂) := e.surjective + have he : Function.Surjective (⇑(↑e : M' →ₗ[R] M) : M' → M) := e.surjective show BilinForm.IsAdjointPair _ _ _ _ ↔ BilinForm.IsAdjointPair _ _ _ _ rw [isAdjointPair_iff_compLeft_eq_compRight, isAdjointPair_iff_compLeft_eq_compRight, hᵣ, hₗ, comp_inj _ _ he he] @@ -327,26 +325,24 @@ theorem isSkewAdjoint_iff_neg_self_adjoint (f : Module.End R₁ M₁) : /-- 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₂ + isPairSelfAdjointSubmodule B B #align bilin_form.self_adjoint_submodule BilinForm.selfAdjointSubmodule @[simp] -theorem mem_selfAdjointSubmodule (f : Module.End R₂ M₂) : - f ∈ B₂.selfAdjointSubmodule ↔ B₂.IsSelfAdjoint f := +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 -variable (B₃ : BilinForm R₃ M₃) - /-- 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₃ + isPairSelfAdjointSubmodule (-B₁) B₁ #align bilin_form.skew_adjoint_submodule BilinForm.skewAdjointSubmodule @[simp] -theorem mem_skewAdjointSubmodule (f : Module.End R₃ M₃) : - f ∈ B₃.skewAdjointSubmodule ↔ B₃.IsSkewAdjoint f := by +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 @@ -381,21 +377,21 @@ theorem not_nondegenerate_zero [Nontrivial M] : ¬(0 : BilinForm R M).Nondegener end -variable {M₂' : Type*} -variable [AddCommMonoid M₂'] [Module R₂ M₂'] +variable {M' : Type*} +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 -theorem Nondegenerate.congr {B : BilinForm R₂ M₂} (e : M₂ ≃ₗ[R₂] M₂') (h : B.Nondegenerate) : +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 @[simp] -theorem nondegenerate_congr_iff {B : BilinForm R₂ M₂} (e : M₂ ≃ₗ[R₂] M₂') : +theorem nondegenerate_congr_iff {B : BilinForm R M} (e : M ≃ₗ[R] M') : (congr e B).Nondegenerate ↔ B.Nondegenerate := ⟨fun h => by convert h.congr e.symm @@ -403,7 +399,7 @@ theorem nondegenerate_congr_iff {B : BilinForm R₂ M₂} (e : M₂ ≃ₗ[R₂] #align bilin_form.nondegenerate_congr_iff 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₂} : +theorem nondegenerate_iff_ker_eq_bot {B : BilinForm R M} : B.Nondegenerate ↔ LinearMap.ker (BilinForm.toLin B) = ⊥ := by rw [LinearMap.ker_eq_bot'] constructor <;> intro h @@ -416,7 +412,7 @@ theorem nondegenerate_iff_ker_eq_bot {B : BilinForm R₂ M₂} : exact hm x #align bilin_form.nondegenerate_iff_ker_eq_bot BilinForm.nondegenerate_iff_ker_eq_bot -theorem Nondegenerate.ker_eq_bot {B : BilinForm R₂ M₂} (h : B.Nondegenerate) : +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 @@ -500,7 +496,7 @@ 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 (R₂ := K), + rw [toLin_apply, apply_dualBasis_left, toLin_apply, ← B.flip_apply, apply_dualBasis_left] simp_rw [@eq_comm _ i j] diff --git a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean index 6ce7c6a29ee784..79d3c20d7c17ce 100644 --- a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean +++ b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean @@ -27,8 +27,8 @@ This file defines the conversion between bilinear forms and matrices. ## Notations In this file we use the following type variables: - - `M`, `M'`, ... are modules over the semiring `R`, - - `M₁`, `M₁'`, ... are modules over the ring `R₁`, + - `M`, `M'`, ... are modules over the commutative semiring `R`, + - `M₁`, `M₁'`, ... are modules over the commutative ring `R₁`, - `M₂`, `M₂'`, ... are modules over the commutative semiring `R₂`, - `M₃`, `M₃'`, ... are modules over the commutative ring `R₃`, - `V`, ... is a vector space over the field `K`. @@ -40,8 +40,8 @@ bilinear form, bilin form, BilinearForm, matrix, basis -/ -variable {R : Type*} {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] -variable {R₁ : Type*} {M₁ : Type*} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] +variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] +variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] variable {R₂ : Type*} {M₂ : Type*} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] variable {R₃ : Type*} {M₃ : Type*} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V] @@ -74,7 +74,7 @@ theorem Matrix.toBilin'Aux_stdBasis [Fintype n] [DecidableEq n] (M : Matrix n n This is an auxiliary definition for the equivalence `Matrix.toBilin'`. -/ def BilinForm.toMatrixAux (b : n → M₂) : BilinForm R₂ M₂ →ₗ[R₂] Matrix n n R₂ := - (LinearMap.toMatrix₂Aux b b) ∘ₗ BilinForm.toLinHom (R₂ := R₂) + (LinearMap.toMatrix₂Aux b b) ∘ₗ BilinForm.toLinHom #align bilin_form.to_matrix_aux BilinForm.toMatrixAux @[simp]