Quadratic form structures related to Module.Dual

Main definitions

• BilinForm.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 BilinForm.dualProd_apply (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : Module.Dual R M × M) (y : Module.Dual R M × M) : BilinForm.bilin (BilinForm.dualProd R M) x y = ↑y.fst x.snd + ↑x.fst y.snd

def BilinForm.dualProd (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : BilinForm R (Module.Dual R M × M)

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

theorem BilinForm.isSymm_dualProd (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : BilinForm.IsSymm (BilinForm.dualProd R M)

theorem BilinForm.nondenerate_dualProd (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : BilinForm.Nondegenerate (BilinForm.dualProd R M) ↔ Function.Injective ↑(Module.Dual.eval R M)

@[simp]

theorem QuadraticForm.dualProd_apply (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (p : Module.Dual R M × M) : ↑(QuadraticForm.dualProd R M) p = ↑p.fst p.snd

def QuadraticForm.dualProd (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : QuadraticForm R (Module.Dual R M × M)

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

@[simp]

theorem BilinForm.dualProd.toQuadraticForm (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : BilinForm.toQuadraticForm (BilinForm.dualProd R M) = 2 • QuadraticForm.dualProd R M

@[simp]

theorem QuadraticForm.dualProdIsometry_invFun {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] N) : ∀ (a : Module.Dual R N × N), LinearEquiv.invFun (QuadraticForm.dualProdIsometry f).toLinearEquiv a = ↑(AddEquiv.symm (AddEquiv.prodCongr ↑(LinearEquiv.dualMap (LinearEquiv.symm f)) ↑f)) a

@[simp]

theorem QuadraticForm.dualProdIsometry_toFun {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] N) : ∀ (a : Module.Dual R M × M), ↑(QuadraticForm.dualProdIsometry f) a = ↑(AddEquiv.prodCongr ↑(LinearEquiv.dualMap (LinearEquiv.symm f)) ↑f) a

def QuadraticForm.dualProdIsometry {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] N) : QuadraticForm.IsometryEquiv (QuadraticForm.dualProd R M) (QuadraticForm.dualProd R N)

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

@[simp]

theorem QuadraticForm.dualProdProdIsometry_toFun {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : ∀ (a : Module.Dual R (M × N) × M × N), ↑QuadraticForm.dualProdProdIsometry a = ((LinearMap.comp a.fst (LinearMap.inl R M N), a.snd.fst), LinearMap.comp a.fst (LinearMap.inr R M N), a.snd.snd)

@[simp]

theorem QuadraticForm.dualProdProdIsometry_invFun {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : ∀ (a : (Module.Dual R M × M) × Module.Dual R N × N), LinearEquiv.invFun QuadraticForm.dualProdProdIsometry.toLinearEquiv a = ↑↑(LinearEquiv.symm (LinearEquiv.prod (LinearEquiv.symm (Module.dualProdDualEquivDual R M N)) (LinearEquiv.refl R (M × N)))) (↑↑(LinearEquiv.prodProdProdComm R (Module.Dual R M) M (Module.Dual R N) N) a)

def QuadraticForm.dualProdProdIsometry {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : QuadraticForm.IsometryEquiv (QuadraticForm.dualProd R (M × N)) (QuadraticForm.prod (QuadraticForm.dualProd R M) (QuadraticForm.dualProd R N))

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

@[simp]

theorem QuadraticForm.toDualProd_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (i : M × M) : ↑(QuadraticForm.toDualProd Q) i = (↑(↑BilinForm.toLin (↑QuadraticForm.associated Q)) i.fst + ↑(↑BilinForm.toLin (↑QuadraticForm.associated Q)) i.snd, i.fst - i.snd)

def QuadraticForm.toDualProd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : QuadraticForm.prod Q (-Q) →qᵢ QuadraticForm.dualProd R M

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.

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