diff --git a/Counterexamples/CliffordAlgebraNotInjective.lean b/Counterexamples/CliffordAlgebraNotInjective.lean index a6600e548440aa..e490b767ffde14 100644 --- a/Counterexamples/CliffordAlgebraNotInjective.lean +++ b/Counterexamples/CliffordAlgebraNotInjective.lean @@ -37,6 +37,7 @@ are quadratic forms that cannot be expressed via even non-symmetric bilinear for noncomputable section open LinearMap (BilinForm) +open LinearMap (BilinMap) namespace Q60596 @@ -149,7 +150,7 @@ abbrev L : Type _ := _ ⧸ LinearMap.ker lFunc /-- The quadratic form corresponding to squaring a single coefficient. -/ def sq {ι R : Type*} [CommRing R] (i : ι) : QuadraticForm R (ι → R) := - QuadraticForm.sq.comp <| LinearMap.proj i + QuadraticMap.sq.comp <| LinearMap.proj i theorem sq_map_add_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a b : ι → R) : sq i (a + b) = sq i a + sq i b := @@ -165,10 +166,10 @@ def Q' : QuadraticForm K (Fin 3 → K) := ∑ i, sq i theorem Q'_add (x y : Fin 3 → K) : Q' (x + y) = Q' x + Q' y := by - simp only [Q', QuadraticForm.sum_apply, sq_map_add_char_two, Finset.sum_add_distrib] + simp only [Q', QuadraticMap.sum_apply, sq_map_add_char_two, Finset.sum_add_distrib] theorem Q'_sub (x y : Fin 3 → K) : Q' (x - y) = Q' x - Q' y := by - simp only [Q', QuadraticForm.sum_apply, sq_map_sub_char_two, Finset.sum_sub_distrib] + simp only [Q', QuadraticMap.sum_apply, sq_map_sub_char_two, Finset.sum_sub_distrib] theorem Q'_apply (a : Fin 3 → K) : Q' a = a 0 * a 0 + a 1 * a 1 + a 2 * a 2 := calc @@ -204,7 +205,7 @@ theorem Q'_zero_under_ideal (v : Fin 3 → K) (hv : v ∈ LinearMap.ker lFunc) : /-- `Q'`, lifted to operate on the quotient space `L`. -/ @[simps!] def Q : QuadraticForm K L := - QuadraticForm.ofPolar + QuadraticMap.ofPolar (fun x => Quotient.liftOn' x Q' fun a b h => by rw [Submodule.quotientRel_r_def] at h @@ -263,7 +264,7 @@ theorem algebraMap_not_injective : ¬Function.Injective (algebraMap K <| Cliffor fun h => αβγ_ne_zero <| h <| by rw [algebraMap_αβγ_eq_zero, RingHom.map_zero] /-- Bonus counterexample: `Q` is a quadratic form that has no bilinear form. -/ -theorem Q_not_in_range_toQuadraticForm : Q ∉ Set.range BilinForm.toQuadraticForm := by +theorem Q_not_in_range_toQuadraticForm : Q ∉ Set.range BilinMap.toQuadraticMap := by rintro ⟨B, hB⟩ rw [← sub_zero Q] at hB apply algebraMap_not_injective @@ -294,10 +295,10 @@ open Q60596 in theorem QuadraticForm.not_forall_mem_range_toQuadraticForm.{v} : -- TODO: make `R` universe polymorphic ¬∀ (R : Type) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M), - Q ∈ Set.range BilinForm.toQuadraticForm := + Q ∈ Set.range BilinMap.toQuadraticMap := fun h => Q_not_in_range_toQuadraticForm <| by let uU := ULift.moduleEquiv (R := K) (M := L) obtain ⟨x, hx⟩ := h K (ULift L) (Q.comp uU) refine ⟨x.compl₁₂ uU.symm uU.symm, ?_⟩ ext - simp [BilinForm.toQuadraticForm_comp_same, hx] + simp [BilinMap.toQuadraticMap_comp_same, hx] diff --git a/Counterexamples/QuadraticForm.lean b/Counterexamples/QuadraticForm.lean index d75316bfc4cbc9..82fb40a17593f1 100644 --- a/Counterexamples/QuadraticForm.lean +++ b/Counterexamples/QuadraticForm.lean @@ -23,6 +23,7 @@ variable (F : Type*) [Nontrivial F] [CommRing F] [CharP F 2] open LinearMap open LinearMap.BilinForm open LinearMap (BilinForm) +open LinearMap.BilinMap namespace Counterexample @@ -53,12 +54,12 @@ This disproves a weaker version of `QuadraticForm.associated_left_inverse`. -/ theorem LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm.{u} : ¬∀ {R M : Type u} [CommSemiring R] [AddCommMonoid M], ∀ [Module R M], - Set.InjOn (toQuadraticForm : BilinForm R M → QuadraticForm R M) {B | B.IsSymm} := by + Set.InjOn (toQuadraticMap : BilinForm R M → QuadraticForm R M) {B | B.IsSymm} := by intro h let F := ULift.{u} (ZMod 2) apply B_ne_zero F apply h (isSymm_B F) isSymm_zero - rw [toQuadraticForm_zero, toQuadraticForm_eq_zero] + rw [toQuadraticMap_zero, toQuadraticMap_eq_zero] exact isAlt_B F #align counterexample.bilin_form.not_inj_on_to_quadratic_form_is_symm Counterexample.LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 771b51e6c3e9f2..c69ff834886747 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -13,9 +13,9 @@ import Mathlib.LinearAlgebra.TensorProduct.Tower ## Main definitions -* `LinearMap.BilinForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by +* `LinearMap.BilinMap.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by applying `B₁` on `M₁` and `B₂` on `M₂`. -* `LinearMap.BilinForm.tensorDistribEquiv`: `BilinForm.tensorDistrib` as an equivalence on finite +* `LinearMap.BilinMap.tensorDistribEquiv`: `BilinForm.tensorDistrib` as an equivalence on finite free modules. -/ @@ -30,8 +30,9 @@ open TensorProduct namespace LinearMap -namespace BilinForm +namespace BilinMap +open LinearMap (BilinMap) open LinearMap (BilinForm) section CommSemiring @@ -53,7 +54,7 @@ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm ∘ₗ (TensorProduct.AlgebraTensorModule.congr (TensorProduct.lift.equiv A M₁ M₁ A) (TensorProduct.lift.equiv R _ _ _)).toLinearMap -#align bilin_form.tensor_distrib LinearMap.BilinForm.tensorDistrib +#align bilin_form.tensor_distrib LinearMap.BilinMap.tensorDistrib -- TODO: make the RHS `MulOpposite.op (B₂ m₂ m₂') • B₁ m₁ m₁'` so that this has a nicer defeq for -- `R = A` of `B₁ m₁ m₁' * B₂ m₂ m₂'`, as it did before the generalization in #6306. @@ -63,16 +64,16 @@ theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) ( tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₂ m₂ m₂' • B₁ m₁ m₁' := rfl -#align bilin_form.tensor_distrib_tmul LinearMap.BilinForm.tensorDistrib_tmulₓ +#align bilin_form.tensor_distrib_tmul LinearMap.BilinMap.tensorDistrib_tmulₓ /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ -protected abbrev tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (M₁ ⊗[R] M₂) := +protected abbrev tmul (B₁ : BilinMap A M₁ A) (B₂ : BilinMap R M₂ R) : BilinMap A (M₁ ⊗[R] M₂) A := tensorDistrib R A (B₁ ⊗ₜ[R] B₂) -#align bilin_form.tmul LinearMap.BilinForm.tmul +#align bilin_form.tmul LinearMap.BilinMap.tmul attribute [local ext] TensorProduct.ext in /-- A tensor product of symmetric bilinear forms is symmetric. -/ -lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂} +lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R M₂ R} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by rw [LinearMap.isSymm_iff_eq_flip] ext x₁ x₂ y₁ y₂ @@ -80,11 +81,11 @@ lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R variable (A) in /-- The base change of a bilinear form. -/ -protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := - BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B +protected def baseChange (B : BilinMap R M₂ R) : BilinForm A (A ⊗[R] M₂) := + BilinMap.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B @[simp] -theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂) +theorem baseChange_tmul (B₂ : BilinMap R M₂ R) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := rfl @@ -115,7 +116,7 @@ noncomputable def tensorDistribEquiv : TensorProduct.dualDistribEquiv R (M₁ ⊗ M₁) (M₂ ⊗ M₂) ≪≫ₗ (TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ (TensorProduct.lift.equiv R _ _ _).symm -#align bilin_form.tensor_distrib_equiv LinearMap.BilinForm.tensorDistribEquiv +#align bilin_form.tensor_distrib_equiv LinearMap.BilinMap.tensorDistribEquiv @[simp] theorem tensorDistribEquiv_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) @@ -137,10 +138,10 @@ theorem tensorDistribEquiv_toLinearMap : theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) : tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B := DFunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B -#align bilin_form.tensor_distrib_equiv_apply LinearMap.BilinForm.tensorDistribEquiv_apply +#align bilin_form.tensor_distrib_equiv_apply LinearMap.BilinMap.tensorDistribEquiv_apply end CommRing -end BilinForm +end BilinMap end LinearMap diff --git a/Mathlib/LinearAlgebra/BilinearMap.lean b/Mathlib/LinearAlgebra/BilinearMap.lean index cec1b7120a8a23..f81852e042ee1b 100644 --- a/Mathlib/LinearAlgebra/BilinearMap.lean +++ b/Mathlib/LinearAlgebra/BilinearMap.lean @@ -393,9 +393,6 @@ theorem compr₂_apply (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] variable (R M) -/-- For convenience, a shorthand for the type of bilinear forms from `M` to `R`. -/ -protected abbrev BilinForm : Type _ := M →ₗ[R] M →ₗ[R] R - /-- Scalar multiplication as a bilinear map `R → M → M`. -/ def lsmul : R →ₗ[R] M →ₗ[R] M := mk₂ R (· • ·) add_smul (fun _ _ _ => mul_smul _ _ _) smul_add fun r s m => by @@ -413,6 +410,14 @@ variable {M} theorem lsmul_apply (r : R) (m : M) : lsmul R M r m = r • m := rfl #align linear_map.lsmul_apply LinearMap.lsmul_apply +variable (R M Nₗ) in +/-- A shorthand for the type of `R`-bilinear `Nₗ`-valued maps on `M`. -/ +protected abbrev BilinMap : Type _ := M →ₗ[R] M →ₗ[R] Nₗ + +variable (R M) in +/-- For convenience, a shorthand for the type of bilinear forms from `M` to `R`. -/ +protected abbrev BilinForm : Type _ := LinearMap.BilinMap R M R + end CommSemiring section CommRing diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index 4ac9d24d981cad..5dac845eb2db09 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -85,7 +85,7 @@ noncomputable def toBaseChange (Q : QuadraticForm R V) : letI : Invertible (2 : A ⊗[R] CliffordAlgebra Q) := (Invertible.map (algebraMap R _) 2).copy 2 (map_ofNat _ _).symm suffices hpure_tensor : ∀ v w, (1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) = - QuadraticForm.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 by + QuadraticMap.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 by -- the crux is that by converting to a statement about linear maps instead of quadratic forms, -- we then have access to all the partially-applied `ext` lemmas. rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)] @@ -95,8 +95,8 @@ noncomputable def toBaseChange (Q : QuadraticForm R V) : exact hpure_tensor v w intros v w rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap, - QuadraticForm.polarBilin_baseChange, LinearMap.BilinForm.baseChange_tmul, one_mul, - TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticForm.polarBilin_apply_apply] + QuadraticForm.polarBilin_baseChange, LinearMap.BilinMap.baseChange_tmul, one_mul, + TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticMap.polarBilin_apply_apply] @[simp] theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) : toBaseChange A Q (ι (Q.baseChange A) (z ⊗ₜ v)) = z ⊗ₜ ι Q v := diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean index 29b0e35ae90358..e65bb684bd141b 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean @@ -235,14 +235,14 @@ theorem induction {C : CliffordAlgebra Q → Prop} theorem mul_add_swap_eq_polar_of_forall_mul_self_eq {A : Type*} [Ring A] [Algebra R A] (f : M →ₗ[R] A) (hf : ∀ x, f x * f x = algebraMap _ _ (Q x)) (a b : M) : - f a * f b + f b * f a = algebraMap R _ (QuadraticForm.polar Q a b) := + f a * f b + f b * f a = algebraMap R _ (QuadraticMap.polar Q a b) := calc f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b := by rw [f.map_add, mul_add, add_mul, add_mul]; abel _ = algebraMap R _ (Q (a + b)) - algebraMap R _ (Q a) - algebraMap R _ (Q b) := by rw [hf, hf, hf] _ = algebraMap R _ (Q (a + b) - Q a - Q b) := by rw [← RingHom.map_sub, ← RingHom.map_sub] - _ = algebraMap R _ (QuadraticForm.polar Q a b) := rfl + _ = algebraMap R _ (QuadraticMap.polar Q a b) := rfl /-- An alternative way to provide the argument to `CliffordAlgebra.lift` when `2` is invertible. @@ -255,18 +255,18 @@ theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit ( Q.polarBilin.compr₂ (Algebra.linearMap R A) := by simp_rw [DFunLike.ext_iff] refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩ - change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticForm.polar Q x y) at h + change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticMap.polar Q x y) at h apply h2.mul_left_cancel - rw [two_mul, two_mul, h x x, QuadraticForm.polar_self, two_mul, map_add] + rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add] /-- The symmetric product of vectors is a scalar -/ theorem ι_mul_ι_add_swap (a b : M) : - ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticForm.polar Q a b) := + ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticMap.polar Q a b) := mul_add_swap_eq_polar_of_forall_mul_self_eq _ (ι_sq_scalar _) _ _ #align clifford_algebra.ι_mul_ι_add_swap CliffordAlgebra.ι_mul_ι_add_swap theorem ι_mul_ι_comm (a b : M) : - ι Q a * ι Q b = algebraMap R _ (QuadraticForm.polar Q a b) - ι Q b * ι Q a := + ι Q a * ι Q b = algebraMap R _ (QuadraticMap.polar Q a b) - ι Q b * ι Q a := eq_sub_of_add_eq (ι_mul_ι_add_swap a b) #align clifford_algebra.ι_mul_comm CliffordAlgebra.ι_mul_ι_comm @@ -293,7 +293,7 @@ end isOrtho /-- $aba$ is a vector. -/ theorem ι_mul_ι_mul_ι (a b : M) : - ι Q a * ι Q b * ι Q a = ι Q (QuadraticForm.polar Q a b • a - Q a • b) := by + ι Q a * ι Q b * ι Q a = ι Q (QuadraticMap.polar Q a b • a - Q a • b) := by rw [ι_mul_ι_comm, sub_mul, mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← Algebra.commutes, ← Algebra.smul_def, ← map_smul, ← map_smul, ← map_sub] #align clifford_algebra.ι_mul_ι_mul_ι CliffordAlgebra.ι_mul_ι_mul_ι diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean index 07aa8d9ddc01fc..9152fb3d7f2b36 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean @@ -42,6 +42,7 @@ Within this file, we use the local notation -/ +open LinearMap (BilinMap) open LinearMap (BilinForm) universe u1 u2 u3 @@ -255,39 +256,39 @@ theorem changeFormAux_changeFormAux (B : BilinForm R M) (v : M) (x : CliffordAlg variable {Q} variable {Q' Q'' : QuadraticForm R M} {B B' : BilinForm R M} -variable (h : B.toQuadraticForm = Q' - Q) (h' : B'.toQuadraticForm = Q'' - Q') +variable (h : B.toQuadraticMap = Q' - Q) (h' : B'.toQuadraticMap = Q'' - Q') /-- Convert between two algebras of different quadratic form, sending vector to vectors, scalars to scalars, and adjusting products by a contraction term. This is $\lambda_B$ from [bourbaki2007][] $9 Lemma 2. -/ -def changeForm (h : B.toQuadraticForm = Q' - Q) : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' := +def changeForm (h : B.toQuadraticMap = Q' - Q) : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' := foldr Q (changeFormAux Q' B) (fun m x => (changeFormAux_changeFormAux Q' B m x).trans <| by - dsimp only [← BilinForm.toQuadraticForm_apply] - rw [h, QuadraticForm.sub_apply, sub_sub_cancel]) + dsimp only [← BilinMap.toQuadraticMap_apply] + rw [h, QuadraticMap.sub_apply, sub_sub_cancel]) 1 #align clifford_algebra.change_form CliffordAlgebra.changeForm /-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm` -/ -theorem changeForm.zero_proof : (0 : BilinForm R M).toQuadraticForm = Q - Q := +theorem changeForm.zero_proof : (0 : BilinForm R M).toQuadraticMap = Q - Q := (sub_self _).symm #align clifford_algebra.change_form.zero_proof CliffordAlgebra.changeForm.zero_proof /-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm` -/ -theorem changeForm.add_proof : (B + B').toQuadraticForm = Q'' - Q := +theorem changeForm.add_proof : (B + B').toQuadraticMap = Q'' - Q := (congr_arg₂ (· + ·) h h').trans <| sub_add_sub_cancel' _ _ _ #align clifford_algebra.change_form.add_proof CliffordAlgebra.changeForm.add_proof /-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm` -/ -theorem changeForm.neg_proof : (-B).toQuadraticForm = Q - Q' := +theorem changeForm.neg_proof : (-B).toQuadraticMap = Q - Q' := (congr_arg Neg.neg h).trans <| neg_sub _ _ #align clifford_algebra.change_form.neg_proof CliffordAlgebra.changeForm.neg_proof theorem changeForm.associated_neg_proof [Invertible (2 : R)] : - (QuadraticForm.associated (R := R) (M := M) (-Q)).toQuadraticForm = 0 - Q := by - simp [QuadraticForm.toQuadraticForm_associated] + (QuadraticMap.associated (R := R) (M := M) (-Q)).toQuadraticMap = 0 - Q := by + simp [QuadraticMap.toQuadraticMap_associated] #align clifford_algebra.change_form.associated_neg_proof CliffordAlgebra.changeForm.associated_neg_proof @[simp] diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean index 5a8e9f08dfdd70..aae8e242b66296 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean @@ -127,7 +127,7 @@ open scoped ComplexConjugate /-- The quadratic form sending elements to the negation of their square. -/ def Q : QuadraticForm ℝ ℝ := - -QuadraticForm.sq (R := ℝ) -- Porting note: Added `(R := ℝ)` + -QuadraticMap.sq (R := ℝ) -- Porting note: Added `(R := ℝ)` set_option linter.uppercaseLean3 false in #align clifford_algebra_complex.Q CliffordAlgebraComplex.Q @@ -259,7 +259,8 @@ variable {R : Type*} [CommRing R] (c₁ c₂ : R) /-- `Q c₁ c₂` is a quadratic form over `R × R` such that `CliffordAlgebra (Q c₁ c₂)` is isomorphic as an `R`-algebra to `ℍ[R,c₁,c₂]`. -/ def Q : QuadraticForm R (R × R) := - (c₁ • QuadraticForm.sq (R := R)).prod (c₂ • QuadraticForm.sq) -- Porting note: Added `(R := R)` + -- Porting note: Added `(R := R)` + QuadraticForm.prod (c₁ • QuadraticMap.sq (R := R)) (c₂ • QuadraticMap.sq) set_option linter.uppercaseLean3 false in #align clifford_algebra_quaternion.Q CliffordAlgebraQuaternion.Q @@ -283,7 +284,7 @@ def quaternionBasis : QuaternionAlgebra.Basis (CliffordAlgebra (Q c₁ c₂)) c simp i_mul_j := rfl j_mul_i := by - rw [eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticForm.polar] + rw [eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticMap.polar] simp #align clifford_algebra_quaternion.quaternion_basis CliffordAlgebraQuaternion.quaternionBasis @@ -399,7 +400,7 @@ variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] theorem ι_mul_ι (r₁ r₂) : ι (0 : QuadraticForm R R) r₁ * ι (0 : QuadraticForm R R) r₂ = 0 := by rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul R, ← smul_eq_mul R, LinearMap.map_smul, - LinearMap.map_smul, smul_mul_smul, ι_sq_scalar, QuadraticForm.zero_apply, RingHom.map_zero, + LinearMap.map_smul, smul_mul_smul, ι_sq_scalar, QuadraticMap.zero_apply, RingHom.map_zero, smul_zero] #align clifford_algebra_dual_number.ι_mul_ι CliffordAlgebraDualNumber.ι_mul_ι @@ -415,14 +416,14 @@ protected def equiv : CliffordAlgebra (0 : QuadraticForm R R) ≃ₐ[R] R[ε] := (by ext : 1 -- This used to be a single `simp` before leanprover/lean4#2644 - simp only [QuadraticForm.zero_apply, AlgHom.coe_comp, Function.comp_apply, lift_apply_eps, + simp only [QuadraticMap.zero_apply, AlgHom.coe_comp, Function.comp_apply, lift_apply_eps, AlgHom.coe_id, id_eq] erw [lift_ι_apply] simp) -- This used to be a single `simp` before leanprover/lean4#2644 (by ext : 2 - simp only [QuadraticForm.zero_apply, AlgHom.comp_toLinearMap, LinearMap.coe_comp, + simp only [QuadraticMap.zero_apply, AlgHom.comp_toLinearMap, LinearMap.coe_comp, Function.comp_apply, AlgHom.toLinearMap_apply, AlgHom.toLinearMap_id, LinearMap.id_comp] erw [lift_ι_apply] simp) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean index ff323c0dd90a07..611e1bffb3263a 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean @@ -47,7 +47,7 @@ namespace EquivEven /-- The quadratic form on the augmented vector space `M × R` sending `v + r•e0` to `Q v - r^2`. -/ abbrev Q' : QuadraticForm R (M × R) := - Q.prod <| -@QuadraticForm.sq R _ + Q.prod <| -QuadraticMap.sq (R := R) set_option linter.uppercaseLean3 false in #align clifford_algebra.equiv_even.Q' CliffordAlgebra.EquivEven.Q' @@ -81,8 +81,8 @@ theorem v_sq_scalar (m : M) : v Q m * v Q m = algebraMap _ _ (Q m) := theorem neg_e0_mul_v (m : M) : -(e0 Q * v Q m) = v Q m * e0 Q := by refine neg_eq_of_add_eq_zero_right ((ι_mul_ι_add_swap _ _).trans ?_) - dsimp [QuadraticForm.polar] - simp only [add_zero, mul_zero, mul_one, zero_add, neg_zero, QuadraticForm.map_zero, + dsimp [QuadraticMap.polar] + simp only [add_zero, mul_zero, mul_one, zero_add, neg_zero, QuadraticMap.map_zero, add_sub_cancel_right, sub_self, map_zero, zero_sub] #align clifford_algebra.equiv_even.neg_e0_mul_v CliffordAlgebra.EquivEven.neg_e0_mul_v @@ -261,11 +261,10 @@ def evenToNeg (Q' : QuadraticForm R M) (h : Q' = -Q) : letI : HasDistribNeg (even Q') := NonUnitalNonAssocRing.toHasDistribNeg { bilin := -(even.ι Q' : _).bilin contract := fun m => by - simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticForm.neg_apply, map_neg, - neg_neg] + simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticMap.neg_apply, map_neg, neg_neg] contract_mid := fun m₁ m₂ m₃ => by simp_rw [LinearMap.neg_apply, neg_mul_neg, EvenHom.contract_mid, h, - QuadraticForm.neg_apply, smul_neg, neg_smul] } + QuadraticMap.neg_apply, smul_neg, neg_smul] } #align clifford_algebra.even_to_neg CliffordAlgebra.evenToNeg -- Porting note: `simpNF` times out, but only in CI where all of `Mathlib` is imported diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean index 923d4985f90626..6401944bc84513 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean @@ -42,14 +42,14 @@ theorem isUnit_ι_of_isUnit {m : M} (h : IsUnit (Q m)) : IsUnit (ι Q m) := by /-- $aba^{-1}$ is a vector. -/ theorem ι_mul_ι_mul_invOf_ι (a b : M) [Invertible (ι Q a)] [Invertible (Q a)] : - ι Q a * ι Q b * ⅟ (ι Q a) = ι Q ((⅟ (Q a) * QuadraticForm.polar Q a b) • a - b) := by + ι Q a * ι Q b * ⅟ (ι Q a) = ι Q ((⅟ (Q a) * QuadraticMap.polar Q a b) • a - b) := by rw [invOf_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul, invOf_mul_self, one_smul] #align clifford_algebra.ι_mul_ι_mul_inv_of_ι CliffordAlgebra.ι_mul_ι_mul_invOf_ι /-- $a^{-1}ba$ is a vector. -/ theorem invOf_ι_mul_ι_mul_ι (a b : M) [Invertible (ι Q a)] [Invertible (Q a)] : - ⅟ (ι Q a) * ι Q b * ι Q a = ι Q ((⅟ (Q a) * QuadraticForm.polar Q a b) • a - b) := by + ⅟ (ι Q a) * ι Q b * ι Q a = ι Q ((⅟ (Q a) * QuadraticMap.polar Q a b) • a - b) := by rw [invOf_ι, map_smul, smul_mul_assoc, smul_mul_assoc, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul, invOf_mul_self, one_smul] #align clifford_algebra.inv_of_ι_mul_ι_mul_ι CliffordAlgebra.invOf_ι_mul_ι_mul_ι diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean index 39f752d0f3bf9e..c75c98a28071d8 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean @@ -135,7 +135,8 @@ def toProd : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂ →ₐ[R] CliffordAlgebra (Q₁ GradedTensorProduct.lift _ _ (CliffordAlgebra.map <| .inl _ _) (CliffordAlgebra.map <| .inr _ _) - fun _i₁ _i₂ x₁ x₂ => map_mul_map_of_isOrtho_of_mem_evenOdd _ _ (.inl_inr) _ _ x₁.prop x₂.prop + fun _i₁ _i₂ x₁ x₂ => map_mul_map_of_isOrtho_of_mem_evenOdd _ _ (QuadraticForm.IsOrtho.inl_inr) _ + _ x₁.prop x₂.prop @[simp] lemma toProd_ι_tmul_one (m₁ : M₁) : toProd Q₁ Q₂ (ι _ m₁ ᵍ⊗ₜ 1) = ι _ (m₁, 0) := by diff --git a/Mathlib/LinearAlgebra/Matrix/PosDef.lean b/Mathlib/LinearAlgebra/Matrix/PosDef.lean index 7e9e72cc1b61be..2c87bb1691d8a7 100644 --- a/Mathlib/LinearAlgebra/Matrix/PosDef.lean +++ b/Mathlib/LinearAlgebra/Matrix/PosDef.lean @@ -338,17 +338,17 @@ protected lemma add {A : Matrix m m R} {B : Matrix m m R} hA.add_posSemidef hB.posSemidef theorem of_toQuadraticForm' [DecidableEq n] {M : Matrix n n ℝ} (hM : M.IsSymm) - (hMq : M.toQuadraticForm'.PosDef) : M.PosDef := by - refine ⟨hM, fun x hx => ?_⟩ - simp only [toQuadraticForm', QuadraticForm.PosDef, LinearMap.BilinForm.toQuadraticForm_apply, + (hMq : M.toQuadraticMap'.PosDef) : M.PosDef := by + refine' ⟨hM, fun x hx => _⟩ + simp only [toQuadraticMap', QuadraticMap.PosDef, LinearMap.BilinMap.toQuadraticMap_apply, toLinearMap₂'_apply'] at hMq apply hMq x hx #align matrix.pos_def_of_to_quadratic_form' Matrix.PosDef.of_toQuadraticForm' theorem toQuadraticForm' [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) : - M.toQuadraticForm'.PosDef := by + M.toQuadraticMap'.PosDef := by intro x hx - simp only [Matrix.toQuadraticForm', LinearMap.BilinForm.toQuadraticForm_apply, + simp only [Matrix.toQuadraticMap', LinearMap.BilinMap.toQuadraticMap_apply, toLinearMap₂'_apply'] apply hM.2 x hx #align matrix.pos_def_to_quadratic_form' Matrix.PosDef.toQuadraticForm' @@ -372,18 +372,20 @@ end Matrix namespace QuadraticForm +open QuadraticMap + variable {n : Type*} [Fintype n] theorem posDef_of_toMatrix' [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)} (hQ : Q.toMatrix'.PosDef) : Q.PosDef := by - rw [← toQuadraticForm_associated ℝ Q, + rw [← toQuadraticMap_associated ℝ Q, ← LinearMap.toMatrix₂'.left_inv ((associatedHom (R := ℝ) ℝ) Q)] exact hQ.toQuadraticForm' #align quadratic_form.pos_def_of_to_matrix' QuadraticForm.posDef_of_toMatrix' theorem posDef_toMatrix' [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)} (hQ : Q.PosDef) : Q.toMatrix'.PosDef := by - rw [← toQuadraticForm_associated ℝ Q, ← + rw [← toQuadraticMap_associated ℝ Q, ← LinearMap.toMatrix₂'.left_inv ((associatedHom (R := ℝ) ℝ) Q)] at hQ exact .of_toQuadraticForm' (isSymm_toMatrix' Q) hQ #align quadratic_form.pos_def_to_matrix' QuadraticForm.posDef_toMatrix' diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 116e8d71862432..562359784b7e19 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -6,46 +6,48 @@ Authors: Anne Baanen, Kexing Ying, Eric Wieser import Mathlib.LinearAlgebra.Matrix.Determinant.Basic import Mathlib.LinearAlgebra.Matrix.SesquilinearForm import Mathlib.LinearAlgebra.Matrix.Symmetric +import Mathlib.LinearAlgebra.BilinearMap #align_import linear_algebra.quadratic_form.basic from "leanprover-community/mathlib"@"d11f435d4e34a6cea0a1797d6b625b0c170be845" /-! -# Quadratic forms +# Quadratic maps -This file defines quadratic forms over a `R`-module `M`. -A quadratic form on a commutative ring `R` is a map `Q : M → R` such that: +This file defines quadratic maps on an `R`-module `M`, taking values in an `R`-module `N`. +An `N`-valued quadratic map on a module `M` over a commutative ring `R` is a map `Q : M → N` such +that: -* `QuadraticForm.map_smul`: `Q (a • x) = a * a * Q x` -* `QuadraticForm.polar_add_left`, `QuadraticForm.polar_add_right`, - `QuadraticForm.polar_smul_left`, `QuadraticForm.polar_smul_right`: - the map `QuadraticForm.polar Q := fun x y ↦ Q (x + y) - Q x - Q y` is bilinear. +* `QuadraticMap.map_smul`: `Q (a • x) = (a * a) • Q x` +* `QuadraticMap.polar_add_left`, `QuadraticMap.polar_add_right`, + `QuadraticMap.polar_smul_left`, `QuadraticMap.polar_smul_right`: + the map `QuadraticMap.polar Q := fun x y ↦ Q (x + y) - Q x - Q y` is bilinear. This notion generalizes to commutative semirings using the approach in [izhakian2016][] which -requires that there be a (possibly non-unique) companion bilinear form `B` such that -`∀ x y, Q (x + y) = Q x + Q y + B x y`. Over a ring, this `B` is precisely `QuadraticForm.polar Q`. +requires that there be a (possibly non-unique) companion bilinear map `B` such that +`∀ x y, Q (x + y) = Q x + Q y + B x y`. Over a ring, this `B` is precisely `QuadraticMap.polar Q`. -To build a `QuadraticForm` from the `polar` axioms, use `QuadraticForm.ofPolar`. +To build a `QuadraticMap` from the `polar` axioms, use `QuadraticMap.ofPolar`. -Quadratic forms come with a scalar multiplication, `(a • Q) x = Q (a • x) = a * a * Q x`, +Quadratic maps come with a scalar multiplication, `(a • Q) x = a • Q x`, and composition with linear maps `f`, `Q.comp f x = Q (f x)`. ## Main definitions - * `QuadraticForm.ofPolar`: a more familiar constructor that works on rings - * `QuadraticForm.associated`: associated bilinear form - * `QuadraticForm.PosDef`: positive definite quadratic forms - * `QuadraticForm.Anisotropic`: anisotropic quadratic forms - * `QuadraticForm.discr`: discriminant of a quadratic form - * `QuadraticForm.IsOrtho`: orthogonality of vectors with respect to a quadratic form. + * `QuadraticMap.ofPolar`: a more familiar constructor that works on rings + * `QuadraticMap.associated`: associated bilinear map + * `QuadraticMap.PosDef`: positive definite quadratic maps + * `QuadraticMap.Anisotropic`: anisotropic quadratic maps + * `QuadraticMap.discr`: discriminant of a quadratic map + * `QuadraticMap.IsOrtho`: orthogonality of vectors with respect to a quadratic map. ## Main statements - * `QuadraticForm.associated_left_inverse`, - * `QuadraticForm.associated_rightInverse`: in a commutative ring where 2 has - an inverse, there is a correspondence between quadratic forms and symmetric + * `QuadraticMap.associated_left_inverse`, + * `QuadraticMap.associated_rightInverse`: in a commutative ring where 2 has + an inverse, there is a correspondence between quadratic maps and symmetric bilinear forms * `LinearMap.BilinForm.exists_orthogonal_basis`: There exists an orthogonal basis with - respect to any nondegenerate, symmetric bilinear form `B`. + respect to any nondegenerate, symmetric bilinear map `B`. ## Notation @@ -56,7 +58,7 @@ The variable `S` is used when `R` itself has a `•` action. ## Implementation notes While the definition and many results make sense if we drop commutativity assumptions, -the correct definition of a quadratic form in the noncommutative setting would require +the correct definition of a quadratic maps in the noncommutative setting would require substantial refactors from the current version, such that $Q(rm) = rQ(m)r^*$ for some suitable conjugation $r^*$. @@ -70,50 +72,51 @@ has some further discusion. ## Tags -quadratic form, homogeneous polynomial, quadratic polynomial +quadratic map, homogeneous polynomial, quadratic polynomial -/ universe u v w variable {S T : Type*} -variable {R : Type*} {M N : Type*} +variable {R : Type*} {M N P A : Type*} +open LinearMap (BilinMap) open LinearMap (BilinForm) section Polar -variable [CommRing R] [AddCommGroup M] +variable [CommRing R] [AddCommGroup M] [AddCommGroup N] -namespace QuadraticForm +namespace QuadraticMap -/-- Up to a factor 2, `Q.polar` is the associated bilinear form for a quadratic form `Q`. +/-- Up to a factor 2, `Q.polar` is the associated bilinear map for a quadratic map `Q`. Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization -/ -def polar (f : M → R) (x y : M) := +def polar (f : M → N) (x y : M) := f (x + y) - f x - f y -#align quadratic_form.polar QuadraticForm.polar +#align quadratic_form.polar QuadraticMap.polar -theorem polar_add (f g : M → R) (x y : M) : polar (f + g) x y = polar f x y + polar g x y := by +theorem polar_add (f g : M → N) (x y : M) : polar (f + g) x y = polar f x y + polar g x y := by simp only [polar, Pi.add_apply] abel -#align quadratic_form.polar_add QuadraticForm.polar_add +#align quadratic_form.polar_add QuadraticMap.polar_add -theorem polar_neg (f : M → R) (x y : M) : polar (-f) x y = -polar f x y := by +theorem polar_neg (f : M → N) (x y : M) : polar (-f) x y = -polar f x y := by simp only [polar, Pi.neg_apply, sub_eq_add_neg, neg_add] -#align quadratic_form.polar_neg QuadraticForm.polar_neg +#align quadratic_form.polar_neg QuadraticMap.polar_neg -theorem polar_smul [Monoid S] [DistribMulAction S R] (f : M → R) (s : S) (x y : M) : +theorem polar_smul [Monoid S] [DistribMulAction S N] (f : M → N) (s : S) (x y : M) : polar (s • f) x y = s • polar f x y := by simp only [polar, Pi.smul_apply, smul_sub] -#align quadratic_form.polar_smul QuadraticForm.polar_smul +#align quadratic_form.polar_smul QuadraticMap.polar_smul -theorem polar_comm (f : M → R) (x y : M) : polar f x y = polar f y x := by +theorem polar_comm (f : M → N) (x y : M) : polar f x y = polar f y x := by rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)] -#align quadratic_form.polar_comm QuadraticForm.polar_comm +#align quadratic_form.polar_comm QuadraticMap.polar_comm -/-- Auxiliary lemma to express bilinearity of `QuadraticForm.polar` without subtraction. -/ -theorem polar_add_left_iff {f : M → R} {x x' y : M} : +/-- Auxiliary lemma to express bilinearity of `QuadraticMap.polar` without subtraction. -/ +theorem polar_add_left_iff {f : M → N} {x x' y : M} : polar f (x + x') y = polar f x y + polar f x' y ↔ f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x) := by simp only [← add_assoc] @@ -121,228 +124,239 @@ theorem polar_add_left_iff {f : M → R} {x x' y : M} : simp only [add_right_comm _ (f y) _, add_right_comm _ (f x') (f x)] rw [add_comm y x, add_right_comm _ _ (f (x + y)), add_comm _ (f (x + y)), add_right_comm (f (x + y)), add_left_inj] -#align quadratic_form.polar_add_left_iff QuadraticForm.polar_add_left_iff +#align quadratic_form.polar_add_left_iff QuadraticMap.polar_add_left_iff -theorem polar_comp {F : Type*} [CommRing S] [FunLike F R S] [AddMonoidHomClass F R S] - (f : M → R) (g : F) (x y : M) : +theorem polar_comp {F : Type*} [CommRing S] [FunLike F N S] [AddMonoidHomClass F N S] + (f : M → N) (g : F) (x y : M) : polar (g ∘ f) x y = g (polar f x y) := by simp only [polar, Pi.smul_apply, Function.comp_apply, map_sub] -#align quadratic_form.polar_comp QuadraticForm.polar_comp +#align quadratic_form.polar_comp QuadraticMap.polar_comp -end QuadraticForm +end QuadraticMap end Polar -/-- A quadratic form over a module. +/-- A quadratic map on a module. + +For a more familiar constructor when `R` is a ring, see `QuadraticMap.ofPolar`. -/ +structure QuadraticMap (R : Type u) (M : Type v) (N : Type w) [CommSemiring R] [AddCommMonoid M] + [Module R M] [AddCommMonoid N] [Module R N] where + toFun : M → N + toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x + exists_companion' : ∃ B : BilinMap R M N, ∀ x y, toFun (x + y) = toFun x + toFun y + B x y +#align quadratic_form QuadraticMap -For a more familiar constructor when `R` is a ring, see `QuadraticForm.ofPolar`. -/ -structure QuadraticForm (R : Type u) (M : Type v) - [CommSemiring R] [AddCommMonoid M] [Module R M] where - toFun : M → R - toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = a * a * toFun x - exists_companion' : - ∃ B : BilinForm R M, ∀ x y, toFun (x + y) = toFun x + toFun y + B x y -#align quadratic_form QuadraticForm +section QuadraticForm -namespace QuadraticForm +variable (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] + +variable (R M) in +/-- A quadratic form on a module. -/ +abbrev QuadraticForm : Type _ := QuadraticMap R M R + +end QuadraticForm + +namespace QuadraticMap section DFunLike -variable [CommSemiring R] [AddCommMonoid M] [Module R M] -variable {Q Q' : QuadraticForm R M} +variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] +variable {Q Q' : QuadraticMap R M N} -instance instFunLike : FunLike (QuadraticForm R M) M R where +instance instFunLike : FunLike (QuadraticMap R M N) M N where coe := toFun coe_injective' x y h := by cases x; cases y; congr -#align quadratic_form.fun_like QuadraticForm.instFunLike +#align quadratic_form.fun_like QuadraticMap.instFunLike /-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun` directly. -/ -instance : CoeFun (QuadraticForm R M) fun _ => M → R := +instance : CoeFun (QuadraticMap R M N) fun _ => M → N := ⟨DFunLike.coe⟩ variable (Q) -/-- The `simp` normal form for a quadratic form is `DFunLike.coe`, not `toFun`. -/ +/-- The `simp` normal form for a quadratic map is `DFunLike.coe`, not `toFun`. -/ @[simp] theorem toFun_eq_coe : Q.toFun = ⇑Q := rfl -#align quadratic_form.to_fun_eq_coe QuadraticForm.toFun_eq_coe +#align quadratic_form.to_fun_eq_coe QuadraticMap.toFun_eq_coe -- this must come after the coe_to_fun definition -initialize_simps_projections QuadraticForm (toFun → apply) +initialize_simps_projections QuadraticMap (toFun → apply) variable {Q} @[ext] theorem ext (H : ∀ x : M, Q x = Q' x) : Q = Q' := DFunLike.ext _ _ H -#align quadratic_form.ext QuadraticForm.ext +#align quadratic_form.ext QuadraticMap.ext theorem congr_fun (h : Q = Q') (x : M) : Q x = Q' x := DFunLike.congr_fun h _ -#align quadratic_form.congr_fun QuadraticForm.congr_fun +#align quadratic_form.congr_fun QuadraticMap.congr_fun theorem ext_iff : Q = Q' ↔ ∀ x, Q x = Q' x := DFunLike.ext_iff -#align quadratic_form.ext_iff QuadraticForm.ext_iff +#align quadratic_form.ext_iff QuadraticMap.ext_iff -/-- Copy of a `QuadraticForm` with a new `toFun` equal to the old one. Useful to fix definitional +/-- Copy of a `QuadraticMap` with a new `toFun` equal to the old one. Useful to fix definitional equalities. -/ -protected def copy (Q : QuadraticForm R M) (Q' : M → R) (h : Q' = ⇑Q) : QuadraticForm R M where +protected def copy (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q) : QuadraticMap R M N where toFun := Q' toFun_smul := h.symm ▸ Q.toFun_smul exists_companion' := h.symm ▸ Q.exists_companion' -#align quadratic_form.copy QuadraticForm.copy +#align quadratic_form.copy QuadraticMap.copy @[simp] -theorem coe_copy (Q : QuadraticForm R M) (Q' : M → R) (h : Q' = ⇑Q) : ⇑(Q.copy Q' h) = Q' := +theorem coe_copy (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q) : ⇑(Q.copy Q' h) = Q' := rfl -#align quadratic_form.coe_copy QuadraticForm.coe_copy +#align quadratic_form.coe_copy QuadraticMap.coe_copy -theorem copy_eq (Q : QuadraticForm R M) (Q' : M → R) (h : Q' = ⇑Q) : Q.copy Q' h = Q := +theorem copy_eq (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q) : Q.copy Q' h = Q := DFunLike.ext' h -#align quadratic_form.copy_eq QuadraticForm.copy_eq +#align quadratic_form.copy_eq QuadraticMap.copy_eq end DFunLike section CommSemiring -variable [CommSemiring R] [AddCommMonoid M] [Module R M] -variable (Q : QuadraticForm R M) +variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] +variable (Q : QuadraticMap R M N) -theorem map_smul (a : R) (x : M) : Q (a • x) = a * a * Q x := +theorem map_smul (a : R) (x : M) : Q (a • x) = (a * a) • Q x := Q.toFun_smul a x -#align quadratic_form.map_smul QuadraticForm.map_smul +#align quadratic_form.map_smul QuadraticMap.map_smul -theorem exists_companion : ∃ B : BilinForm R M, ∀ x y, Q (x + y) = Q x + Q y + B x y := +theorem exists_companion : ∃ B : BilinMap R M N, ∀ x y, Q (x + y) = Q x + Q y + B x y := Q.exists_companion' -#align quadratic_form.exists_companion QuadraticForm.exists_companion +#align quadratic_form.exists_companion QuadraticMap.exists_companion theorem map_add_add_add_map (x y z : M) : Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x) := by obtain ⟨B, h⟩ := Q.exists_companion rw [add_comm z x] - simp only [h, map_add, LinearMap.add_apply] + simp only [h, LinearMap.map_add₂] abel -#align quadratic_form.map_add_add_add_map QuadraticForm.map_add_add_add_map +#align quadratic_form.map_add_add_add_map QuadraticMap.map_add_add_add_map -theorem map_add_self (x : M) : Q (x + x) = 4 * Q x := by - rw [← one_smul R x, ← add_smul, map_smul] +theorem map_add_self (x : M) : Q (x + x) = 4 • Q x := by + rw [← two_smul R x, map_smul, nsmul_eq_smul_cast R] norm_num -#align quadratic_form.map_add_self QuadraticForm.map_add_self +#align quadratic_form.map_add_self QuadraticMap.map_add_self -- not @[simp] because it is superseded by `ZeroHomClass.map_zero` protected theorem map_zero : Q 0 = 0 := by - rw [← @zero_smul R _ _ _ _ (0 : M), map_smul, zero_mul, zero_mul] -#align quadratic_form.map_zero QuadraticForm.map_zero + rw [← @zero_smul R _ _ _ _ (0 : M), map_smul, zero_mul, zero_smul] +#align quadratic_form.map_zero QuadraticMap.map_zero -instance zeroHomClass : ZeroHomClass (QuadraticForm R M) M R where - map_zero := QuadraticForm.map_zero -#align quadratic_form.zero_hom_class QuadraticForm.zeroHomClass +instance zeroHomClass : ZeroHomClass (QuadraticMap R M N) M N := + { QuadraticMap.instFunLike (R := R) (M := M) (N := N) with map_zero := QuadraticMap.map_zero } +#align quadratic_form.zero_hom_class QuadraticMap.zeroHomClass -theorem map_smul_of_tower [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (a : S) +theorem map_smul_of_tower [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] + [Module S N] [IsScalarTower S R N] (a : S) (x : M) : Q (a • x) = (a * a) • Q x := by - rw [← IsScalarTower.algebraMap_smul R a x, map_smul, ← RingHom.map_mul, Algebra.smul_def] -#align quadratic_form.map_smul_of_tower QuadraticForm.map_smul_of_tower + rw [← IsScalarTower.algebraMap_smul R a x, map_smul, ← RingHom.map_mul, algebraMap_smul] +#align quadratic_form.map_smul_of_tower QuadraticMap.map_smul_of_tower end CommSemiring section CommRing -variable [CommRing R] [AddCommGroup M] -variable [Module R M] (Q : QuadraticForm R M) +variable [CommRing R] [AddCommGroup M] [AddCommGroup N] +variable [Module R M] [Module R N] (Q : QuadraticMap R M N) @[simp] theorem map_neg (x : M) : Q (-x) = Q x := by - rw [← @neg_one_smul R _ _ _ _ x, map_smul, neg_one_mul, neg_neg, one_mul] -#align quadratic_form.map_neg QuadraticForm.map_neg + rw [← @neg_one_smul R _ _ _ _ x, map_smul, neg_one_mul, neg_neg, one_smul] +#align quadratic_form.map_neg QuadraticMap.map_neg theorem map_sub (x y : M) : Q (x - y) = Q (y - x) := by rw [← neg_sub, map_neg] -#align quadratic_form.map_sub QuadraticForm.map_sub +#align quadratic_form.map_sub QuadraticMap.map_sub @[simp] theorem polar_zero_left (y : M) : polar Q 0 y = 0 := by - simp only [polar, zero_add, QuadraticForm.map_zero, sub_zero, sub_self] -#align quadratic_form.polar_zero_left QuadraticForm.polar_zero_left + simp only [polar, zero_add, QuadraticMap.map_zero, sub_zero, sub_self] +#align quadratic_form.polar_zero_left QuadraticMap.polar_zero_left @[simp] theorem polar_add_left (x x' y : M) : polar Q (x + x') y = polar Q x y + polar Q x' y := polar_add_left_iff.mpr <| Q.map_add_add_add_map x x' y -#align quadratic_form.polar_add_left QuadraticForm.polar_add_left +#align quadratic_form.polar_add_left QuadraticMap.polar_add_left @[simp] -theorem polar_smul_left (a : R) (x y : M) : polar Q (a • x) y = a * polar Q x y := by +theorem polar_smul_left (a : R) (x y : M) : polar Q (a • x) y = a • polar Q x y := by obtain ⟨B, h⟩ := Q.exists_companion - simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel_left, smul_eq_mul] -#align quadratic_form.polar_smul_left QuadraticForm.polar_smul_left + simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel_left] +#align quadratic_form.polar_smul_left QuadraticMap.polar_smul_left @[simp] theorem polar_neg_left (x y : M) : polar Q (-x) y = -polar Q x y := by - rw [← neg_one_smul R x, polar_smul_left, neg_one_mul] -#align quadratic_form.polar_neg_left QuadraticForm.polar_neg_left + rw [← neg_one_smul R x, polar_smul_left, neg_one_smul] +#align quadratic_form.polar_neg_left QuadraticMap.polar_neg_left @[simp] theorem polar_sub_left (x x' y : M) : polar Q (x - x') y = polar Q x y - polar Q x' y := by rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_left, polar_neg_left] -#align quadratic_form.polar_sub_left QuadraticForm.polar_sub_left +#align quadratic_form.polar_sub_left QuadraticMap.polar_sub_left @[simp] theorem polar_zero_right (y : M) : polar Q y 0 = 0 := by - simp only [add_zero, polar, QuadraticForm.map_zero, sub_self] -#align quadratic_form.polar_zero_right QuadraticForm.polar_zero_right + simp only [add_zero, polar, QuadraticMap.map_zero, sub_self] +#align quadratic_form.polar_zero_right QuadraticMap.polar_zero_right @[simp] theorem polar_add_right (x y y' : M) : polar Q x (y + y') = polar Q x y + polar Q x y' := by rw [polar_comm Q x, polar_comm Q x, polar_comm Q x, polar_add_left] -#align quadratic_form.polar_add_right QuadraticForm.polar_add_right +#align quadratic_form.polar_add_right QuadraticMap.polar_add_right @[simp] -theorem polar_smul_right (a : R) (x y : M) : polar Q x (a • y) = a * polar Q x y := by +theorem polar_smul_right (a : R) (x y : M) : polar Q x (a • y) = a • polar Q x y := by rw [polar_comm Q x, polar_comm Q x, polar_smul_left] -#align quadratic_form.polar_smul_right QuadraticForm.polar_smul_right +#align quadratic_form.polar_smul_right QuadraticMap.polar_smul_right @[simp] theorem polar_neg_right (x y : M) : polar Q x (-y) = -polar Q x y := by - rw [← neg_one_smul R y, polar_smul_right, neg_one_mul] -#align quadratic_form.polar_neg_right QuadraticForm.polar_neg_right + rw [← neg_one_smul R y, polar_smul_right, neg_one_smul] +#align quadratic_form.polar_neg_right QuadraticMap.polar_neg_right @[simp] theorem polar_sub_right (x y y' : M) : polar Q x (y - y') = polar Q x y - polar Q x y' := by rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right] -#align quadratic_form.polar_sub_right QuadraticForm.polar_sub_right +#align quadratic_form.polar_sub_right QuadraticMap.polar_sub_right @[simp] -theorem polar_self (x : M) : polar Q x x = 2 * Q x := by - rw [polar, map_add_self, sub_sub, sub_eq_iff_eq_add, ← two_mul, ← two_mul, ← mul_assoc] +theorem polar_self (x : M) : polar Q x x = 2 • Q x := by + rw [polar, map_add_self, sub_sub, sub_eq_iff_eq_add, ← two_smul ℕ, ← two_smul ℕ, ← mul_smul] norm_num -#align quadratic_form.polar_self QuadraticForm.polar_self +#align quadratic_form.polar_self QuadraticMap.polar_self -/-- `QuadraticForm.polar` as a bilinear map -/ +/-- `QuadraticMap.polar` as a bilinear map -/ @[simps!] -def polarBilin : BilinForm R M := +def polarBilin : BilinMap R M N := LinearMap.mk₂ R (polar Q) (polar_add_left Q) (polar_smul_left Q) (polar_add_right Q) (polar_smul_right Q) -#align quadratic_form.polar_bilin QuadraticForm.polarBilin +#align quadratic_form.polar_bilin QuadraticMap.polarBilin -variable [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] +variable [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] [Module S N] + [IsScalarTower S R N] @[simp] theorem polar_smul_left_of_tower (a : S) (x y : M) : polar Q (a • x) y = a • polar Q x y := by - rw [← IsScalarTower.algebraMap_smul R a x, polar_smul_left, Algebra.smul_def] -#align quadratic_form.polar_smul_left_of_tower QuadraticForm.polar_smul_left_of_tower + rw [← IsScalarTower.algebraMap_smul R a x, polar_smul_left, algebraMap_smul] +#align quadratic_form.polar_smul_left_of_tower QuadraticMap.polar_smul_left_of_tower @[simp] theorem polar_smul_right_of_tower (a : S) (x y : M) : polar Q x (a • y) = a • polar Q x y := by - rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, Algebra.smul_def] -#align quadratic_form.polar_smul_right_of_tower QuadraticForm.polar_smul_right_of_tower + rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, algebraMap_smul] +#align quadratic_form.polar_smul_right_of_tower QuadraticMap.polar_smul_right_of_tower -/-- An alternative constructor to `QuadraticForm.mk`, for rings where `polar` can be used. -/ +/-- An alternative constructor to `QuadraticMap.mk`, for rings where `polar` can be used. -/ @[simps] -def ofPolar (toFun : M → R) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = a * a * toFun x) +def ofPolar (toFun : M → N) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x) (polar_add_left : ∀ x x' y : M, polar toFun (x + x') y = polar toFun x y + polar toFun x' y) (polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y) : - QuadraticForm R M := + QuadraticMap R M N := { toFun toFun_smul exists_companion' := ⟨LinearMap.mk₂ R (polar toFun) (polar_add_left) (polar_smul_left) @@ -351,78 +365,79 @@ def ofPolar (toFun : M → R) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) fun _ _ ↦ by simp only [LinearMap.mk₂_apply] rw [polar, sub_sub, add_sub_cancel]⟩ } -#align quadratic_form.of_polar QuadraticForm.ofPolar +#align quadratic_form.of_polar QuadraticMap.ofPolar -/-- In a ring the companion bilinear form is unique and equal to `QuadraticForm.polar`. -/ +/-- In a ring the companion bilinear form is unique and equal to `QuadraticMap.polar`. -/ theorem choose_exists_companion : Q.exists_companion.choose = polarBilin Q := LinearMap.ext₂ fun x y => by rw [polarBilin_apply_apply, polar, Q.exists_companion.choose_spec, sub_sub, add_sub_cancel_left] -#align quadratic_form.some_exists_companion QuadraticForm.choose_exists_companion +#align quadratic_form.some_exists_companion QuadraticMap.choose_exists_companion end CommRing section SemiringOperators -variable [CommSemiring R] [AddCommMonoid M] [Module R M] +variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] section SMul -variable [Monoid S] [Monoid T] [DistribMulAction S R] [DistribMulAction T R] -variable [SMulCommClass S R R] [SMulCommClass T R R] +variable [Monoid S] [Monoid T] [DistribMulAction S N] [DistribMulAction T N] +variable [SMulCommClass S R N] [SMulCommClass T R N] -/-- `QuadraticForm R M` inherits the scalar action from any algebra over `R`. +/-- `QuadraticMap R M N` inherits the scalar action from any algebra over `R`. This provides an `R`-action via `Algebra.id`. -/ -instance : SMul S (QuadraticForm R M) := +instance : SMul S (QuadraticMap R M N) := ⟨fun a Q => { toFun := a • ⇑Q - toFun_smul := fun b x => by rw [Pi.smul_apply, map_smul, Pi.smul_apply, mul_smul_comm] + toFun_smul := fun b x => by + rw [Pi.smul_apply, map_smul, Pi.smul_apply, smul_comm] exists_companion' := let ⟨B, h⟩ := Q.exists_companion - letI := SMulCommClass.symm S R R + letI := SMulCommClass.symm S R N ⟨a • B, by simp [h]⟩ }⟩ @[simp] -theorem coeFn_smul (a : S) (Q : QuadraticForm R M) : ⇑(a • Q) = a • ⇑Q := +theorem coeFn_smul (a : S) (Q : QuadraticMap R M N) : ⇑(a • Q) = a • ⇑Q := rfl -#align quadratic_form.coe_fn_smul QuadraticForm.coeFn_smul +#align quadratic_form.coe_fn_smul QuadraticMap.coeFn_smul @[simp] -theorem smul_apply (a : S) (Q : QuadraticForm R M) (x : M) : (a • Q) x = a • Q x := +theorem smul_apply (a : S) (Q : QuadraticMap R M N) (x : M) : (a • Q) x = a • Q x := rfl -#align quadratic_form.smul_apply QuadraticForm.smul_apply +#align quadratic_form.smul_apply QuadraticMap.smul_apply -instance [SMulCommClass S T R] : SMulCommClass S T (QuadraticForm R M) where +instance [SMulCommClass S T N] : SMulCommClass S T (QuadraticMap R M N) where smul_comm _s _t _q := ext fun _ => smul_comm _ _ _ -instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T (QuadraticForm R M) where +instance [SMul S T] [IsScalarTower S T N] : IsScalarTower S T (QuadraticMap R M N) where smul_assoc _s _t _q := ext fun _ => smul_assoc _ _ _ end SMul -instance : Zero (QuadraticForm R M) := +instance : Zero (QuadraticMap R M N) := ⟨{ toFun := fun _ => 0 - toFun_smul := fun a _ => by simp only [mul_zero] + toFun_smul := fun a _ => by simp only [smul_zero] exists_companion' := ⟨0, fun _ _ => by simp only [add_zero, LinearMap.zero_apply]⟩ }⟩ @[simp] -theorem coeFn_zero : ⇑(0 : QuadraticForm R M) = 0 := +theorem coeFn_zero : ⇑(0 : QuadraticMap R M N) = 0 := rfl -#align quadratic_form.coe_fn_zero QuadraticForm.coeFn_zero +#align quadratic_form.coe_fn_zero QuadraticMap.coeFn_zero @[simp] -theorem zero_apply (x : M) : (0 : QuadraticForm R M) x = 0 := +theorem zero_apply (x : M) : (0 : QuadraticMap R M N) x = 0 := rfl -#align quadratic_form.zero_apply QuadraticForm.zero_apply +#align quadratic_form.zero_apply QuadraticMap.zero_apply -instance : Inhabited (QuadraticForm R M) := +instance : Inhabited (QuadraticMap R M N) := ⟨0⟩ -instance : Add (QuadraticForm R M) := +instance : Add (QuadraticMap R M N) := ⟨fun Q Q' => { toFun := Q + Q' - toFun_smul := fun a x => by simp only [Pi.add_apply, map_smul, mul_add] + toFun_smul := fun a x => by simp only [Pi.add_apply, smul_add, map_smul] exists_companion' := let ⟨B, h⟩ := Q.exists_companion let ⟨B', h'⟩ := Q'.exists_companion @@ -430,54 +445,54 @@ instance : Add (QuadraticForm R M) := simp_rw [Pi.add_apply, h, h', LinearMap.add_apply, add_add_add_comm]⟩ }⟩ @[simp] -theorem coeFn_add (Q Q' : QuadraticForm R M) : ⇑(Q + Q') = Q + Q' := +theorem coeFn_add (Q Q' : QuadraticMap R M N) : ⇑(Q + Q') = Q + Q' := rfl -#align quadratic_form.coe_fn_add QuadraticForm.coeFn_add +#align quadratic_form.coe_fn_add QuadraticMap.coeFn_add @[simp] -theorem add_apply (Q Q' : QuadraticForm R M) (x : M) : (Q + Q') x = Q x + Q' x := +theorem add_apply (Q Q' : QuadraticMap R M N) (x : M) : (Q + Q') x = Q x + Q' x := rfl -#align quadratic_form.add_apply QuadraticForm.add_apply +#align quadratic_form.add_apply QuadraticMap.add_apply -instance : AddCommMonoid (QuadraticForm R M) := +instance : AddCommMonoid (QuadraticMap R M N) := DFunLike.coe_injective.addCommMonoid _ coeFn_zero coeFn_add fun _ _ => coeFn_smul _ _ -/-- `@CoeFn (QuadraticForm R M)` as an `AddMonoidHom`. +/-- `@CoeFn (QuadraticMap R M)` as an `AddMonoidHom`. This API mirrors `AddMonoidHom.coeFn`. -/ @[simps apply] -def coeFnAddMonoidHom : QuadraticForm R M →+ M → R where +def coeFnAddMonoidHom : QuadraticMap R M N →+ M → N where toFun := DFunLike.coe map_zero' := coeFn_zero map_add' := coeFn_add -#align quadratic_form.coe_fn_add_monoid_hom QuadraticForm.coeFnAddMonoidHom +#align quadratic_form.coe_fn_add_monoid_hom QuadraticMap.coeFnAddMonoidHom -/-- Evaluation on a particular element of the module `M` is an additive map over quadratic forms. -/ +/-- Evaluation on a particular element of the module `M` is an additive map on quadratic maps. -/ @[simps! apply] -def evalAddMonoidHom (m : M) : QuadraticForm R M →+ R := +def evalAddMonoidHom (m : M) : QuadraticMap R M N →+ N := (Pi.evalAddMonoidHom _ m).comp coeFnAddMonoidHom -#align quadratic_form.eval_add_monoid_hom QuadraticForm.evalAddMonoidHom +#align quadratic_form.eval_add_monoid_hom QuadraticMap.evalAddMonoidHom section Sum @[simp] -theorem coeFn_sum {ι : Type*} (Q : ι → QuadraticForm R M) (s : Finset ι) : +theorem coeFn_sum {ι : Type*} (Q : ι → QuadraticMap R M N) (s : Finset ι) : ⇑(∑ i ∈ s, Q i) = ∑ i ∈ s, ⇑(Q i) := map_sum coeFnAddMonoidHom Q s -#align quadratic_form.coe_fn_sum QuadraticForm.coeFn_sum +#align quadratic_form.coe_fn_sum QuadraticMap.coeFn_sum @[simp] -theorem sum_apply {ι : Type*} (Q : ι → QuadraticForm R M) (s : Finset ι) (x : M) : +theorem sum_apply {ι : Type*} (Q : ι → QuadraticMap R M N) (s : Finset ι) (x : M) : (∑ i ∈ s, Q i) x = ∑ i ∈ s, Q i x := - map_sum (evalAddMonoidHom x : _ →+ R) Q s -#align quadratic_form.sum_apply QuadraticForm.sum_apply + map_sum (evalAddMonoidHom x : _ →+ N) Q s +#align quadratic_form.sum_apply QuadraticMap.sum_apply end Sum -instance [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] : - DistribMulAction S (QuadraticForm R M) where +instance [Monoid S] [DistribMulAction S N] [SMulCommClass S R N] : + DistribMulAction S (QuadraticMap R M N) where mul_smul a b Q := ext fun x => by simp only [smul_apply, mul_smul] - one_smul Q := ext fun x => by simp only [QuadraticForm.smul_apply, one_smul] + one_smul Q := ext fun x => by simp only [QuadraticMap.smul_apply, one_smul] smul_add a Q Q' := by ext simp only [add_apply, smul_apply, smul_add] @@ -485,8 +500,8 @@ instance [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] : ext simp only [zero_apply, smul_apply, smul_zero] -instance [Semiring S] [Module S R] [SMulCommClass S R R] : - Module S (QuadraticForm R M) where +instance [Semiring S] [Module S N] [SMulCommClass S R N] : + Module S (QuadraticMap R M N) where zero_smul Q := by ext simp only [zero_apply, smul_apply, zero_smul] @@ -498,397 +513,435 @@ end SemiringOperators section RingOperators -variable [CommRing R] [AddCommGroup M] [Module R M] +variable [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] -instance : Neg (QuadraticForm R M) := +instance : Neg (QuadraticMap R M N) := ⟨fun Q => { toFun := -Q - toFun_smul := fun a x => by simp only [Pi.neg_apply, map_smul, mul_neg] + toFun_smul := fun a x => by simp only [Pi.neg_apply, map_smul, smul_neg] exists_companion' := let ⟨B, h⟩ := Q.exists_companion ⟨-B, fun x y => by simp_rw [Pi.neg_apply, h, LinearMap.neg_apply, neg_add]⟩ }⟩ @[simp] -theorem coeFn_neg (Q : QuadraticForm R M) : ⇑(-Q) = -Q := +theorem coeFn_neg (Q : QuadraticMap R M N) : ⇑(-Q) = -Q := rfl -#align quadratic_form.coe_fn_neg QuadraticForm.coeFn_neg +#align quadratic_form.coe_fn_neg QuadraticMap.coeFn_neg @[simp] -theorem neg_apply (Q : QuadraticForm R M) (x : M) : (-Q) x = -Q x := +theorem neg_apply (Q : QuadraticMap R M N) (x : M) : (-Q) x = -Q x := rfl -#align quadratic_form.neg_apply QuadraticForm.neg_apply +#align quadratic_form.neg_apply QuadraticMap.neg_apply -instance : Sub (QuadraticForm R M) := +instance : Sub (QuadraticMap R M N) := ⟨fun Q Q' => (Q + -Q').copy (Q - Q') (sub_eq_add_neg _ _)⟩ @[simp] -theorem coeFn_sub (Q Q' : QuadraticForm R M) : ⇑(Q - Q') = Q - Q' := +theorem coeFn_sub (Q Q' : QuadraticMap R M N) : ⇑(Q - Q') = Q - Q' := rfl -#align quadratic_form.coe_fn_sub QuadraticForm.coeFn_sub +#align quadratic_form.coe_fn_sub QuadraticMap.coeFn_sub @[simp] -theorem sub_apply (Q Q' : QuadraticForm R M) (x : M) : (Q - Q') x = Q x - Q' x := +theorem sub_apply (Q Q' : QuadraticMap R M N) (x : M) : (Q - Q') x = Q x - Q' x := rfl -#align quadratic_form.sub_apply QuadraticForm.sub_apply +#align quadratic_form.sub_apply QuadraticMap.sub_apply -instance : AddCommGroup (QuadraticForm R M) := +instance : AddCommGroup (QuadraticMap R M N) := DFunLike.coe_injective.addCommGroup _ coeFn_zero coeFn_add coeFn_neg coeFn_sub (fun _ _ => coeFn_smul _ _) fun _ _ => coeFn_smul _ _ end RingOperators +section restrictScalars + +variable [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] + [Module R N] [Module S M] [Module S N] [Algebra S R] +variable [IsScalarTower S R M] [IsScalarTower S R N] + +/-- If `B : M → N → Pₗ` is `R`-`S` bilinear and `R'` and `S'` are compatible scalar multiplications, +then the restriction of scalars is a `R'`-`S'` bilinear map. -/ +@[simps!] +def restrictScalars (Q : QuadraticMap R M N) : QuadraticMap S M N where + toFun x := Q x + toFun_smul a x := by + simp [map_smul_of_tower] + exists_companion' := + let ⟨B, h⟩ := Q.exists_companion + ⟨B.restrictScalars₁₂ (S := R) (R' := S) (S' := S), fun x y => by + simp only [LinearMap.restrictScalars₁₂_apply_apply, h]⟩ + +end restrictScalars + section Comp -variable [CommSemiring R] [AddCommMonoid M] [Module R M] -variable [AddCommMonoid N] [Module R N] +variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] +variable [AddCommMonoid P] [Module R P] -/-- Compose the quadratic form with a linear function. -/ -def comp (Q : QuadraticForm R N) (f : M →ₗ[R] N) : QuadraticForm R M where +/-- Compose the quadratic map with a linear function on the right. -/ +def comp (Q : QuadraticMap R N P) (f : M →ₗ[R] N) : QuadraticMap R M P where toFun x := Q (f x) toFun_smul a x := by simp only [map_smul, f.map_smul] exists_companion' := let ⟨B, h⟩ := Q.exists_companion ⟨B.compl₁₂ f f, fun x y => by simp_rw [f.map_add]; exact h (f x) (f y)⟩ -#align quadratic_form.comp QuadraticForm.comp +#align quadratic_form.comp QuadraticMap.comp @[simp] -theorem comp_apply (Q : QuadraticForm R N) (f : M →ₗ[R] N) (x : M) : (Q.comp f) x = Q (f x) := +theorem comp_apply (Q : QuadraticMap R N P) (f : M →ₗ[R] N) (x : M) : (Q.comp f) x = Q (f x) := rfl -#align quadratic_form.comp_apply QuadraticForm.comp_apply +#align quadratic_form.comp_apply QuadraticMap.comp_apply -/-- Compose a quadratic form with a linear function on the left. -/ +/-- Compose a quadratic map with a linear function on the left. -/ @[simps (config := { simpRhs := true })] -def _root_.LinearMap.compQuadraticForm [CommSemiring S] [Algebra S R] [Module S M] - [IsScalarTower S R M] (f : R →ₗ[S] S) (Q : QuadraticForm R M) : QuadraticForm S M where +def _root_.LinearMap.compQuadraticMap (f : N →ₗ[R] P) (Q : QuadraticMap R M N) : + QuadraticMap R M P where toFun x := f (Q x) - toFun_smul b x := by simp only [Q.map_smul_of_tower b x, f.map_smul, smul_eq_mul] + toFun_smul b x := by simp only [map_smul, f.map_smul] exists_companion' := let ⟨B, h⟩ := Q.exists_companion - ⟨(B.restrictScalars₁₂ S S).compr₂ f, fun x y => by - simp_rw [h, f.map_add, LinearMap.compr₂_apply, LinearMap.restrictScalars₁₂_apply_apply]⟩ -#align linear_map.comp_quadratic_form LinearMap.compQuadraticForm + ⟨B.compr₂ f, fun x y => by simp only [h, map_add, LinearMap.compr₂_apply]⟩ -end Comp +/-- Compose a quadratic map with a linear function on the left. -/ +@[simps! (config := { simpRhs := true })] +def _root_.LinearMap.compQuadraticMap' [CommSemiring S] [Algebra S R] [Module S N] [Module S M] + [IsScalarTower S R N] [IsScalarTower S R M] [Module S P] + (f : N →ₗ[S] P) (Q : QuadraticMap R M N) : QuadraticMap S M P := + _root_.LinearMap.compQuadraticMap f Q.restrictScalars +#align linear_map.comp_quadratic_form LinearMap.compQuadraticMap' -section CommRing +end Comp +section NonUnitalNonAssocSemiring -variable [CommSemiring R] [AddCommMonoid M] [Module R M] +variable [CommSemiring R] [NonUnitalNonAssocSemiring A] [AddCommMonoid M] [Module R M] +variable [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] /-- The product of linear forms is a quadratic form. -/ -def linMulLin (f g : M →ₗ[R] R) : QuadraticForm R M where +def linMulLin (f g : M →ₗ[R] A) : QuadraticMap R M A where toFun := f * g toFun_smul a x := by - simp only [smul_eq_mul, RingHom.id_apply, Pi.mul_apply, LinearMap.map_smulₛₗ] - ring + rw [Pi.mul_apply, Pi.mul_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, LinearMap.map_smulₛₗ, + RingHom.id_apply, smul_mul_assoc, mul_smul_comm, ← smul_assoc, (smul_eq_mul R)] exists_companion' := - ⟨(LinearMap.mul R R).compl₁₂ f g + (LinearMap.mul R R).compl₁₂ g f, fun x y => by - simp only [Pi.mul_apply, map_add, LinearMap.compl₁₂_apply, LinearMap.mul_apply', - LinearMap.add_apply] - ring_nf⟩ -#align quadratic_form.lin_mul_lin QuadraticForm.linMulLin + ⟨(LinearMap.mul R A).compl₁₂ f g + (LinearMap.mul R A).flip.compl₁₂ g f, fun x y => by + simp only [Pi.mul_apply, map_add, left_distrib, right_distrib, LinearMap.add_apply, + LinearMap.compl₁₂_apply, LinearMap.mul_apply', LinearMap.flip_apply] + abel_nf⟩ +#align quadratic_form.lin_mul_lin QuadraticMap.linMulLin @[simp] -theorem linMulLin_apply (f g : M →ₗ[R] R) (x) : linMulLin f g x = f x * g x := +theorem linMulLin_apply (f g : M →ₗ[R] A) (x) : linMulLin f g x = f x * g x := rfl -#align quadratic_form.lin_mul_lin_apply QuadraticForm.linMulLin_apply +#align quadratic_form.lin_mul_lin_apply QuadraticMap.linMulLin_apply @[simp] -theorem add_linMulLin (f g h : M →ₗ[R] R) : linMulLin (f + g) h = linMulLin f h + linMulLin g h := +theorem add_linMulLin (f g h : M →ₗ[R] A) : linMulLin (f + g) h = linMulLin f h + linMulLin g h := ext fun _ => add_mul _ _ _ -#align quadratic_form.add_lin_mul_lin QuadraticForm.add_linMulLin +#align quadratic_form.add_lin_mul_lin QuadraticMap.add_linMulLin @[simp] -theorem linMulLin_add (f g h : M →ₗ[R] R) : linMulLin f (g + h) = linMulLin f g + linMulLin f h := +theorem linMulLin_add (f g h : M →ₗ[R] A) : linMulLin f (g + h) = linMulLin f g + linMulLin f h := ext fun _ => mul_add _ _ _ -#align quadratic_form.lin_mul_lin_add QuadraticForm.linMulLin_add +#align quadratic_form.lin_mul_lin_add QuadraticMap.linMulLin_add -variable [AddCommMonoid N] [Module R N] +variable {N' : Type*} [AddCommMonoid N'] [Module R N'] @[simp] -theorem linMulLin_comp (f g : M →ₗ[R] R) (h : N →ₗ[R] M) : +theorem linMulLin_comp (f g : M →ₗ[R] A) (h : N' →ₗ[R] M) : (linMulLin f g).comp h = linMulLin (f.comp h) (g.comp h) := rfl -#align quadratic_form.lin_mul_lin_comp QuadraticForm.linMulLin_comp +#align quadratic_form.lin_mul_lin_comp QuadraticMap.linMulLin_comp variable {n : Type*} -/-- `sq` is the quadratic form mapping the vector `x : R` to `x * x` -/ +/-- `sq` is the quadratic form mapping the vector `x : A` to `x * x` -/ @[simps!] -def sq : QuadraticForm R R := +def sq : QuadraticMap R A A := linMulLin LinearMap.id LinearMap.id -#align quadratic_form.sq QuadraticForm.sq +#align quadratic_form.sq QuadraticMap.sq /-- `proj i j` is the quadratic form mapping the vector `x : n → R` to `x i * x j` -/ -def proj (i j : n) : QuadraticForm R (n → R) := - linMulLin (@LinearMap.proj _ _ _ (fun _ => R) _ _ i) (@LinearMap.proj _ _ _ (fun _ => R) _ _ j) -#align quadratic_form.proj QuadraticForm.proj +def proj (i j : n) : QuadraticMap R (n → A) A := + linMulLin (@LinearMap.proj _ _ _ (fun _ => A) _ _ i) (@LinearMap.proj _ _ _ (fun _ => A) _ _ j) +#align quadratic_form.proj QuadraticMap.proj @[simp] -theorem proj_apply (i j : n) (x : n → R) : proj i j x = x i * x j := +theorem proj_apply (i j : n) (x : n → A) : proj (R := R) i j x = x i * x j := rfl -#align quadratic_form.proj_apply QuadraticForm.proj_apply +#align quadratic_form.proj_apply QuadraticMap.proj_apply -end CommRing +end NonUnitalNonAssocSemiring -end QuadraticForm +end QuadraticMap /-! -### Associated bilinear forms +### Associated bilinear maps -Over a commutative ring with an inverse of 2, the theory of quadratic forms is -basically identical to that of symmetric bilinear forms. The map from quadratic -forms to bilinear forms giving this identification is called the `associated` -quadratic form. +Over a commutative ring with an inverse of 2, the theory of quadratic maps is +basically identical to that of symmetric bilinear maps. The map from quadratic +maps to bilinear maps giving this identification is called the `associated` +quadratic map. -/ namespace LinearMap -namespace BilinForm +namespace BilinMap -open QuadraticForm +open QuadraticMap +open LinearMap (BilinMap) section Semiring -variable [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] +variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] +variable {N' : Type*} [AddCommMonoid N'] [Module R N'] -/-- A bilinear map into `R` gives a quadratic form by applying the argument twice. -/ -def toQuadraticForm (B : BilinForm R M) : QuadraticForm R M where +/-- A bilinear map gives a quadratic map by applying the argument twice. -/ +def toQuadraticMap (B : BilinMap R M N) : QuadraticMap R M N where toFun x := B x x - toFun_smul a x := by - simp only [_root_.map_smul, LinearMap.smul_apply, smul_eq_mul, mul_assoc] - exists_companion' := ⟨B + B.flip, - fun x y => by simp only [map_add, LinearMap.add_apply, LinearMap.flip_apply]; abel⟩ -#align bilin_form.to_quadratic_form LinearMap.BilinForm.toQuadraticForm - -variable {B : BilinForm R M} + toFun_smul a x := by simp only [_root_.map_smul, LinearMap.smul_apply, smul_smul] + exists_companion' := ⟨B + LinearMap.flip B, fun x y => by simp [add_add_add_comm, add_comm]⟩ +#align bilin_form.to_quadratic_form LinearMap.BilinMap.toQuadraticMap @[simp] -theorem toQuadraticForm_apply (B : BilinForm R M) (x : M) : B.toQuadraticForm x = B x x := +theorem toQuadraticMap_apply (B : BilinMap R M N) (x : M) : B.toQuadraticMap x = B x x := rfl -#align bilin_form.to_quadratic_form_apply LinearMap.BilinForm.toQuadraticForm_apply +#align bilin_form.to_quadratic_form_apply LinearMap.BilinMap.toQuadraticMap_apply -theorem toQuadraticForm_comp_same (B : BilinForm R N) (f : M →ₗ[R] N) : - BilinForm.toQuadraticForm (B.compl₁₂ f f) = B.toQuadraticForm.comp f := rfl +theorem toQuadraticMap_comp_same (B : BilinMap R M N) (f : N' →ₗ[R] M) : + BilinMap.toQuadraticMap (B.compl₁₂ f f) = B.toQuadraticMap.comp f := rfl section variable (R M) @[simp] -theorem toQuadraticForm_zero : (0 : BilinForm R M).toQuadraticForm = 0 := +theorem toQuadraticMap_zero : (0 : BilinMap R M N).toQuadraticMap = 0 := rfl -#align bilin_form.to_quadratic_form_zero LinearMap.BilinForm.toQuadraticForm_zero +#align bilin_form.to_quadratic_form_zero LinearMap.BilinMap.toQuadraticMap_zero end @[simp] -theorem toQuadraticForm_add (B₁ B₂ : BilinForm R M) : - (B₁ + B₂).toQuadraticForm = B₁.toQuadraticForm + B₂.toQuadraticForm := +theorem toQuadraticMap_add (B₁ B₂ : BilinMap R M N) : + (B₁ + B₂).toQuadraticMap = B₁.toQuadraticMap + B₂.toQuadraticMap := rfl -#align bilin_form.to_quadratic_form_add LinearMap.BilinForm.toQuadraticForm_add +#align bilin_form.to_quadratic_form_add LinearMap.BilinMap.toQuadraticMap_add @[simp] -theorem toQuadraticForm_smul [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] - (a : S) (B : BilinForm R M) : - letI := SMulCommClass.symm S R R - (a • B).toQuadraticForm = a • B.toQuadraticForm := +theorem toQuadraticMap_smul [Monoid S] [DistribMulAction S N] [SMulCommClass S R N] + [SMulCommClass R S N] (a : S) + (B : BilinMap R M N) : (a • B).toQuadraticMap = a • B.toQuadraticMap := rfl -#align bilin_form.to_quadratic_form_smul LinearMap.BilinForm.toQuadraticForm_smul +#align bilin_form.to_quadratic_form_smul LinearMap.BilinMap.toQuadraticMap_smul section variable (S R M) -/-- `LinearMap.BilinForm.toQuadraticForm` as an additive homomorphism -/ +/-- `LinearMap.BilinForm.toQuadraticMap` as an additive homomorphism -/ @[simps] -def toQuadraticFormAddMonoidHom : BilinForm R M →+ QuadraticForm R M where - toFun := toQuadraticForm - map_zero' := toQuadraticForm_zero _ _ - map_add' := toQuadraticForm_add -#align bilin_form.to_quadratic_form_add_monoid_hom LinearMap.BilinForm.toQuadraticFormAddMonoidHom +def toQuadraticMapAddMonoidHom : (BilinMap R M N) →+ QuadraticMap R M N where + toFun := toQuadraticMap + map_zero' := toQuadraticMap_zero _ _ + map_add' := toQuadraticMap_add +#align bilin_form.to_quadratic_form_add_monoid_hom LinearMap.BilinMap.toQuadraticMapAddMonoidHom -/-- `LinearMap.BilinForm.toQuadraticForm` as a linear map -/ +/-- `LinearMap.BilinForm.toQuadraticMap` as a linear map -/ @[simps!] -def toQuadraticFormLinearMap [Semiring S] [Module S R] [SMulCommClass S R R] [SMulCommClass R S R] : - BilinForm R M →ₗ[S] QuadraticForm R M where - toFun := toQuadraticForm - map_smul' := toQuadraticForm_smul - map_add' := toQuadraticForm_add +def toQuadraticMapLinearMap [Semiring S] [Module S N] [SMulCommClass S R N] [SMulCommClass R S N] : + (BilinMap R M N) →ₗ[S] QuadraticMap R M N where + toFun := toQuadraticMap + map_smul' := toQuadraticMap_smul + map_add' := toQuadraticMap_add end @[simp] -theorem toQuadraticForm_list_sum (B : List (BilinForm R M)) : - B.sum.toQuadraticForm = (B.map toQuadraticForm).sum := - map_list_sum (toQuadraticFormAddMonoidHom R M) B -#align bilin_form.to_quadratic_form_list_sum LinearMap.BilinForm.toQuadraticForm_list_sum +theorem toQuadraticMap_list_sum (B : List (BilinMap R M N)) : + B.sum.toQuadraticMap = (B.map toQuadraticMap).sum := + map_list_sum (toQuadraticMapAddMonoidHom R M) B +#align bilin_form.to_quadratic_form_list_sum LinearMap.BilinMap.toQuadraticMap_list_sum @[simp] -theorem toQuadraticForm_multiset_sum (B : Multiset (BilinForm R M)) : - B.sum.toQuadraticForm = (B.map toQuadraticForm).sum := - map_multiset_sum (toQuadraticFormAddMonoidHom R M) B -#align bilin_form.to_quadratic_form_multiset_sum LinearMap.BilinForm.toQuadraticForm_multiset_sum +theorem toQuadraticMap_multiset_sum (B : Multiset (BilinMap R M N)) : + B.sum.toQuadraticMap = (B.map toQuadraticMap).sum := + map_multiset_sum (toQuadraticMapAddMonoidHom R M) B +#align bilin_form.to_quadratic_form_multiset_sum LinearMap.BilinMap.toQuadraticMap_multiset_sum @[simp] -theorem toQuadraticForm_sum {ι : Type*} (s : Finset ι) (B : ι → BilinForm R M) : - (∑ i ∈ s, B i).toQuadraticForm = ∑ i ∈ s, (B i).toQuadraticForm := - map_sum (toQuadraticFormAddMonoidHom R M) B s -#align bilin_form.to_quadratic_form_sum LinearMap.BilinForm.toQuadraticForm_sum +theorem toQuadraticMap_sum {ι : Type*} (s : Finset ι) (B : ι → (BilinMap R M N)) : + (∑ i ∈ s, B i).toQuadraticMap = ∑ i ∈ s, (B i).toQuadraticMap := + map_sum (toQuadraticMapAddMonoidHom R M) B s +#align bilin_form.to_quadratic_form_sum LinearMap.BilinMap.toQuadraticMap_sum @[simp] -theorem toQuadraticForm_eq_zero {B : BilinForm R M} : B.toQuadraticForm = 0 ↔ B.IsAlt := - QuadraticForm.ext_iff -#align bilin_form.to_quadratic_form_eq_zero LinearMap.BilinForm.toQuadraticForm_eq_zero +theorem toQuadraticMap_eq_zero {B : BilinMap R M N} : + B.toQuadraticMap = 0 ↔ B.IsAlt := + QuadraticMap.ext_iff +#align bilin_form.to_quadratic_form_eq_zero LinearMap.BilinMap.toQuadraticMap_eq_zero end Semiring section Ring -open QuadraticForm - -variable [CommRing R] [AddCommGroup M] [Module R M] -variable {B : BilinForm R M} +variable [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] +variable {B : BilinMap R M N} @[simp] -theorem toQuadraticForm_neg (B : BilinForm R M) : (-B).toQuadraticForm = -B.toQuadraticForm := +theorem toQuadraticMap_neg (B : BilinMap R M N) : (-B).toQuadraticMap = -B.toQuadraticMap := rfl -#align bilin_form.to_quadratic_form_neg LinearMap.BilinForm.toQuadraticForm_neg +#align bilin_form.to_quadratic_form_neg LinearMap.BilinMap.toQuadraticMap_neg @[simp] -theorem toQuadraticForm_sub (B₁ B₂ : BilinForm R M) : - (B₁ - B₂).toQuadraticForm = B₁.toQuadraticForm - B₂.toQuadraticForm := +theorem toQuadraticMap_sub (B₁ B₂ : BilinMap R M N) : + (B₁ - B₂).toQuadraticMap = B₁.toQuadraticMap - B₂.toQuadraticMap := rfl -#align bilin_form.to_quadratic_form_sub LinearMap.BilinForm.toQuadraticForm_sub +#align bilin_form.to_quadratic_form_sub LinearMap.BilinMap.toQuadraticMap_sub -theorem polar_toQuadraticForm (x y : M) : polar (toQuadraticForm B) x y = B x y + B y x := by - simp only [toQuadraticForm_apply, add_assoc, add_sub_cancel_left, add_apply, polar, add_left_inj, - add_neg_cancel_left, map_add, sub_eq_add_neg _ (B y y), add_comm (B y x) _] -#align bilin_form.polar_to_quadratic_form LinearMap.BilinForm.polar_toQuadraticForm +theorem polar_toQuadraticMap (x y : M) : polar (toQuadraticMap B) x y = B x y + B y x := by + simp only [polar, toQuadraticMap_apply, map_add, add_apply, add_assoc, add_comm (B y x) _, + add_sub_cancel_left, sub_eq_add_neg _ (B y y), add_neg_cancel_left] +#align bilin_form.polar_to_quadratic_form LinearMap.BilinMap.polar_toQuadraticMap -theorem polarBilin_toQuadraticForm : polarBilin (toQuadraticForm B) = B + B.flip := - ext₂ polar_toQuadraticForm +theorem polarBilin_toQuadraticMap : polarBilin (toQuadraticMap B) = B + flip B := + LinearMap.ext₂ polar_toQuadraticMap -@[simp] theorem _root_.QuadraticForm.toQuadraticForm_polarBilin (Q : QuadraticForm R M) : - toQuadraticForm (polarBilin Q) = 2 • Q := - QuadraticForm.ext fun x => (polar_self _ x).trans <| by simp +@[simp] theorem _root_.QuadraticMap.toQuadraticMap_polarBilin (Q : QuadraticMap R M N) : + toQuadraticMap (polarBilin Q) = 2 • Q := + QuadraticMap.ext fun x => (polar_self _ x).trans <| by simp -theorem _root_.QuadraticForm.polarBilin_injective (h : IsUnit (2 : R)) : - Function.Injective (polarBilin : QuadraticForm R M → _) := - fun Q₁ Q₂ h₁₂ => QuadraticForm.ext fun x => h.mul_left_cancel <| by - simpa using DFunLike.congr_fun (congr_arg toQuadraticForm h₁₂) x +theorem _root_.QuadraticMap.polarBilin_injective (h : IsUnit (2 : R)) : + Function.Injective (polarBilin : QuadraticMap R M N → _) := by + intro Q₁ Q₂ h₁₂ + apply h.smul_left_cancel.mp + rw [show (2 : R) = (2 : ℕ) by rfl] + simp_rw [← nsmul_eq_smul_cast R, ← QuadraticMap.toQuadraticMap_polarBilin] + exact congrArg toQuadraticMap h₁₂ +section + +variable {N' : Type*} [AddCommGroup N'] [Module R N'] variable [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M] -variable [AddCommGroup N] [Module R N] -theorem _root_.QuadraticForm.polarBilin_comp (Q : QuadraticForm R N) (f : M →ₗ[R] N) : - polarBilin (Q.comp f) = compl₁₂ (polarBilin Q) f f := - ext₂ fun x y => by simp [polar] +theorem _root_.QuadraticMap.polarBilin_comp (Q : QuadraticMap R N' N) (f : M →ₗ[R] N') : + polarBilin (Q.comp f) = LinearMap.compl₁₂ (polarBilin Q) f f := + LinearMap.ext₂ <| fun x y => by simp [polar] + +end + +variable {N' : Type*} [AddCommGroup N'] [Module R N'] -theorem compQuadraticForm_polar (f : R →ₗ[S] S) (Q : QuadraticForm R M) (x y : M) : - polar (f.compQuadraticForm Q) x y = f (polar Q x y) := by +theorem _root_.LinearMap.compQuadraticMap_polar [CommSemiring S] [Algebra S R] [Module S N] + [Module S N'] [IsScalarTower S R N] [Module S M] [IsScalarTower S R M] (f : N →ₗ[S] N') + (Q : QuadraticMap R M N) (x y : M) : polar (f.compQuadraticMap' Q) x y = f (polar Q x y) := by simp [polar] -theorem compQuadraticForm_polarBilin (f : R →ₗ[S] S) (Q : QuadraticForm R M) : - (f.compQuadraticForm Q).polarBilin = - (Q.polarBilin.restrictScalars₁₂ S S).compr₂ f := - ext₂ <| compQuadraticForm_polar _ _ +theorem _root_.LinearMap.compQuadraticMap_polarBilin (f : N →ₗ[R] N') (Q : QuadraticMap R M N) : + (f.compQuadraticMap' Q).polarBilin = Q.polarBilin.compr₂ f := by + ext + rw [polarBilin_apply_apply, compr₂_apply, polarBilin_apply_apply, + LinearMap.compQuadraticMap_polar] end Ring -end BilinForm +end BilinMap end LinearMap -namespace QuadraticForm +namespace QuadraticMap -open LinearMap.BilinForm +open LinearMap (BilinMap) section AssociatedHom -variable [CommRing R] [AddCommGroup M] [Module R M] +variable [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] variable (S) [CommSemiring S] [Algebra S R] -variable [Invertible (2 : R)] {B₁ : BilinForm R M} +variable [Module S N] [IsScalarTower S R N] +variable [Invertible (2 : R)] {B₁ : BilinMap R M R} -/-- `associatedHom` is the map that sends a quadratic form on a module `M` over `R` to its -associated symmetric bilinear form. As provided here, this has the structure of an `S`-linear map +/-- `associatedHom` is the map that sends a quadratic map on a module `M` over `R` to its +associated symmetric bilinear map. As provided here, this has the structure of an `S`-linear map where `S` is a commutative subring of `R`. -Over a commutative ring, use `QuadraticForm.associated`, which gives an `R`-linear map. Over a -general ring with no nontrivial distinguished commutative subring, use `QuadraticForm.associated'`, +Over a commutative ring, use `QuadraticMap.associated`, which gives an `R`-linear map. Over a +general ring with no nontrivial distinguished commutative subring, use `QuadraticMap.associated'`, which gives an additive homomorphism (or more precisely a `ℤ`-linear map.) -/ -def associatedHom : QuadraticForm R M →ₗ[S] BilinForm R M := +def associatedHom : QuadraticMap R M N →ₗ[S] (BilinMap R M N) := -- TODO: this `center` stuff is vertigial from an incorrect non-commutative version, but we leave -- it behind to make a future refactor to a *correct* non-commutative version easier in future. (⟨⅟2, Set.invOf_mem_center (Set.ofNat_mem_center _ _)⟩ : Submonoid.center R) • { toFun := polarBilin map_add' := fun _x _y => LinearMap.ext₂ <| polar_add _ _ map_smul' := fun _c _x => LinearMap.ext₂ <| polar_smul _ _ } -#align quadratic_form.associated_hom QuadraticForm.associatedHom +#align quadratic_form.associated_hom QuadraticMap.associatedHom -variable (Q : QuadraticForm R M) +variable (Q : QuadraticMap R M N) @[simp] -theorem associated_apply (x y : M) : associatedHom S Q x y = ⅟ 2 * (Q (x + y) - Q x - Q y) := +theorem associated_apply (x y : M) : associatedHom S Q x y = ⅟ (2 : R) • (Q (x + y) - Q x - Q y) := rfl -#align quadratic_form.associated_apply QuadraticForm.associated_apply +#align quadratic_form.associated_apply QuadraticMap.associated_apply @[simp] theorem two_nsmul_associated : 2 • associatedHom S Q = Q.polarBilin := by ext dsimp - rw [← smul_mul_assoc, two_nsmul, invOf_two_add_invOf_two, one_mul, polar] + rw [← smul_assoc, two_nsmul, invOf_two_add_invOf_two, one_smul, polar] -theorem associated_isSymm : (associatedHom S Q).IsSymm := fun x y => by +theorem associated_isSymm (Q : QuadraticMap R M R) : (associatedHom S Q).IsSymm := fun x y => by simp only [associated_apply, sub_eq_add_neg, add_assoc, map_mul, RingHom.id_apply, map_add, _root_.map_neg, add_comm, add_left_comm] -#align quadratic_form.associated_is_symm QuadraticForm.associated_isSymm +#align quadratic_form.associated_is_symm QuadraticMap.associated_isSymm + @[simp] -theorem associated_comp [AddCommGroup N] [Module R N] (f : N →ₗ[R] M) : +theorem associated_comp {N' : Type*} [AddCommGroup N'] [Module R N'] (f : N' →ₗ[R] M) : associatedHom S (Q.comp f) = (associatedHom S Q).compl₁₂ f f := by ext simp only [associated_apply, comp_apply, map_add, LinearMap.compl₁₂_apply] -#align quadratic_form.associated_comp QuadraticForm.associated_comp +#align quadratic_form.associated_comp QuadraticMap.associated_comp -theorem associated_toQuadraticForm (B : BilinForm R M) (x y : M) : - associatedHom S B.toQuadraticForm x y = ⅟ 2 * (B x y + B y x) := by - simp only [associated_apply, toQuadraticForm_apply, map_add, add_apply, ← polar_toQuadraticForm, - polar.eq_1] -#align quadratic_form.associated_to_quadratic_form QuadraticForm.associated_toQuadraticForm +theorem associated_toQuadraticMap (B : BilinMap R M R) (x y : M) : + associatedHom S B.toQuadraticMap x y = ⅟ (2 : R) • (B x y + B y x) := by + simp only [associated_apply, LinearMap.BilinMap.toQuadraticMap_apply, map_add, + LinearMap.add_apply, smul_eq_mul] + abel_nf +#align quadratic_form.associated_to_quadratic_form QuadraticMap.associated_toQuadraticMap -theorem associated_left_inverse (h : B₁.IsSymm) : associatedHom S B₁.toQuadraticForm = B₁ := +theorem associated_left_inverse (h : B₁.IsSymm) : associatedHom S B₁.toQuadraticMap = B₁ := LinearMap.ext₂ fun x y => by - rw [associated_toQuadraticForm, ← h.eq, RingHom.id_apply, ← two_mul, ← mul_assoc, - invOf_mul_self, one_mul] -#align quadratic_form.associated_left_inverse QuadraticForm.associated_left_inverse + rw [associated_toQuadraticMap, ← h.eq x y, RingHom.id_apply, ← two_mul, ← smul_mul_assoc, + smul_eq_mul, invOf_mul_self, one_mul] +#align quadratic_form.associated_left_inverse QuadraticMap.associated_left_inverse -- Porting note: moved from below to golf the next theorem theorem associated_eq_self_apply (x : M) : associatedHom S Q x x = Q x := by - rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, - add_mul, add_mul, one_mul, add_sub_cancel_right, add_sub_cancel_right, invOf_mul_self_assoc] -#align quadratic_form.associated_eq_self_apply QuadraticForm.associated_eq_self_apply + rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul, + add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R, + ← smul_assoc] + simp only [smul_eq_mul, invOf_mul_self', one_smul] +#align quadratic_form.associated_eq_self_apply QuadraticMap.associated_eq_self_apply -theorem toQuadraticForm_associated : (associatedHom S Q).toQuadraticForm = Q := - QuadraticForm.ext <| associated_eq_self_apply S Q -#align quadratic_form.to_quadratic_form_associated QuadraticForm.toQuadraticForm_associated +theorem toQuadraticMap_associated : (associatedHom S Q).toQuadraticMap = Q := + QuadraticMap.ext <| associated_eq_self_apply S Q +#align quadratic_form.to_quadratic_form_associated QuadraticMap.toQuadraticMap_associated -- note: usually `rightInverse` lemmas are named the other way around, but this is consistent -- with historical naming in this file. theorem associated_rightInverse : - Function.RightInverse (associatedHom S) (toQuadraticForm : _ → QuadraticForm R M) := - fun Q => toQuadraticForm_associated S Q -#align quadratic_form.associated_right_inverse QuadraticForm.associated_rightInverse + Function.RightInverse (associatedHom S) (BilinMap.toQuadraticMap : _ → QuadraticMap R M R) := + fun Q => toQuadraticMap_associated S Q +#align quadratic_form.associated_right_inverse QuadraticMap.associated_rightInverse /-- `associated'` is the `ℤ`-linear map that sends a quadratic form on a module `M` over `R` to its associated symmetric bilinear form. -/ -abbrev associated' : QuadraticForm R M →ₗ[ℤ] BilinForm R M := +abbrev associated' : QuadraticMap R M R →ₗ[ℤ] BilinMap R M R := associatedHom ℤ -#align quadratic_form.associated' QuadraticForm.associated' +#align quadratic_form.associated' QuadraticMap.associated' /-- Symmetric bilinear forms can be lifted to quadratic forms -/ instance canLift : - CanLift (BilinForm R M) (QuadraticForm R M) (associatedHom ℕ) LinearMap.IsSymm where - prf B hB := ⟨B.toQuadraticForm, associated_left_inverse _ hB⟩ -#align quadratic_form.can_lift QuadraticForm.canLift + CanLift (BilinMap R M R) (QuadraticForm R M) (associatedHom ℕ) LinearMap.IsSymm where + prf B hB := ⟨B.toQuadraticMap, associated_left_inverse _ hB⟩ +#align quadratic_form.can_lift QuadraticMap.canLift /-- There exists a non-null vector with respect to any quadratic form `Q` whose associated bilinear form is non-zero, i.e. there exists `x` such that `Q x ≠ 0`. -/ @@ -899,27 +952,28 @@ theorem exists_quadraticForm_ne_zero {Q : QuadraticForm R M} rw [← not_forall] intro h apply hB₁ - rw [(QuadraticForm.ext h : Q = 0), LinearMap.map_zero] -#align quadratic_form.exists_quadratic_form_ne_zero QuadraticForm.exists_quadraticForm_ne_zero + rw [(QuadraticMap.ext h : Q = 0), LinearMap.map_zero] +#align quadratic_form.exists_quadratic_form_ne_zero QuadraticMap.exists_quadraticForm_ne_zero end AssociatedHom section Associated variable [CommSemiring S] [CommRing R] [AddCommGroup M] [Algebra S R] [Module R M] +variable [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower S R N] variable [Invertible (2 : R)] -- Note: When possible, rather than writing lemmas about `associated`, write a lemma applying to -- the more general `associatedHom` and place it in the previous section. -/-- `associated` is the linear map that sends a quadratic form over a commutative ring to its -associated symmetric bilinear form. -/ -abbrev associated : QuadraticForm R M →ₗ[R] BilinForm R M := +/-- `associated` is the linear map that sends a quadratic map over a commutative ring to its +associated symmetric bilinear map. -/ +abbrev associated : QuadraticMap R M N →ₗ[R] BilinMap R M N := associatedHom R -#align quadratic_form.associated QuadraticForm.associated +#align quadratic_form.associated QuadraticMap.associated variable (S) in theorem coe_associatedHom : - ⇑(associatedHom S : QuadraticForm R M →ₗ[S] BilinForm R M) = associated := + ⇑(associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) = associated := rfl open LinearMap in @@ -931,7 +985,7 @@ theorem associated_linMulLin (f g : M →ₗ[R] R) : simp only [associated_apply, linMulLin_apply, map_add, smul_add, LinearMap.add_apply, LinearMap.smul_apply, compl₁₂_apply, mul_apply', smul_eq_mul] ring_nf -#align quadratic_form.associated_lin_mul_lin QuadraticForm.associated_linMulLin +#align quadratic_form.associated_lin_mul_lin QuadraticMap.associated_linMulLin open LinearMap in @[simp] @@ -946,22 +1000,23 @@ section IsOrtho /-! ### Orthogonality -/ section CommSemiring -variable [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} +variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] + {Q : QuadraticMap R M N} -/-- The proposition that two elements of a quadratic form space are orthogonal. -/ -def IsOrtho (Q : QuadraticForm R M) (x y : M) : Prop := +/-- The proposition that two elements of a quadratic map space are orthogonal. -/ +def IsOrtho (Q : QuadraticMap R M N) (x y : M) : Prop := Q (x + y) = Q x + Q y -theorem isOrtho_def {Q : QuadraticForm R M} {x y : M} : Q.IsOrtho x y ↔ Q (x + y) = Q x + Q y := +theorem isOrtho_def {Q : QuadraticMap R M N} {x y : M} : Q.IsOrtho x y ↔ Q (x + y) = Q x + Q y := Iff.rfl -theorem IsOrtho.all (x y : M) : IsOrtho (0 : QuadraticForm R M) x y := (zero_add _).symm +theorem IsOrtho.all (x y : M) : IsOrtho (0 : QuadraticMap R M N) x y := (zero_add _).symm theorem IsOrtho.zero_left (x : M) : IsOrtho Q (0 : M) x := by simp [isOrtho_def] theorem IsOrtho.zero_right (x : M) : IsOrtho Q x (0 : M) := by simp [isOrtho_def] -theorem ne_zero_of_not_isOrtho_self {Q : QuadraticForm R M} (x : M) (hx₁ : ¬Q.IsOrtho x x) : +theorem ne_zero_of_not_isOrtho_self {Q : QuadraticMap R M N} (x : M) (hx₁ : ¬Q.IsOrtho x x) : x ≠ 0 := fun hx₂ => hx₁ (hx₂.symm ▸ .zero_left _) @@ -969,23 +1024,23 @@ theorem isOrtho_comm {x y : M} : IsOrtho Q x y ↔ IsOrtho Q y x := by simp_rw [ alias ⟨IsOrtho.symm, _⟩ := isOrtho_comm -theorem _root_.LinearMap.BilinForm.toQuadraticForm_isOrtho [IsCancelAdd R] - [NoZeroDivisors R] [CharZero R] {B : BilinForm R M} {x y : M} (h : B.IsSymm) : - B.toQuadraticForm.IsOrtho x y ↔ B.IsOrtho x y := by +theorem _root_.LinearMap.BilinForm.toQuadraticMap_isOrtho [IsCancelAdd R] + [NoZeroDivisors R] [CharZero R] {B : BilinMap R M R} {x y : M} (h : B.IsSymm) : + B.toQuadraticMap.IsOrtho x y ↔ B.IsOrtho x y := by letI : AddCancelMonoid R := { ‹IsCancelAdd R›, (inferInstanceAs <| AddCommMonoid R) with } - simp_rw [isOrtho_def, LinearMap.isOrtho_def, toQuadraticForm_apply, map_add, + simp_rw [isOrtho_def, LinearMap.isOrtho_def, B.toQuadraticMap_apply, map_add, LinearMap.add_apply, add_comm _ (B y y), add_add_add_comm _ _ (B y y), add_comm (B y y)] rw [add_right_eq_self (a := B x x + B y y), ← h, RingHom.id_apply, add_self_eq_zero] end CommSemiring section CommRing -variable [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} +variable [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] + {Q : QuadraticMap R M N} @[simp] theorem isOrtho_polarBilin {x y : M} : Q.polarBilin.IsOrtho x y ↔ IsOrtho Q x y := by - simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, - sub_eq_zero] + simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero] theorem IsOrtho.polar_eq_zero {x y : M} (h : IsOrtho Q x y) : polar Q x y = 0 := isOrtho_polarBilin.mpr h @@ -993,8 +1048,8 @@ theorem IsOrtho.polar_eq_zero {x y : M} (h : IsOrtho Q x y) : polar Q x y = 0 := @[simp] theorem associated_isOrtho [Invertible (2 : R)] {x y : M} : Q.associated.IsOrtho x y ↔ Q.IsOrtho x y := by - simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_mul_eq_iff_eq_mul_left, - mul_zero, sub_sub, sub_eq_zero] + simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff, + smul_zero, sub_sub, sub_eq_zero] end CommRing @@ -1004,22 +1059,22 @@ section Anisotropic section Semiring -variable [CommSemiring R] [AddCommMonoid M] [Module R M] +variable [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] -/-- An anisotropic quadratic form is zero only on zero vectors. -/ -def Anisotropic (Q : QuadraticForm R M) : Prop := +/-- An anisotropic quadratic map is zero only on zero vectors. -/ +def Anisotropic (Q : QuadraticMap R M N) : Prop := ∀ x, Q x = 0 → x = 0 -#align quadratic_form.anisotropic QuadraticForm.Anisotropic +#align quadratic_form.anisotropic QuadraticMap.Anisotropic -theorem not_anisotropic_iff_exists (Q : QuadraticForm R M) : +theorem not_anisotropic_iff_exists (Q : QuadraticMap R M N) : ¬Anisotropic Q ↔ ∃ x, x ≠ 0 ∧ Q x = 0 := by simp only [Anisotropic, not_forall, exists_prop, and_comm] -#align quadratic_form.not_anisotropic_iff_exists QuadraticForm.not_anisotropic_iff_exists +#align quadratic_form.not_anisotropic_iff_exists QuadraticMap.not_anisotropic_iff_exists -theorem Anisotropic.eq_zero_iff {Q : QuadraticForm R M} (h : Anisotropic Q) {x : M} : +theorem Anisotropic.eq_zero_iff {Q : QuadraticMap R M N} (h : Anisotropic Q) {x : M} : Q x = 0 ↔ x = 0 := ⟨h x, fun h => h.symm ▸ map_zero Q⟩ -#align quadratic_form.anisotropic.eq_zero_iff QuadraticForm.Anisotropic.eq_zero_iff +#align quadratic_form.anisotropic.eq_zero_iff QuadraticMap.Anisotropic.eq_zero_iff end Semiring @@ -1028,13 +1083,13 @@ section Ring variable [CommRing R] [AddCommGroup M] [Module R M] /-- The associated bilinear form of an anisotropic quadratic form is nondegenerate. -/ -theorem separatingLeft_of_anisotropic [Invertible (2 : R)] (Q : QuadraticForm R M) +theorem separatingLeft_of_anisotropic [Invertible (2 : R)] (Q : QuadraticMap R M R) (hB : Q.Anisotropic) : -- Porting note: added implicit argument - (QuadraticForm.associated' (R := R) Q).SeparatingLeft := fun x hx ↦ hB _ <| by + (QuadraticMap.associated' (R := R) Q).SeparatingLeft := fun x hx ↦ hB _ <| by rw [← hx x] exact (associated_eq_self_apply _ _ x).symm -#align quadratic_form.nondegenerate_of_anisotropic QuadraticForm.separatingLeft_of_anisotropic +#align quadratic_form.nondegenerate_of_anisotropic QuadraticMap.separatingLeft_of_anisotropic end Ring @@ -1042,52 +1097,56 @@ end Anisotropic section PosDef -variable {R₂ : Type u} [OrderedCommRing R₂] [AddCommMonoid M] [Module R₂ M] -variable {Q₂ : QuadraticForm R₂ M} +variable {R₂ : Type u} [CommSemiring R₂] [AddCommMonoid M] [Module R₂ M] +variable [PartialOrder N] [AddCommMonoid N] [Module R₂ N] [CovariantClass N N (· + ·) (· < ·)] +variable {Q₂ : QuadraticMap R₂ M N} /-- A positive definite quadratic form is positive on nonzero vectors. -/ -def PosDef (Q₂ : QuadraticForm R₂ M) : Prop := +def PosDef (Q₂ : QuadraticMap R₂ M N) : Prop := ∀ x, x ≠ 0 → 0 < Q₂ x -#align quadratic_form.pos_def QuadraticForm.PosDef +#align quadratic_form.pos_def QuadraticMap.PosDef + -theorem PosDef.smul {R} [LinearOrderedCommRing R] [Module R M] {Q : QuadraticForm R M} - (h : PosDef Q) {a : R} (a_pos : 0 < a) : PosDef (a • Q) := fun x hx => mul_pos a_pos (h x hx) -#align quadratic_form.pos_def.smul QuadraticForm.PosDef.smul +theorem PosDef.smul {R} [LinearOrderedCommRing R] [Module R M] [Module R N] [PosSMulStrictMono R N] + {Q : QuadraticMap R M N} (h : PosDef Q) {a : R} (a_pos : 0 < a) : PosDef (a • Q) := + fun x hx => smul_pos a_pos (h x hx) +#align quadratic_form.pos_def.smul QuadraticMap.PosDef.smul variable {n : Type*} -theorem PosDef.nonneg {Q : QuadraticForm R₂ M} (hQ : PosDef Q) (x : M) : 0 ≤ Q x := +theorem PosDef.nonneg {Q : QuadraticMap R₂ M N} (hQ : PosDef Q) (x : M) : 0 ≤ Q x := (eq_or_ne x 0).elim (fun h => h.symm ▸ (map_zero Q).symm.le) fun h => (hQ _ h).le -#align quadratic_form.pos_def.nonneg QuadraticForm.PosDef.nonneg +#align quadratic_form.pos_def.nonneg QuadraticMap.PosDef.nonneg -theorem PosDef.anisotropic {Q : QuadraticForm R₂ M} (hQ : Q.PosDef) : Q.Anisotropic := fun x hQx => - by_contradiction fun hx => - lt_irrefl (0 : R₂) <| by +theorem PosDef.anisotropic {Q : QuadraticMap R₂ M N} (hQ : Q.PosDef) : Q.Anisotropic := + fun x hQx => by_contradiction fun hx => + lt_irrefl (0 : N) <| by have := hQ _ hx rw [hQx] at this exact this -#align quadratic_form.pos_def.anisotropic QuadraticForm.PosDef.anisotropic +#align quadratic_form.pos_def.anisotropic QuadraticMap.PosDef.anisotropic -theorem posDef_of_nonneg {Q : QuadraticForm R₂ M} (h : ∀ x, 0 ≤ Q x) (h0 : Q.Anisotropic) : +theorem posDef_of_nonneg {Q : QuadraticMap R₂ M N} (h : ∀ x, 0 ≤ Q x) (h0 : Q.Anisotropic) : PosDef Q := fun x hx => lt_of_le_of_ne (h x) (Ne.symm fun hQx => hx <| h0 _ hQx) -#align quadratic_form.pos_def_of_nonneg QuadraticForm.posDef_of_nonneg +#align quadratic_form.pos_def_of_nonneg QuadraticMap.posDef_of_nonneg -theorem posDef_iff_nonneg {Q : QuadraticForm R₂ M} : PosDef Q ↔ (∀ x, 0 ≤ Q x) ∧ Q.Anisotropic := +theorem posDef_iff_nonneg {Q : QuadraticMap R₂ M N} : PosDef Q ↔ (∀ x, 0 ≤ Q x) ∧ Q.Anisotropic := ⟨fun h => ⟨h.nonneg, h.anisotropic⟩, fun ⟨n, a⟩ => posDef_of_nonneg n a⟩ -#align quadratic_form.pos_def_iff_nonneg QuadraticForm.posDef_iff_nonneg +#align quadratic_form.pos_def_iff_nonneg QuadraticMap.posDef_iff_nonneg -theorem PosDef.add (Q Q' : QuadraticForm R₂ M) (hQ : PosDef Q) (hQ' : PosDef Q') : +theorem PosDef.add (Q Q' : QuadraticMap R₂ M N) (hQ : PosDef Q) (hQ' : PosDef Q') : PosDef (Q + Q') := fun x hx => add_pos (hQ x hx) (hQ' x hx) -#align quadratic_form.pos_def.add QuadraticForm.PosDef.add +#align quadratic_form.pos_def.add QuadraticMap.PosDef.add -theorem linMulLinSelfPosDef {R} [LinearOrderedCommRing R] [Module R M] (f : M →ₗ[R] R) - (hf : LinearMap.ker f = ⊥) : PosDef (linMulLin f f) := fun _x hx => - mul_self_pos.2 fun h => hx <| LinearMap.ker_eq_bot'.mp hf _ h -#align quadratic_form.lin_mul_lin_self_pos_def QuadraticForm.linMulLinSelfPosDef +theorem linMulLinSelfPosDef {R} [LinearOrderedCommRing R] [Module R M] [LinearOrderedSemiring A] + [ExistsAddOfLE A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A) + (hf : LinearMap.ker f = ⊥) : PosDef (linMulLin (A := A) f f) := + fun _x hx => mul_self_pos.2 fun h => hx <| LinearMap.ker_eq_bot'.mp hf _ h +#align quadratic_form.lin_mul_lin_self_pos_def QuadraticMap.linMulLinSelfPosDef end PosDef -end QuadraticForm +end QuadraticMap section @@ -1103,34 +1162,34 @@ The determinant of the matrix is the discriminant of the quadratic form. variable {n : Type w} [Fintype n] [DecidableEq n] variable [CommRing R] [AddCommMonoid M] [Module R M] -/-- `M.toQuadraticForm'` is the map `fun x ↦ col x * M * row x` as a quadratic form. -/ -def Matrix.toQuadraticForm' (M : Matrix n n R) : QuadraticForm R (n → R) := - LinearMap.BilinForm.toQuadraticForm (Matrix.toLinearMap₂' M) -#align matrix.to_quadratic_form' Matrix.toQuadraticForm' +/-- `M.toQuadraticMap'` is the map `fun x ↦ row x * M * col x` as a quadratic form. -/ +def Matrix.toQuadraticMap' (M : Matrix n n R) : QuadraticMap R (n → R) R := + LinearMap.BilinMap.toQuadraticMap (Matrix.toLinearMap₂' M) +#align matrix.to_quadratic_form' Matrix.toQuadraticMap' variable [Invertible (2 : R)] /-- A matrix representation of the quadratic form. -/ -def QuadraticForm.toMatrix' (Q : QuadraticForm R (n → R)) : Matrix n n R := +def QuadraticMap.toMatrix' (Q : QuadraticMap R (n → R) R) : Matrix n n R := LinearMap.toMatrix₂' (associated (R := R) Q) -#align quadratic_form.to_matrix' QuadraticForm.toMatrix' +#align quadratic_form.to_matrix' QuadraticMap.toMatrix' -open QuadraticForm +open QuadraticMap -theorem QuadraticForm.toMatrix'_smul (a : R) (Q : QuadraticForm R (n → R)) : +theorem QuadraticMap.toMatrix'_smul (a : R) (Q : QuadraticMap R (n → R) R) : (a • Q).toMatrix' = a • Q.toMatrix' := by simp only [toMatrix', LinearEquiv.map_smul, LinearMap.map_smul] -#align quadratic_form.to_matrix'_smul QuadraticForm.toMatrix'_smul +#align quadratic_form.to_matrix'_smul QuadraticMap.toMatrix'_smul -theorem QuadraticForm.isSymm_toMatrix' (Q : QuadraticForm R (n → R)) : Q.toMatrix'.IsSymm := by +theorem QuadraticMap.isSymm_toMatrix' (Q : QuadraticMap R (n → R) R) : Q.toMatrix'.IsSymm := by ext i j rw [toMatrix', Matrix.transpose_apply, LinearMap.toMatrix₂'_apply, LinearMap.toMatrix₂'_apply, ← associated_isSymm, RingHom.id_apply, associated_apply] -#align quadratic_form.is_symm_to_matrix' QuadraticForm.isSymm_toMatrix' +#align quadratic_form.is_symm_to_matrix' QuadraticMap.isSymm_toMatrix' end -namespace QuadraticForm +namespace QuadraticMap variable {n : Type w} [Fintype n] variable [CommRing R] [DecidableEq n] [Invertible (2 : R)] @@ -1139,44 +1198,46 @@ variable {m : Type w} [DecidableEq m] [Fintype m] open Matrix @[simp] -theorem toMatrix'_comp (Q : QuadraticForm R (m → R)) (f : (n → R) →ₗ[R] m → R) : +theorem toMatrix'_comp (Q : QuadraticMap R (m → R) R) (f : (n → R) →ₗ[R] m → R) : (Q.comp f).toMatrix' = (LinearMap.toMatrix' f)ᵀ * Q.toMatrix' * (LinearMap.toMatrix' f) := by ext - simp only [QuadraticForm.associated_comp, LinearMap.toMatrix₂'_compl₁₂, toMatrix'] + simp only [QuadraticMap.associated_comp, LinearMap.toMatrix₂'_compl₁₂, toMatrix'] -#align quadratic_form.to_matrix'_comp QuadraticForm.toMatrix'_comp +#align quadratic_form.to_matrix'_comp QuadraticMap.toMatrix'_comp section Discriminant -variable {Q : QuadraticForm R (n → R)} +variable {Q : QuadraticMap R (n → R) R} /-- The discriminant of a quadratic form generalizes the discriminant of a quadratic polynomial. -/ -def discr (Q : QuadraticForm R (n → R)) : R := +def discr (Q : QuadraticMap R (n → R) R) : R := Q.toMatrix'.det -#align quadratic_form.discr QuadraticForm.discr +#align quadratic_form.discr QuadraticMap.discr theorem discr_smul (a : R) : (a • Q).discr = a ^ Fintype.card n * Q.discr := by simp only [discr, toMatrix'_smul, Matrix.det_smul] -#align quadratic_form.discr_smul QuadraticForm.discr_smul +#align quadratic_form.discr_smul QuadraticMap.discr_smul theorem discr_comp (f : (n → R) →ₗ[R] n → R) : (Q.comp f).discr = f.toMatrix'.det * f.toMatrix'.det * Q.discr := by - simp only [Matrix.det_transpose, mul_left_comm, QuadraticForm.toMatrix'_comp, mul_comm, + simp only [Matrix.det_transpose, mul_left_comm, QuadraticMap.toMatrix'_comp, mul_comm, Matrix.det_mul, discr] -#align quadratic_form.discr_comp QuadraticForm.discr_comp +#align quadratic_form.discr_comp QuadraticMap.discr_comp end Discriminant -end QuadraticForm +end QuadraticMap -namespace QuadraticForm +namespace QuadraticMap -end QuadraticForm +end QuadraticMap namespace LinearMap namespace BilinForm +open LinearMap (BilinMap) + section Semiring variable [CommSemiring R] [AddCommMonoid M] [Module R M] @@ -1184,7 +1245,7 @@ variable [CommSemiring R] [AddCommMonoid M] [Module R M] /-- A bilinear form is separating left if the quadratic form it is associated with is anisotropic. -/ -theorem separatingLeft_of_anisotropic {B : BilinForm R M} (hB : B.toQuadraticForm.Anisotropic) : +theorem separatingLeft_of_anisotropic {B : BilinForm R M} (hB : B.toQuadraticMap.Anisotropic) : B.SeparatingLeft := fun x hx => hB _ (hx x) #align bilin_form.nondegenerate_of_anisotropic LinearMap.BilinForm.separatingLeft_of_anisotropic @@ -1198,7 +1259,7 @@ on a module `M` over a ring `R` with invertible `2`, i.e. there exists some theorem exists_bilinForm_self_ne_zero [htwo : Invertible (2 : R)] {B : BilinForm R M} (hB₁ : B ≠ 0) (hB₂ : B.IsSymm) : ∃ x, ¬B.IsOrtho x x := by lift B to QuadraticForm R M using hB₂ with Q - obtain ⟨x, hx⟩ := QuadraticForm.exists_quadraticForm_ne_zero hB₁ + obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticForm_ne_zero hB₁ exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩ #align bilin_form.exists_bilin_form_self_ne_zero LinearMap.BilinForm.exists_bilinForm_self_ne_zero @@ -1209,8 +1270,8 @@ variable [FiniteDimensional K V] /-- Given a symmetric bilinear form `B` on some vector space `V` over a field `K` in which `2` is invertible, there exists an orthogonal basis with respect to `B`. -/ -theorem exists_orthogonal_basis [hK : Invertible (2 : K)] {B : BilinForm K V} (hB₂ : B.IsSymm) : - ∃ v : Basis (Fin (finrank K V)) K V, B.IsOrthoᵢ v := by +theorem exists_orthogonal_basis [hK : Invertible (2 : K)] {B : LinearMap.BilinForm K V} + (hB₂ : B.IsSymm) : ∃ v : Basis (Fin (finrank K V)) K V, B.IsOrthoᵢ v := by induction' hd : finrank K V with d ih generalizing V · exact ⟨basisOfFinrankZero hd, fun _ _ _ => map_zero _⟩ haveI := finrank_pos_iff.1 (hd.symm ▸ Nat.succ_pos d : 0 < finrank K V) @@ -1258,25 +1319,25 @@ end BilinForm end LinearMap -namespace QuadraticForm +namespace QuadraticMap open Finset -variable [CommSemiring R] [AddCommMonoid M] [Module R M] +variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] variable {ι : Type*} -/-- Given a quadratic form `Q` and a basis, `basisRepr` is the basis representation of `Q`. -/ -noncomputable def basisRepr [Finite ι] (Q : QuadraticForm R M) (v : Basis ι R M) : - QuadraticForm R (ι → R) := +/-- Given a quadratic map `Q` and a basis, `basisRepr` is the basis representation of `Q`. -/ +noncomputable def basisRepr [Finite ι] (Q : QuadraticMap R M N) (v : Basis ι R M) : + QuadraticMap R (ι → R) N := Q.comp v.equivFun.symm -#align quadratic_form.basis_repr QuadraticForm.basisRepr +#align quadratic_form.basis_repr QuadraticMap.basisRepr @[simp] -theorem basisRepr_apply [Fintype ι] {v : Basis ι R M} (Q : QuadraticForm R M) (w : ι → R) : +theorem basisRepr_apply [Fintype ι] {v : Basis ι R M} (Q : QuadraticMap R M N) (w : ι → R) : Q.basisRepr v w = Q (∑ i : ι, w i • v i) := by rw [← v.equivFun_symm_apply] rfl -#align quadratic_form.basis_repr_apply QuadraticForm.basisRepr_apply +#align quadratic_form.basis_repr_apply QuadraticMap.basisRepr_apply variable [Fintype ι] {v : Basis ι R M} @@ -1289,9 +1350,9 @@ variable (R) The weights are applied using `•`; typically this definition is used either with `S = R` or `[Algebra S R]`, although this is stated more generally. -/ def weightedSumSquares [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) : - QuadraticForm R (ι → R) := - ∑ i : ι, w i • proj i i -#align quadratic_form.weighted_sum_squares QuadraticForm.weightedSumSquares + QuadraticMap R (ι → R) R := + ∑ i : ι, w i • (proj (R := R) (n := ι) i i) +#align quadratic_form.weighted_sum_squares QuadraticMap.weightedSumSquares end @@ -1299,12 +1360,12 @@ end theorem weightedSumSquares_apply [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) (v : ι → R) : weightedSumSquares R w v = ∑ i : ι, w i • (v i * v i) := - QuadraticForm.sum_apply _ _ _ -#align quadratic_form.weighted_sum_squares_apply QuadraticForm.weightedSumSquares_apply + QuadraticMap.sum_apply _ _ _ +#align quadratic_form.weighted_sum_squares_apply QuadraticMap.weightedSumSquares_apply /-- On an orthogonal basis, the basis representation of `Q` is just a sum of squares. -/ theorem basisRepr_eq_of_iIsOrtho {R M} [CommRing R] [AddCommGroup M] [Module R M] - [Invertible (2 : R)] (Q : QuadraticForm R M) (v : Basis ι R M) + [Invertible (2 : R)] (Q : QuadraticMap R M R) (v : Basis ι R M) (hv₂ : (associated (R := R) Q).IsOrthoᵢ v) : Q.basisRepr v = weightedSumSquares _ fun i => Q (v i) := by ext w @@ -1312,13 +1373,13 @@ theorem basisRepr_eq_of_iIsOrtho {R M} [CommRing R] [AddCommGroup M] [Module R M refine sum_congr rfl fun j hj => ?_ rw [← @associated_eq_self_apply R, LinearMap.map_sum₂, sum_eq_single_of_mem j hj] · rw [LinearMap.map_smul, LinearMap.map_smul₂, smul_eq_mul, associated_apply, smul_eq_mul, - smul_eq_mul] - ring + smul_eq_mul, smul_eq_mul] + ring_nf · intro i _ hij rw [LinearMap.map_smul, LinearMap.map_smul₂, show associatedHom R Q (v i) (v j) = 0 from hv₂ hij, smul_eq_mul, smul_eq_mul, mul_zero, mul_zero] set_option linter.uppercaseLean3 false in -#align quadratic_form.basis_repr_eq_of_is_Ortho QuadraticForm.basisRepr_eq_of_iIsOrtho +#align quadratic_form.basis_repr_eq_of_is_Ortho QuadraticMap.basisRepr_eq_of_iIsOrtho -end QuadraticForm +end QuadraticMap diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean index c05c09d93c97e0..6a9105353b0d69 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean @@ -21,6 +21,8 @@ namespace QuadraticForm open Finset +open QuadraticMap + variable {ι : Type*} [Fintype ι] /-- The isometry between a weighted sum of squares on the complex numbers and the @@ -32,7 +34,7 @@ noncomputable def isometryEquivSumSquares (w' : ι → ℂ) : 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').isometryEquivBasisRepr + convert QuadraticForm.isometryEquivBasisRepr (weightedSumSquares ℂ w') ((Pi.basisFun ℂ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hw' i).unit) ext1 v erw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply] diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean b/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean index 414f09c76b831b..52e963a00b72f7 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean @@ -78,6 +78,8 @@ end LinearMap namespace QuadraticForm +open QuadraticMap + section Semiring variable [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] @@ -89,7 +91,7 @@ def dualProd : QuadraticForm R (Module.Dual R M × M) where toFun_smul a p := by dsimp only -- Porting note: added rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, LinearMap.map_smul, smul_eq_mul, - smul_eq_mul, mul_assoc] + smul_eq_mul, smul_eq_mul, mul_assoc] exists_companion' := ⟨LinearMap.dualProd R M, fun p q => by dsimp only -- Porting note: added @@ -100,7 +102,7 @@ def dualProd : QuadraticForm R (Module.Dual R M × M) where @[simp] theorem _root_.LinearMap.dualProd.toQuadraticForm : - (LinearMap.dualProd R M).toQuadraticForm = 2 • dualProd R M := + (LinearMap.dualProd R M).toQuadraticMap = 2 • dualProd R M := ext fun _a => (two_nsmul _).symm #align bilin_form.dual_prod.to_quadratic_form LinearMap.dualProd.toQuadraticForm diff --git a/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean b/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean index d8413097262b6a..894a451f9100b0 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean @@ -25,6 +25,8 @@ import Mathlib.LinearAlgebra.QuadraticForm.Isometry variable {ι R K M M₁ M₂ M₃ V : Type*} +open QuadraticMap + namespace QuadraticForm variable [CommSemiring R] diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean index e52834ea45563d..0121f397adbe0d 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean @@ -39,6 +39,8 @@ variable {ι : Type*} {R : Type*} {M₁ M₂ N₁ N₂ : Type*} {Mᵢ Nᵢ : ι namespace QuadraticForm +open QuadraticMap + section Prod section Semiring @@ -188,7 +190,8 @@ theorem IsOrtho.prod {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} @[simp] theorem IsOrtho.inl_inr {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (m₁ : M₁) (m₂ : M₂) : - (Q₁.prod Q₂).IsOrtho (m₁, 0) (0, m₂) := .prod (.zero_right _) (.zero_left _) + (Q₁.prod Q₂).IsOrtho (m₁, 0) (0, m₂) := + QuadraticForm.IsOrtho.prod (.zero_right _) (.zero_left _) @[simp] theorem IsOrtho.inr_inl {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (m₁ : M₁) (m₂ : M₂) : diff --git a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean index d149729c84060f..0a4c42c63fd3ca 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean @@ -35,6 +35,7 @@ variable {R : Type u} [CommRing R] [Invertible (2 : R)] namespace QuadraticModuleCat +open QuadraticMap open QuadraticForm namespace instMonoidalCategory diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Real.lean b/Mathlib/LinearAlgebra/QuadraticForm/Real.lean index cb09ccd2242f39..21714c6f12e31c 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Real.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Real.lean @@ -28,6 +28,8 @@ namespace QuadraticForm open Finset SignType +open QuadraticMap + variable {ι : Type*} [Fintype ι] /-- The isometry between a weighted sum of squares with weights `u` on the @@ -41,7 +43,7 @@ noncomputable def isometryEquivSignWeightedSumSquares (w : ι → ℝ) : by positivity have hwu : ∀ i, w i / |(u i : ℝ)| = sign (w i) := fun i ↦ by by_cases hi : w i = 0 <;> field_simp [hi, u] - convert (weightedSumSquares ℝ w).isometryEquivBasisRepr + convert QuadraticForm.isometryEquivBasisRepr (weightedSumSquares ℝ w) ((Pi.basisFun ℝ ι).unitsSMul fun i => .mk0 _ (hu i)) ext1 v classical diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 6db36b5862630c..54a0bb985a977f 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -21,7 +21,9 @@ universe uR uA uM₁ uM₂ variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} open TensorProduct +open LinearMap (BilinMap) open LinearMap (BilinForm) +open QuadraticMap namespace QuadraticForm @@ -44,11 +46,11 @@ noncomputable def tensorDistrib : letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm -- while `letI`s would produce a better term than `let`, they would make this already-slow -- definition even slower. - let toQ := BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) - let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) + let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) + let tmulB := BilinMap.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) let toB := AlgebraTensorModule.map - (QuadraticForm.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) - (QuadraticForm.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) + (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) + (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) toQ ∘ₗ tmulB ∘ₗ toB -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for @@ -57,7 +59,7 @@ noncomputable def tensorDistrib : theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) : tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₂ m₂ • Q₁ m₁ := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm - (BilinForm.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _ + (BilinMap.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _ (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ @@ -69,14 +71,14 @@ protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : Quadra theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : associated (R := A) (Q₁.tmul Q₂) = (associated (R := A) Q₁).tmul (associated (R := R) Q₂) := by - rw [QuadraticForm.tmul, tensorDistrib, BilinForm.tmul] + rw [QuadraticForm.tmul, tensorDistrib, BilinMap.tmul] dsimp have : Subsingleton (Invertible (2 : A)) := inferInstance convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • (polarBilin Q₁).tmul (polarBilin Q₂) := by - simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinForm.tmul, tmul_smul, + simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinMap.tmul, tmul_smul, ← smul_tmul', map_nsmul, associated_tmul] rw [smul_comm (_ : A) (_ : ℕ), ← smul_assoc, two_smul _ (_ : A), invOf_two_add_invOf_two, one_smul] @@ -85,7 +87,7 @@ variable (A) in /-- The base change of a quadratic form. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 protected noncomputable def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := - QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq (R := A)) Q + QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticMap.sq (R := A)) Q @[simp] theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : @@ -95,12 +97,12 @@ theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : associated (R := A) (Q.baseChange A) = (associated (R := R) Q).baseChange A := by dsimp only [QuadraticForm.baseChange, LinearMap.baseChange] - rw [associated_tmul (QuadraticForm.sq (R := A)) Q, associated_sq] + rw [associated_tmul (QuadraticMap.sq (R := A)) Q, associated_sq] exact rfl theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : polarBilin (Q.baseChange A) = (polarBilin Q).baseChange A := by - rw [QuadraticForm.baseChange, BilinForm.baseChange, polarBilin_tmul, BilinForm.tmul, + rw [QuadraticForm.baseChange, BilinMap.baseChange, polarBilin_tmul, BilinMap.tmul, ← LinearMap.map_smul, smul_tmul', ← two_nsmul_associated R, coe_associatedHom, associated_sq, smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul] @@ -114,7 +116,7 @@ theorem baseChange_ext ⦃Q₁ Q₂ : QuadraticForm A (A ⊗[R] M₂)⦄ (h : ∀ m, Q₁ (1 ⊗ₜ m) = Q₂ (1 ⊗ₜ m)) : Q₁ = Q₂ := by replace h (a m) : Q₁ (a ⊗ₜ m) = Q₂ (a ⊗ₜ m) := by - rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', map_smul, map_smul, h] + rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h] ext x induction x with | tmul => simp [h] diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean index fb1a6f21270f64..ac6eb938e2b5b0 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean @@ -27,6 +27,8 @@ variable {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM open scoped TensorProduct +open QuadraticMap + namespace QuadraticForm variable [CommRing R] @@ -39,9 +41,9 @@ theorem tmul_comp_tensorMap {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) : (Q₂.tmul Q₄).comp (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃ := by - have h₁ : Q₁ = Q₂.comp f.toLinearMap := QuadraticForm.ext fun x => (f.map_app x).symm - have h₃ : Q₃ = Q₄.comp g.toLinearMap := QuadraticForm.ext fun x => (g.map_app x).symm - refine (QuadraticForm.associated_rightInverse R).injective ?_ + have h₁ : Q₁ = Q₂.comp f.toLinearMap := QuadraticMap.ext fun x => (f.map_app x).symm + have h₃ : Q₃ = Q₄.comp g.toLinearMap := QuadraticMap.ext fun x => (g.map_app x).symm + refine (QuadraticMap.associated_rightInverse R).injective ?_ ext m₁ m₃ m₁' m₃' simp [-associated_apply, h₁, h₃, associated_tmul] @@ -78,10 +80,10 @@ section tensorComm @[simp] theorem tmul_comp_tensorComm (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : (Q₂.tmul Q₁).comp (TensorProduct.comm R M₁ M₂) = Q₁.tmul Q₂ := by - refine (QuadraticForm.associated_rightInverse R).injective ?_ + refine (QuadraticMap.associated_rightInverse R).injective ?_ ext m₁ m₂ m₁' m₂' dsimp [-associated_apply] - simp only [associated_tmul, QuadraticForm.associated_comp] + simp only [associated_tmul, QuadraticMap.associated_comp] exact mul_comm _ _ @[simp] @@ -114,10 +116,10 @@ section tensorAssoc theorem tmul_comp_tensorAssoc (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) : (Q₁.tmul (Q₂.tmul Q₃)).comp (TensorProduct.assoc R M₁ M₂ M₃) = (Q₁.tmul Q₂).tmul Q₃ := by - refine (QuadraticForm.associated_rightInverse R).injective ?_ + refine (QuadraticMap.associated_rightInverse R).injective ?_ ext m₁ m₂ m₁' m₂' m₁'' m₂'' dsimp [-associated_apply] - simp only [associated_tmul, QuadraticForm.associated_comp] + simp only [associated_tmul, QuadraticMap.associated_comp] exact mul_assoc _ _ _ @[simp] @@ -152,10 +154,10 @@ section tensorRId theorem comp_tensorRId_eq (Q₁ : QuadraticForm R M₁) : Q₁.comp (TensorProduct.rid R M₁) = Q₁.tmul (sq (R := R)) := by - refine (QuadraticForm.associated_rightInverse R).injective ?_ + refine (QuadraticMap.associated_rightInverse R).injective ?_ ext m₁ m₁' dsimp [-associated_apply] - simp only [associated_tmul, QuadraticForm.associated_comp] + simp only [associated_tmul, QuadraticMap.associated_comp] simp [-associated_apply, one_mul] @[simp] @@ -184,23 +186,23 @@ end tensorRId section tensorLId theorem comp_tensorLId_eq (Q₂ : QuadraticForm R M₂) : - Q₂.comp (TensorProduct.lid R M₂) = (sq (R := R)).tmul Q₂ := by - refine (QuadraticForm.associated_rightInverse R).injective ?_ + Q₂.comp (TensorProduct.lid R M₂) = QuadraticForm.tmul (sq (R := R)) Q₂ := by + refine (QuadraticMap.associated_rightInverse R).injective ?_ ext m₂ m₂' dsimp [-associated_apply] - simp only [associated_tmul, QuadraticForm.associated_comp] + simp only [associated_tmul, QuadraticMap.associated_comp] simp [-associated_apply, mul_one] @[simp] theorem tmul_tensorLId_apply (Q₂ : QuadraticForm R M₂) (x : R ⊗[R] M₂) : - Q₂ (TensorProduct.lid R M₂ x) = (sq (R := R)).tmul Q₂ x := + Q₂ (TensorProduct.lid R M₂ x) = QuadraticForm.tmul (sq (R := R)) Q₂ x := DFunLike.congr_fun (comp_tensorLId_eq Q₂) x /-- `TensorProduct.lid` preserves tensor products of quadratic forms. -/ @[simps toLinearEquiv] def tensorLId (Q₂ : QuadraticForm R M₂) : - ((sq (R := R)).tmul Q₂).IsometryEquiv Q₂ where + (QuadraticForm.tmul (sq (R := R)) Q₂).IsometryEquiv Q₂ where toLinearEquiv := TensorProduct.lid R M₂ map_app' := tmul_tensorLId_apply Q₂ diff --git a/docs/overview.yaml b/docs/overview.yaml index b93a98c3dc113f..5d884c7e1cabb5 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -190,7 +190,7 @@ Linear algebra: symmetric bilinear form: 'LinearMap.BilinForm.IsSymm' matrix representation: 'BilinForm.toMatrix' quadratic form: 'QuadraticForm' - polar form of a quadratic: 'QuadraticForm.polar' + polar form of a quadratic: 'QuadraticMap.polar' Finite-dimensional inner product spaces (see also Hilbert spaces, below): existence of orthonormal basis: 'OrthonormalBasis' diagonalization of self-adjoint endomorphisms: 'LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply' diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml index e174f56799d6c3..21619980559e52 100644 --- a/docs/undergrad.yaml +++ b/docs/undergrad.yaml @@ -202,7 +202,7 @@ Bilinear and Quadratic Forms Over a Vector Space: rank of a bilinear form: '' Quadratic forms: quadratic form: 'QuadraticForm' - polar form of a quadratic: 'QuadraticForm.polar' + polar form of a quadratic: 'QuadraticMap.polar' Orthogonality: orthogonal elements: 'LinearMap.BilinForm.IsOrtho' adjoint endomorphism: 'LinearMap.BilinForm.leftAdjointOfNondegenerate' diff --git a/scripts/nolints.json b/scripts/nolints.json index a1ac7f7736fa46..0f394683593a3c 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -335,7 +335,7 @@ ["docBlame", "QPF.P"], ["docBlame", "QPF.abs"], ["docBlame", "QPF.repr"], - ["docBlame", "QuadraticForm.toFun"], + ["docBlame", "QuadraticMap.toFun"], ["docBlame", "Quaternion.«termℍ[_]»"], ["docBlame", "QuaternionAlgebra.imI"], ["docBlame", "QuaternionAlgebra.imJ"], diff --git a/test/TCSynth.lean b/test/TCSynth.lean index 417ce1dd503f82..8e32f2f8c1cf70 100644 --- a/test/TCSynth.lean +++ b/test/TCSynth.lean @@ -42,7 +42,6 @@ section /-- info: NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring -/ #guard_msgs in -set_option synthInstance.maxHeartbeats 6000 in variable {A : Type} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [CstarRing A] [StarModule ℂ A] (x : A) in #synth NonUnitalNonAssocSemiring (elementalStarAlgebra ℂ x)