# Quadratic form structures related to module.dual#

## Main definitions #

• bilin_form.dual_prod R M, the bilinear form on (f, x) : module.dual R M × M defined as f x.
• quadratic_form.dual_prod R M, the quadratic form on (f, x) : module.dual R M × M defined as f x.
• quadratic_form.to_dual_prod : M × M →ₗ[R] module.dual R M × M a form-preserving map from (Q.prod $-Q) to quadratic_form.dual_prod R M. Note that we do not have the morphism version of quadratic_form.isometry, so for now this is stated without full bundling. def bilin_form.dual_prod (R : Type u_1) (M : Type u_2) [ M] : M × M) The symmetric bilinear form on module.dual R M × M defined as B (f, x) (g, y) = f y + g x. Equations @[simp] theorem bilin_form.dual_prod_apply (R : Type u_1) (M : Type u_2) [ M] (x y : M × M) : M) x y = (y.fst) x.snd + (x.fst) y.snd theorem bilin_form.is_symm_dual_prod (R : Type u_1) (M : Type u_2) [ M] : theorem bilin_form.nondenerate_dual_prod (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] : def quadratic_form.dual_prod (R : Type u_1) (M : Type u_2) [ M] : M × M) The quadratic form on module.dual R M × M defined as Q (f, x) = f x. Equations @[simp] theorem quadratic_form.dual_prod_apply (R : Type u_1) (M : Type u_2) [ M] (p : M × M) : p = (p.fst) p.snd @[simp] theorem bilin_form.dual_prod.to_quadratic_form (R : Type u_1) (M : Type u_2) [ M] : def quadratic_form.dual_prod_isometry {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (f : M ≃ₗ[R] N) : Any module isomorphism induces a quadratic isomorphism between the corresponding dual_prod. Equations @[simp] theorem quadratic_form.dual_prod_isometry_to_linear_equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (f : M ≃ₗ[R] N) : def quadratic_form.dual_prod_prod_isometry {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] : (M × N)).isometry M).prod N)) quadratic_form.dual_prod commutes (isometrically) with quadratic_form.prod. Equations @[simp] theorem quadratic_form.to_dual_prod_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) [invertible 2] (i : M × M) : (Q.to_dual_prod) i = , i.fst - i.snd) def quadratic_form.to_dual_prod {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) [invertible 2] : M × M →ₗ[R] M × M The isometry sending (Q.prod$ -Q) to (quadratic_form.dual_prod R M).

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

Equations
theorem quadratic_form.to_dual_prod_isometry {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] [invertible 2] (Q : M) (x : M × M) :
((Q.to_dual_prod) x) = (Q.prod (-Q)) x