# Quadratic form structures related to Module.Dual#

## Main definitions #

• LinearMap.dualProd R M, the bilinear form on (f, x) : Module.Dual R M × M defined as f x.
• QuadraticForm.dualProd R M, the quadratic form on (f, x) : Module.Dual R M × M defined as f x.
• QuadraticForm.toDualProd : (Q.prod <| -Q) →qᵢ QuadraticForm.dualProd R M a form-preserving map from (Q.prod <| -Q) to QuadraticForm.dualProd R M.
@[simp]
theorem LinearMap.dualProd_apply_apply (R : Type u_1) (M : Type u_2) [] [] [Module R M] (a : × M) (a : × M) :
(() a✝) a = a.1 a✝.2 + a✝.1 a.2
def LinearMap.dualProd (R : Type u_1) (M : Type u_2) [] [] [Module R M] :

The symmetric bilinear form on Module.Dual R M × M defined as B (f, x) (g, y) = f y + g x.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem LinearMap.isSymm_dualProd (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
theorem LinearMap.separatingLeft_dualProd (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
@[simp]
theorem QuadraticForm.dualProd_apply (R : Type u_1) (M : Type u_2) [] [] [Module R M] (p : × M) :
() p = p.1 p.2
def QuadraticForm.dualProd (R : Type u_1) (M : Type u_2) [] [] [Module R M] :

The quadratic form on Module.Dual R M × M defined as Q (f, x) = f x.

Equations
• = { toFun := fun (p : × M) => p.1 p.2, toFun_smul := , exists_companion' := }
Instances For
@[simp]
theorem LinearMap.dualProd.toQuadraticForm (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
@[simp]
theorem QuadraticForm.dualProdIsometry_toFun {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] (f : M ≃ₗ[R] N) :
∀ (a : × M), = ((f.symm.dualMap).prodCongr f) a
@[simp]
theorem QuadraticForm.dualProdIsometry_invFun {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] (f : M ≃ₗ[R] N) :
∀ (a : × N), .invFun a = ((f.symm.dualMap).prodCongr f).symm a
def QuadraticForm.dualProdIsometry {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] (f : M ≃ₗ[R] N) :
().IsometryEquiv ()

Any module isomorphism induces a quadratic isomorphism between the corresponding dual_prod.

Equations
• = { toLinearEquiv := f.dualMap.symm.prod f, map_app' := }
Instances For
@[simp]
theorem QuadraticForm.dualProdProdIsometry_toFun {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] :
∀ (a : Module.Dual R (M × N) × M × N), QuadraticForm.dualProdProdIsometry a = ((a.1 ∘ₗ , a.2.1), a.1 ∘ₗ , a.2.2)
@[simp]
theorem QuadraticForm.dualProdProdIsometry_invFun {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] :
∀ (a : ( × M) × × N), QuadraticForm.dualProdProdIsometry.invFun a = (().symm.prod (LinearEquiv.refl R (M × N))).symm ((a.1.1, a.2.1), a.1.2, a.2.2)
def QuadraticForm.dualProdProdIsometry {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] :
(QuadraticForm.dualProd R (M × N)).IsometryEquiv (().prod ())

QuadraticForm.dualProd commutes (isometrically) with QuadraticForm.prod.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem QuadraticForm.toDualProd_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) [] (i : M × M) :
Q.toDualProd i = ((QuadraticForm.associated Q) i.1 + (QuadraticForm.associated Q) i.2, i.1 - i.2)
def QuadraticForm.toDualProd {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) [] :
Q.prod (-Q) →qᵢ

The isometry sending (Q.prod <| -Q) to (QuadraticForm.dualProd R M).

This is σ from Proposition 4.8, page 84 of [Hermitian K-Theory and Geometric Applications][hyman1973]; though we swap the order of the pairs.

Equations
• One or more equations did not get rendered due to their size.
Instances For

TODO: show that QuadraticForm.toDualProd is an QuadraticForm.IsometryEquiv