From b9cabefa8868ba500a1de5e4d0d5051464a0a5a7 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 18:06:07 +0000 Subject: [PATCH] refactor(LinearAlgebra/QuadraticForm): rename `Isometry` to `IsometryEquiv` (#6305) This is consistent with `LinearIsometryEquiv` vs `LinearIsometry`. The motivation is to make room for `QuadraticForm.Isometry` as the homomorphism. --- Mathlib.lean | 2 +- .../LinearAlgebra/CliffordAlgebra/Basic.lean | 10 +-- .../LinearAlgebra/QuadraticForm/Complex.lean | 20 ++--- .../{Isometry.lean => IsometryEquiv.lean} | 86 ++++++++++--------- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean | 25 +++--- Mathlib/LinearAlgebra/QuadraticForm/Real.lean | 14 +-- 6 files changed, 81 insertions(+), 76 deletions(-) rename Mathlib/LinearAlgebra/QuadraticForm/{Isometry.lean => IsometryEquiv.lean} (64%) diff --git a/Mathlib.lean b/Mathlib.lean index 0cb9af45ba47c..f1d92acdb5a55 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2227,7 +2227,7 @@ import Mathlib.LinearAlgebra.ProjectiveSpace.Independence import Mathlib.LinearAlgebra.ProjectiveSpace.Subspace import Mathlib.LinearAlgebra.QuadraticForm.Basic import Mathlib.LinearAlgebra.QuadraticForm.Complex -import Mathlib.LinearAlgebra.QuadraticForm.Isometry +import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv import Mathlib.LinearAlgebra.QuadraticForm.Prod import Mathlib.LinearAlgebra.QuadraticForm.Real import Mathlib.LinearAlgebra.Quotient diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean index 760b6668c5c94..949d57f145924 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean @@ -5,7 +5,7 @@ Authors: Eric Wieser, Utensil Song -/ import Mathlib.Algebra.RingQuot import Mathlib.LinearAlgebra.TensorAlgebra.Basic -import Mathlib.LinearAlgebra.QuadraticForm.Isometry +import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv #align_import linear_algebra.clifford_algebra.basic from "leanprover-community/mathlib"@"d46774d43797f5d1f507a63a6e904f7a533ae74a" @@ -315,7 +315,7 @@ variable {Q₁ Q₂ Q₃} /-- Two `CliffordAlgebra`s are equivalent as algebras if their quadratic forms are equivalent. -/ @[simps! apply] -def equivOfIsometry (e : Q₁.Isometry Q₂) : CliffordAlgebra Q₁ ≃ₐ[R] CliffordAlgebra Q₂ := +def equivOfIsometry (e : Q₁.IsometryEquiv Q₂) : CliffordAlgebra Q₁ ≃ₐ[R] CliffordAlgebra Q₂ := AlgEquiv.ofAlgHom (map Q₁ Q₂ e e.map_app) (map Q₂ Q₁ e.symm e.symm.map_app) ((map_comp_map _ _ _ _ _ _ _).trans <| by convert map_id Q₂ using 2 -- porting note: replaced `_` with `Q₂` @@ -328,13 +328,13 @@ def equivOfIsometry (e : Q₁.Isometry Q₂) : CliffordAlgebra Q₁ ≃ₐ[R] Cl #align clifford_algebra.equiv_of_isometry CliffordAlgebra.equivOfIsometry @[simp] -theorem equivOfIsometry_symm (e : Q₁.Isometry Q₂) : +theorem equivOfIsometry_symm (e : Q₁.IsometryEquiv Q₂) : (equivOfIsometry e).symm = equivOfIsometry e.symm := rfl #align clifford_algebra.equiv_of_isometry_symm CliffordAlgebra.equivOfIsometry_symm @[simp] -theorem equivOfIsometry_trans (e₁₂ : Q₁.Isometry Q₂) (e₂₃ : Q₂.Isometry Q₃) : +theorem equivOfIsometry_trans (e₁₂ : Q₁.IsometryEquiv Q₂) (e₂₃ : Q₂.IsometryEquiv Q₃) : (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃) := by ext x exact AlgHom.congr_fun (map_comp_map Q₁ Q₂ Q₃ _ _ _ _) x @@ -342,7 +342,7 @@ theorem equivOfIsometry_trans (e₁₂ : Q₁.Isometry Q₂) (e₂₃ : Q₂.Iso @[simp] theorem equivOfIsometry_refl : - (equivOfIsometry <| QuadraticForm.Isometry.refl Q₁) = AlgEquiv.refl := by + (equivOfIsometry <| QuadraticForm.IsometryEquiv.refl Q₁) = AlgEquiv.refl := by ext x exact AlgHom.congr_fun (map_id Q₁) x #align clifford_algebra.equiv_of_isometry_refl CliffordAlgebra.equivOfIsometry_refl diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean index c39a0a6ba379d..23831c622fa0a 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean @@ -3,7 +3,7 @@ Copyright (c) 2020 Anne Baanen. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Anne Baanen, Kexing Ying, Eric Wieser -/ -import Mathlib.LinearAlgebra.QuadraticForm.Isometry +import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv import Mathlib.Analysis.SpecialFunctions.Pow.Complex #align_import linear_algebra.quadratic_form.complex from "leanprover-community/mathlib"@"0b9eaaa7686280fad8cce467f5c3c57ee6ce77f8" @@ -27,14 +27,14 @@ variable {ι : Type _} [Fintype ι] /-- The isometry between a weighted sum of squares on the complex numbers and the sum of squares, i.e. `weightedSumSquares` with weights 1 or 0. -/ -noncomputable def isometrySumSquares [DecidableEq ι] (w' : ι → ℂ) : - Isometry (weightedSumSquares ℂ w') +noncomputable def isometryEquivSumSquares [DecidableEq ι] (w' : ι → ℂ) : + IsometryEquiv (weightedSumSquares ℂ w') (weightedSumSquares ℂ (fun i => if w' i = 0 then 0 else 1 : ι → ℂ)) := by let w i := if h : w' i = 0 then (1 : Units ℂ) else Units.mk0 (w' i) h have hw' : ∀ i : ι, (w i : ℂ) ^ (-(1 / 2 : ℂ)) ≠ 0 := by intro i hi exact (w i).ne_zero ((Complex.cpow_eq_zero_iff _ _).1 hi).1 - convert (weightedSumSquares ℂ w').isometryBasisRepr + convert (weightedSumSquares ℂ w').isometryEquivBasisRepr ((Pi.basisFun ℂ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hw' i).unit) ext1 v erw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply] @@ -60,14 +60,14 @@ noncomputable def isometrySumSquares [DecidableEq ι] (w' : ι → ℂ) : rw [this]; ring rw [← Complex.cpow_add _ _ (w j).ne_zero, show -(1 / 2 : ℂ) + -(1 / 2) = -1 by simp [← two_mul], Complex.cpow_neg_one, inv_mul_cancel (w j).ne_zero, one_mul] -#align quadratic_form.isometry_sum_squares QuadraticForm.isometrySumSquares +#align quadratic_form.isometry_sum_squares QuadraticForm.isometryEquivSumSquares /-- The isometry between a weighted sum of squares on the complex numbers and the sum of squares, i.e. `weightedSumSquares` with weight `fun (i : ι) => 1`. -/ -noncomputable def isometrySumSquaresUnits [DecidableEq ι] (w : ι → Units ℂ) : - Isometry (weightedSumSquares ℂ w) (weightedSumSquares ℂ (1 : ι → ℂ)) := by - simpa using isometrySumSquares ((↑) ∘ w) -#align quadratic_form.isometry_sum_squares_units QuadraticForm.isometrySumSquaresUnits +noncomputable def isometryEquivSumSquaresUnits [DecidableEq ι] (w : ι → Units ℂ) : + IsometryEquiv (weightedSumSquares ℂ w) (weightedSumSquares ℂ (1 : ι → ℂ)) := by + simpa using isometryEquivSumSquares ((↑) ∘ w) +#align quadratic_form.isometry_sum_squares_units QuadraticForm.isometryEquivSumSquaresUnits /-- A nondegenerate quadratic form on the complex numbers is equivalent to the sum of squares, i.e. `weightedSumSquares` with weight `fun (i : ι) => 1`. -/ @@ -75,7 +75,7 @@ theorem equivalent_sum_squares {M : Type _} [AddCommGroup M] [Module ℂ M] [Fin (Q : QuadraticForm ℂ M) (hQ : (associated (R₁ := ℂ) Q).Nondegenerate) : Equivalent Q (weightedSumSquares ℂ (1 : Fin (FiniteDimensional.finrank ℂ M) → ℂ)) := let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ - ⟨hw₁.trans (isometrySumSquaresUnits w)⟩ + ⟨hw₁.trans (isometryEquivSumSquaresUnits w)⟩ #align quadratic_form.equivalent_sum_squares QuadraticForm.equivalent_sum_squares /-- All nondegenerate quadratic forms on the complex numbers are equivalent. -/ diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean b/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean similarity index 64% rename from Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean rename to Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean index 85037258d5a42..1f07c1e32208c 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean @@ -8,11 +8,11 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic #align_import linear_algebra.quadratic_form.isometry from "leanprover-community/mathlib"@"14b69e9f3c16630440a2cbd46f1ddad0d561dee7" /-! -# Isometries with respect to quadratic forms +# Isometric equivalences with respect to quadratic forms ## Main definitions -* `QuadraticForm.Isometry`: `LinearEquiv`s which map between two different quadratic forms +* `QuadraticForm.IsometryEquiv`: `LinearEquiv`s which map between two different quadratic forms * `QuadraticForm.Equivalent`: propositional version of the above ## Main results @@ -32,33 +32,34 @@ variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMon variable [Module R M] [Module R M₁] [Module R M₂] [Module R M₃] -/-- An isometry between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`, +/-- An isometric equivalence between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`, is a linear equivalence between `M₁` and `M₂` that commutes with the quadratic forms. -/ -- Porting note: not implemented @[nolint has_nonempty_instance] -structure Isometry (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) extends M₁ ≃ₗ[R] M₂ where +structure IsometryEquiv (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) + extends M₁ ≃ₗ[R] M₂ where map_app' : ∀ m, Q₂ (toFun m) = Q₁ m -#align quadratic_form.isometry QuadraticForm.Isometry +#align quadratic_form.isometry QuadraticForm.IsometryEquiv /-- Two quadratic forms over a ring `R` are equivalent -if there exists an isometry between them: +if there exists an isometric equivalence between them: a linear equivalence that transforms one quadratic form into the other. -/ -def Equivalent (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) := - Nonempty (Q₁.Isometry Q₂) +def Equivalent (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : Prop := + Nonempty (Q₁.IsometryEquiv Q₂) #align quadratic_form.equivalent QuadraticForm.Equivalent -namespace Isometry +namespace IsometryEquiv variable {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} -- Porting note: was `Coe` -instance : CoeOut (Q₁.Isometry Q₂) (M₁ ≃ₗ[R] M₂) := - ⟨Isometry.toLinearEquiv⟩ +instance : CoeOut (Q₁.IsometryEquiv Q₂) (M₁ ≃ₗ[R] M₂) := + ⟨IsometryEquiv.toLinearEquiv⟩ -- Porting note: syntaut #noalign quadratic_form.isometry.to_linear_equiv_eq_coe --Porting note: replace `CoeFun` with `EquivLike` -instance : EquivLike (Q₁.Isometry Q₂) M₁ M₂ := +instance : EquivLike (Q₁.IsometryEquiv Q₂) M₁ M₂ := { coe := fun f => ⇑(f : M₁ ≃ₗ[R] M₂), inv := fun f => ⇑(f : M₁ ≃ₗ[R] M₂).symm, left_inv := fun f => (f : M₁ ≃ₗ[R] M₂).left_inv @@ -66,36 +67,36 @@ instance : EquivLike (Q₁.Isometry Q₂) M₁ M₂ := coe_injective' := fun f g => by cases f; cases g; simp (config := {contextual := true}) } @[simp] -theorem coe_toLinearEquiv (f : Q₁.Isometry Q₂) : ⇑(f : M₁ ≃ₗ[R] M₂) = f := +theorem coe_toLinearEquiv (f : Q₁.IsometryEquiv Q₂) : ⇑(f : M₁ ≃ₗ[R] M₂) = f := rfl -#align quadratic_form.isometry.coe_to_linear_equiv QuadraticForm.Isometry.coe_toLinearEquiv +#align quadratic_form.isometry.coe_to_linear_equiv QuadraticForm.IsometryEquiv.coe_toLinearEquiv @[simp] -theorem map_app (f : Q₁.Isometry Q₂) (m : M₁) : Q₂ (f m) = Q₁ m := +theorem map_app (f : Q₁.IsometryEquiv Q₂) (m : M₁) : Q₂ (f m) = Q₁ m := f.map_app' m -#align quadratic_form.isometry.map_app QuadraticForm.Isometry.map_app +#align quadratic_form.isometry.map_app QuadraticForm.IsometryEquiv.map_app -/-- The identity isometry from a quadratic form to itself. -/ +/-- The identity isometric equivalence between a quadratic form and itself. -/ @[refl] -def refl (Q : QuadraticForm R M) : Q.Isometry Q := +def refl (Q : QuadraticForm R M) : Q.IsometryEquiv Q := { LinearEquiv.refl R M with map_app' := fun _ => rfl } -#align quadratic_form.isometry.refl QuadraticForm.Isometry.refl +#align quadratic_form.isometry.refl QuadraticForm.IsometryEquiv.refl -/-- The inverse isometry of an isometry between two quadratic forms. -/ +/-- The inverse isometric equivalence of an isometric equivalence between two quadratic forms. -/ @[symm] -def symm (f : Q₁.Isometry Q₂) : Q₂.Isometry Q₁ := +def symm (f : Q₁.IsometryEquiv Q₂) : Q₂.IsometryEquiv Q₁ := { (f : M₁ ≃ₗ[R] M₂).symm with map_app' := by intro m; rw [← f.map_app]; congr; exact f.toLinearEquiv.apply_symm_apply m } -#align quadratic_form.isometry.symm QuadraticForm.Isometry.symm +#align quadratic_form.isometry.symm QuadraticForm.IsometryEquiv.symm -/-- The composition of two isometries between quadratic forms. -/ +/-- The composition of two isometric equivalences between quadratic forms. -/ @[trans] -def trans (f : Q₁.Isometry Q₂) (g : Q₂.Isometry Q₃) : Q₁.Isometry Q₃ := +def trans (f : Q₁.IsometryEquiv Q₂) (g : Q₂.IsometryEquiv Q₃) : Q₁.IsometryEquiv Q₃ := { (f : M₁ ≃ₗ[R] M₂).trans (g : M₂ ≃ₗ[R] M₃) with map_app' := by intro m; rw [← f.map_app, ← g.map_app]; rfl } -#align quadratic_form.isometry.trans QuadraticForm.Isometry.trans +#align quadratic_form.isometry.trans QuadraticForm.IsometryEquiv.trans -end Isometry +end IsometryEquiv namespace Equivalent @@ -103,7 +104,7 @@ variable {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : Qua @[refl] theorem refl (Q : QuadraticForm R M) : Q.Equivalent Q := - ⟨Isometry.refl Q⟩ + ⟨IsometryEquiv.refl Q⟩ #align quadratic_form.equivalent.refl QuadraticForm.Equivalent.refl @[symm] @@ -121,33 +122,34 @@ end Equivalent variable [Fintype ι] {v : Basis ι R M} /-- A quadratic form composed with a `LinearEquiv` is isometric to itself. -/ -def isometryOfCompLinearEquiv (Q : QuadraticForm R M) (f : M₁ ≃ₗ[R] M) : - Q.Isometry (Q.comp (f : M₁ →ₗ[R] M)) := +def isometryEquivOfCompLinearEquiv (Q : QuadraticForm R M) (f : M₁ ≃ₗ[R] M) : + Q.IsometryEquiv (Q.comp (f : M₁ →ₗ[R] M)) := { f.symm with map_app' := by intro simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe, LinearEquiv.apply_symm_apply, f.apply_symm_apply] } -#align quadratic_form.isometry_of_comp_linear_equiv QuadraticForm.isometryOfCompLinearEquiv +#align quadratic_form.isometry_of_comp_linear_equiv QuadraticForm.isometryEquivOfCompLinearEquiv -/-- A quadratic form is isometric to its bases representations. -/ -noncomputable def isometryBasisRepr (Q : QuadraticForm R M) (v : Basis ι R M) : - Isometry Q (Q.basisRepr v) := - isometryOfCompLinearEquiv Q v.equivFun.symm -#align quadratic_form.isometry_basis_repr QuadraticForm.isometryBasisRepr +/-- A quadratic form is isometrically equivalent to its bases representations. -/ +noncomputable def isometryEquivBasisRepr (Q : QuadraticForm R M) (v : Basis ι R M) : + IsometryEquiv Q (Q.basisRepr v) := + isometryEquivOfCompLinearEquiv Q v.equivFun.symm +#align quadratic_form.isometry_basis_repr QuadraticForm.isometryEquivBasisRepr variable [Field K] [Invertible (2 : K)] [AddCommGroup V] [Module K V] -/-- Given an orthogonal basis, a quadratic form is isometric with a weighted sum of squares. -/ -noncomputable def isometryWeightedSumSquares (Q : QuadraticForm K V) +/-- Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of +squares. -/ +noncomputable def isometryEquivWeightedSumSquares (Q : QuadraticForm K V) (v : Basis (Fin (FiniteDimensional.finrank K V)) K V) (hv₁ : (associated (R₁ := K) Q).iIsOrtho v) : - Q.Isometry (weightedSumSquares K fun i => Q (v i)) := by - let iso := Q.isometryBasisRepr v + Q.IsometryEquiv (weightedSumSquares K fun i => Q (v i)) := by + let iso := Q.isometryEquivBasisRepr v refine' ⟨iso, fun m => _⟩ convert iso.map_app m rw [basisRepr_eq_of_iIsOrtho _ _ hv₁] -#align quadratic_form.isometry_weighted_sum_squares QuadraticForm.isometryWeightedSumSquares +#align quadratic_form.isometry_weighted_sum_squares QuadraticForm.isometryEquivWeightedSumSquares variable [FiniteDimensional K V] @@ -156,7 +158,7 @@ open BilinForm theorem equivalent_weightedSumSquares (Q : QuadraticForm K V) : ∃ w : Fin (FiniteDimensional.finrank K V) → K, Equivalent Q (weightedSumSquares K w) := let ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm _ Q) - ⟨_, ⟨Q.isometryWeightedSumSquares v hv₁⟩⟩ + ⟨_, ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩ #align quadratic_form.equivalent_weighted_sum_squares QuadraticForm.equivalent_weightedSumSquares theorem equivalent_weightedSumSquares_units_of_nondegenerate' (Q : QuadraticForm K V) @@ -165,7 +167,7 @@ theorem equivalent_weightedSumSquares_units_of_nondegenerate' (Q : QuadraticForm obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q) have hv₂ := hv₁.not_isOrtho_basis_self_of_nondegenerate hQ simp_rw [IsOrtho, associated_eq_self_apply] at hv₂ - exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryWeightedSumSquares v hv₁⟩⟩ + exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩ #align quadratic_form.equivalent_weighted_sum_squares_units_of_nondegenerate' QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate' end QuadraticForm diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean index 56ad5c8f78783..9451e33e9dfcd 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Eric Wieser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ -import Mathlib.LinearAlgebra.QuadraticForm.Isometry +import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv #align_import linear_algebra.quadratic_form.prod from "leanprover-community/mathlib"@"9b2755b951bc323c962bd072cd447b375cf58101" @@ -58,17 +58,19 @@ def prod (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : Quadratic /-- An isometry between quadratic forms generated by `QuadraticForm.prod` can be constructed from a pair of isometries between the left and right parts. -/ @[simps toLinearEquiv] -def Isometry.prod {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₁' : QuadraticForm R N₁} - {Q₂' : QuadraticForm R N₂} (e₁ : Q₁.Isometry Q₁') (e₂ : Q₂.Isometry Q₂') : - (Q₁.prod Q₂).Isometry (Q₁'.prod Q₂') where +def IsometryEquiv.prod + {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} + {Q₁' : QuadraticForm R N₁} {Q₂' : QuadraticForm R N₂} + (e₁ : Q₁.IsometryEquiv Q₁') (e₂ : Q₂.IsometryEquiv Q₂') : + (Q₁.prod Q₂).IsometryEquiv (Q₁'.prod Q₂') where map_app' x := congr_arg₂ (· + ·) (e₁.map_app x.1) (e₂.map_app x.2) toLinearEquiv := LinearEquiv.prod e₁.toLinearEquiv e₂.toLinearEquiv -#align quadratic_form.isometry.prod QuadraticForm.Isometry.prod +#align quadratic_form.isometry.prod QuadraticForm.IsometryEquiv.prod theorem Equivalent.prod {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₁' : QuadraticForm R N₁} {Q₂' : QuadraticForm R N₂} (e₁ : Q₁.Equivalent Q₁') (e₂ : Q₂.Equivalent Q₂') : (Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂') := - Nonempty.map2 Isometry.prod e₁ e₂ + Nonempty.map2 IsometryEquiv.prod e₁ e₂ #align quadratic_form.equivalent.prod QuadraticForm.Equivalent.prod /-- If a product is anisotropic then its components must be. The converse is not true. -/ @@ -132,18 +134,19 @@ theorem pi_apply [Fintype ι] (Q : ∀ i, QuadraticForm R (Mᵢ i)) (x : ∀ i, /-- An isometry between quadratic forms generated by `QuadraticForm.pi` can be constructed from a pair of isometries between the left and right parts. -/ @[simps toLinearEquiv] -def Isometry.pi [Fintype ι] {Q : ∀ i, QuadraticForm R (Mᵢ i)} {Q' : ∀ i, QuadraticForm R (Nᵢ i)} - (e : ∀ i, (Q i).Isometry (Q' i)) : (pi Q).Isometry (pi Q') where +def IsometryEquiv.pi [Fintype ι] + {Q : ∀ i, QuadraticForm R (Mᵢ i)} {Q' : ∀ i, QuadraticForm R (Nᵢ i)} + (e : ∀ i, (Q i).IsometryEquiv (Q' i)) : (pi Q).IsometryEquiv (pi Q') where map_app' x := by simp only [pi_apply, LinearEquiv.piCongrRight, LinearEquiv.toFun_eq_coe, - Isometry.coe_toLinearEquiv, Isometry.map_app] + IsometryEquiv.coe_toLinearEquiv, IsometryEquiv.map_app] toLinearEquiv := LinearEquiv.piCongrRight fun i => (e i : Mᵢ i ≃ₗ[R] Nᵢ i) -#align quadratic_form.isometry.pi QuadraticForm.Isometry.pi +#align quadratic_form.isometry.pi QuadraticForm.IsometryEquiv.pi theorem Equivalent.pi [Fintype ι] {Q : ∀ i, QuadraticForm R (Mᵢ i)} {Q' : ∀ i, QuadraticForm R (Nᵢ i)} (e : ∀ i, (Q i).Equivalent (Q' i)) : (pi Q).Equivalent (pi Q') := - ⟨Isometry.pi fun i => Classical.choice (e i)⟩ + ⟨IsometryEquiv.pi fun i => Classical.choice (e i)⟩ #align quadratic_form.equivalent.pi QuadraticForm.Equivalent.pi /-- If a family is anisotropic then its components must be. The converse is not true. -/ diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Real.lean b/Mathlib/LinearAlgebra/QuadraticForm/Real.lean index 26d9a21c7a77f..f40d0a268407e 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Real.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Real.lean @@ -3,7 +3,7 @@ Copyright (c) 2020 Anne Baanen. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Anne Baanen, Kexing Ying, Eric Wieser -/ -import Mathlib.LinearAlgebra.QuadraticForm.Isometry +import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Data.Real.Sign @@ -32,14 +32,14 @@ variable {ι : Type _} [Fintype ι] /-- The isometry between a weighted sum of squares with weights `u` on the (non-zero) real numbers and the weighted sum of squares with weights `sign ∘ u`. -/ -noncomputable def isometrySignWeightedSumSquares [DecidableEq ι] (w : ι → ℝ) : - Isometry (weightedSumSquares ℝ w) (weightedSumSquares ℝ (Real.sign ∘ w)) := by +noncomputable def isometryEquivSignWeightedSumSquares [DecidableEq ι] (w : ι → ℝ) : + IsometryEquiv (weightedSumSquares ℝ w) (weightedSumSquares ℝ (Real.sign ∘ w)) := by let u i := if h : w i = 0 then (1 : ℝˣ) else Units.mk0 (w i) h have hu' : ∀ i : ι, (Real.sign (u i) * u i) ^ (-(1 / 2 : ℝ)) ≠ 0 := by intro i refine' (ne_of_lt (Real.rpow_pos_of_pos (sign_mul_pos_of_ne_zero _ <| Units.ne_zero _) _)).symm convert - (weightedSumSquares ℝ w).isometryBasisRepr + (weightedSumSquares ℝ w).isometryEquivBasisRepr ((Pi.basisFun ℝ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hu' i).unit) ext1 v rw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply] @@ -73,7 +73,7 @@ noncomputable def isometrySignWeightedSumSquares [DecidableEq ι] (w : ι → rw [← Real.rpow_add (sign_mul_pos_of_ne_zero _ <| Units.ne_zero _), show -(1 / 2 : ℝ) + -(1 / 2) = -1 by ring, Real.rpow_neg_one, mul_inv, inv_sign, mul_assoc (Real.sign (u j)) (u j)⁻¹, inv_mul_cancel (Units.ne_zero _), mul_one] -#align quadratic_form.isometry_sign_weighted_sum_squares QuadraticForm.isometrySignWeightedSumSquares +#align quadratic_form.isometry_sign_weighted_sum_squares QuadraticForm.isometryEquivSignWeightedSumSquares /-- **Sylvester's law of inertia**: A nondegenerate real quadratic form is equivalent to a weighted sum of squares with the weights being ±1. -/ @@ -83,7 +83,7 @@ theorem equivalent_one_neg_one_weighted_sum_squared {M : Type _} [AddCommGroup M (∀ i, w i = -1 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) := let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ ⟨Real.sign ∘ ((↑) : ℝˣ → ℝ) ∘ w, fun i => sign_apply_eq_of_ne_zero (w i) (w i).ne_zero, - ⟨hw₁.trans (isometrySignWeightedSumSquares (((↑) : ℝˣ → ℝ) ∘ w))⟩⟩ + ⟨hw₁.trans (isometryEquivSignWeightedSumSquares (((↑) : ℝˣ → ℝ) ∘ w))⟩⟩ #align quadratic_form.equivalent_one_neg_one_weighted_sum_squared QuadraticForm.equivalent_one_neg_one_weighted_sum_squared /-- **Sylvester's law of inertia**: A real quadratic form is equivalent to a weighted @@ -94,7 +94,7 @@ theorem equivalent_one_zero_neg_one_weighted_sum_squared {M : Type _} [AddCommGr (∀ i, w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) := let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares ⟨Real.sign ∘ ((↑) : ℝ → ℝ) ∘ w, fun i => sign_apply_eq (w i), - ⟨hw₁.trans (isometrySignWeightedSumSquares w)⟩⟩ + ⟨hw₁.trans (isometryEquivSignWeightedSumSquares w)⟩⟩ #align quadratic_form.equivalent_one_zero_neg_one_weighted_sum_squared QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared end QuadraticForm