refactor(LinearAlgebra/BilinearForm/Hom): Deprecate results (#12078)

Following the removal of `structure BilinForm` from Mathlib (#11278) a number of definitions and results in `LinearAlgebra/BilinearForm/Hom` are essentially just the identity. This PR deprecates these results.



Co-authored-by: Christopher Hoskin <[email protected]>

Mathlib/LinearAlgebra/BilinearForm/Hom.lean

@@ -60,14 +60,18 @@ 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. -/
+@[deprecated]
 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. -/
+@[deprecated]
 def toLinHom : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R := LinearMap.id
 #align bilin_form.to_lin_hom LinearMap.BilinForm.toLinHom
 
+set_option linter.deprecated false in
+@[deprecated]
 theorem toLin'_apply (A : BilinForm R M) (x : M) : toLinHom (M := M) A x = A x :=
   rfl
 #align bilin_form.to_lin'_apply LinearMap.BilinForm.toLin'_apply
@@ -76,7 +80,7 @@ variable (B)
 
 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 (M := M) B).map_sum₂ t g w
+  B.map_sum₂ t g w
 #align bilin_form.sum_left LinearMap.BilinForm.sum_left
 
 variable (w : M)
@@ -94,7 +98,7 @@ variable {B}
 /-- The linear map obtained from a `BilinForm` by fixing the right co-ordinate and evaluating in
 the left. -/
 def toLinHomFlip : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R :=
-  toLinHom.comp flipHom.toLinearMap
+  flipHom.toLinearMap
 #align bilin_form.to_lin_hom_flip LinearMap.BilinForm.toLinHomFlip
 
 theorem toLin'Flip_apply (A : BilinForm R M) (x : M) : toLinHomFlip (M := M) A x = fun y => A y x :=
@@ -116,43 +120,51 @@ This is an auxiliary definition for the full linear equivalence `LinearMap.toBil
 def LinearMap.toBilinAux (f : M →ₗ[R] M →ₗ[R] R) : BilinForm R M := f
 #align linear_map.to_bilin_aux LinearMap.toBilinAux
 
+set_option linter.deprecated false in
 /-- Bilinear forms are linearly equivalent to maps with two arguments that are linear in both. -/
+@[deprecated]
 def LinearMap.BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R] R :=
   { BilinForm.toLinHom with
     invFun := LinearMap.toBilinAux
     left_inv := fun _ => rfl
     right_inv := fun _ => rfl }
 #align bilin_form.to_lin LinearMap.BilinForm.toLin
 
+set_option linter.deprecated false in
 /-- A map with two arguments that is linear in both is linearly equivalent to bilinear form. -/
+@[deprecated]
 def LinearMap.toBilin : (M →ₗ[R] M →ₗ[R] R) ≃ₗ[R] BilinForm R M :=
   BilinForm.toLin.symm
 #align linear_map.to_bilin LinearMap.toBilin
 
-@[simp]
+@[deprecated]
 theorem LinearMap.toBilinAux_eq (f : M →ₗ[R] M →ₗ[R] R) :
-    LinearMap.toBilinAux f = LinearMap.toBilin f :=
+    LinearMap.toBilinAux f = f :=
   rfl
 #align linear_map.to_bilin_aux_eq LinearMap.toBilinAux_eq
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated]
 theorem LinearMap.toBilin_symm :
     (LinearMap.toBilin.symm : BilinForm R M ≃ₗ[R] _) = BilinForm.toLin :=
   rfl
 #align linear_map.to_bilin_symm LinearMap.toBilin_symm
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated]
 theorem BilinForm.toLin_symm :
     (BilinForm.toLin.symm : _ ≃ₗ[R] BilinForm R M) = LinearMap.toBilin :=
   LinearMap.toBilin.symm_symm
 #align bilin_form.to_lin_symm BilinForm.toLin_symm
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated]
 theorem LinearMap.toBilin_apply (f : M →ₗ[R] M →ₗ[R] R) (x y : M) :
     toBilin f x y = f x y :=
   rfl
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated]
 theorem BilinForm.toLin_apply (x : M) : BilinForm.toLin B x = B x :=
   rfl
 #align bilin_form.to_lin_apply BilinForm.toLin_apply

Mathlib/LinearAlgebra/BilinearForm/Properties.lean

@@ -417,7 +417,7 @@ theorem nondegenerate_iff_ker_eq_bot {B : BilinForm R M} :
 #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) = ⊥ :=
+    LinearMap.ker B = ⊥ :=
   nondegenerate_iff_ker_eq_bot.mp h
 #align bilin_form.nondegenerate.ker_eq_bot LinearMap.BilinForm.Nondegenerate.ker_eq_bot
 
@@ -507,8 +507,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 ↦ ?_))
-  simp_rw [BilinForm.toLin_apply, apply_dualBasis_left, ← B.flip_apply,
-    apply_dualBasis_left, @eq_comm _ i j]
+  simp_rw [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) {ι}
@@ -531,7 +530,7 @@ section LinearAdjoints
 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₁)
+  (B₂.toDual b₂).symm.toLinearMap.comp B₁
 #align bilin_form.symm_comp_of_nondegenerate LinearMap.BilinForm.symmCompOfNondegenerate
 
 theorem comp_symmCompOfNondegenerate_apply (B₁ : BilinForm K V) {B₂ : BilinForm K V}
@@ -540,7 +539,6 @@ theorem comp_symmCompOfNondegenerate_apply (B₁ : BilinForm K V) {B₂ : BilinF
   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]

Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

@@ -62,7 +62,7 @@ open Matrix
 
 This is an auxiliary definition for the equivalence `Matrix.toBilin'`. -/
 def Matrix.toBilin'Aux [Fintype n] (M : Matrix n n R₂) : BilinForm R₂ (n → R₂) :=
-  LinearMap.toBilin (Matrix.toLinearMap₂'Aux _ _ M)
+  Matrix.toLinearMap₂'Aux _ _ M
 #align matrix.to_bilin'_aux Matrix.toBilin'Aux
 
 theorem Matrix.toBilin'Aux_stdBasis [Fintype n] [DecidableEq n] (M : Matrix n n R₂) (i j : n) :
@@ -75,7 +75,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
+  LinearMap.toMatrix₂Aux b b
 #align bilin_form.to_matrix_aux BilinForm.toMatrixAux
 
 @[simp]
@@ -91,11 +91,8 @@ theorem toBilin'Aux_toMatrixAux [DecidableEq n] (B₂ : BilinForm R₂ (n → R
     -- Porting note: had to hint the base ring even though it should be clear from context...
     Matrix.toBilin'Aux (BilinForm.toMatrixAux (R₂ := R₂)
       (fun j => stdBasis R₂ (fun _ => R₂) j 1) B₂) = B₂ := by
-  rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux, coe_comp, Function.comp_apply,
+  rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux,
     toLinearMap₂'Aux_toMatrix₂Aux]
-  ext x y
-  simp only [coe_comp, coe_single, Function.comp_apply, toBilin_apply]
-  rfl
 #align to_bilin'_aux_to_matrix_aux toBilin'Aux_toMatrixAux
 
 section ToMatrix'
@@ -236,7 +233,7 @@ variable [DecidableEq n] (b : Basis n R₂ M₂)
 /-- `BilinForm.toMatrix b` is the equivalence between `R`-bilinear forms on `M` and
 `n`-by-`n` matrices with entries in `R`, if `b` is an `R`-basis for `M`. -/
 noncomputable def BilinForm.toMatrix : BilinForm R₂ M₂ ≃ₗ[R₂] Matrix n n R₂ :=
-  BilinForm.toLin ≪≫ₗ (LinearMap.toMatrix₂ b b)
+  LinearMap.toMatrix₂ b b
 #align bilin_form.to_matrix BilinForm.toMatrix
 
 /-- `BilinForm.toMatrix b` is the equivalence between `R`-bilinear forms on `M` and
@@ -282,7 +279,6 @@ theorem Matrix.toBilin_basisFun : Matrix.toBilin (Pi.basisFun R₂ n) = Matrix.t
 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]
@@ -343,11 +339,8 @@ theorem BilinForm.toMatrix_mul (B : BilinForm R₂ M₂) (M : Matrix n n R₂) :
 theorem Matrix.toBilin_comp (M : Matrix n n R₂) (P Q : Matrix n o R₂) :
     (Matrix.toBilin b M).comp (toLin c b P) (toLin c b Q) = Matrix.toBilin c (Pᵀ * M * Q) := by
   ext x y
-  rw [Matrix.toBilin,
-    BilinForm.toMatrix, Matrix.toBilin, BilinForm.toMatrix, LinearEquiv.trans_symm,
-    LinearEquiv.trans_symm, toMatrix₂_symm, BilinForm.toLin_symm, LinearEquiv.trans_apply,
-    toMatrix₂_symm, BilinForm.toLin_symm, LinearEquiv.trans_apply,
-    ← Matrix.toLinearMap₂_compl₁₂ b b c c]
+  rw [Matrix.toBilin, BilinForm.toMatrix, Matrix.toBilin, BilinForm.toMatrix, toMatrix₂_symm,
+    toMatrix₂_symm, ← Matrix.toLinearMap₂_compl₁₂ b b c c]
   simp
 #align matrix.to_bilin_comp Matrix.toBilin_comp
 

Mathlib/RingTheory/Trace.lean

@@ -190,8 +190,8 @@ variable (R S)
 /-- The `traceForm` maps `x y : S` to the trace of `x * y`.
 It is a symmetric bilinear form and is nondegenerate if the extension is separable. -/
 noncomputable def traceForm : BilinForm R S :=
-  -- Porting note: dot notation `().toBilin` does not work anymore.
-  LinearMap.toBilin (LinearMap.compr₂ (lmul R S).toLinearMap (trace R S))
+-- Porting note: dot notation `().toBilin` does not work anymore.
+  LinearMap.compr₂ (lmul R S).toLinearMap (trace R S)
 #align algebra.trace_form Algebra.traceForm
 
 variable {S}