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.

def LinearMap.dualProd (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.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.

@[simp]

theorem LinearMap.dualProd_apply_apply (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (a a✝ : Module.Dual R M × M) : ((dualProd R M) a) a✝ = a✝.1 a.2 + a.1 a✝.2

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

theorem LinearMap.separatingLeft_dualProd (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : SeparatingLeft (dualProd R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)

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 QuadraticForm.dualProd_apply (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (p : Module.Dual R M × M) : (dualProd R M) p = p.1 p.2

@[simp]

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

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) : QuadraticMap.IsometryEquiv (dualProd R M) (dualProd R N)

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

@[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) : (dualProdIsometry f).invFun a✝ = (f.symm.dualMap.toAddEquiv.prodCongr f.toAddEquiv).symm 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) : (dualProdIsometry f) a✝ = (f.symm.dualMap.toAddEquiv.prodCongr f.toAddEquiv) 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] : QuadraticMap.IsometryEquiv (dualProd R (M × N)) (QuadraticMap.prod (dualProd R M) (dualProd R N))

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

@[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) : dualProdProdIsometry.invFun a✝ = ((Module.dualProdDualEquivDual R M N).symm.prodCongr (LinearEquiv.refl R (M × N))).symm ((a✝.1.1, a✝.2.1), a✝.1.2, a✝.2.2)

@[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) : dualProdProdIsometry a✝ = ((a✝.1 ∘ₗ LinearMap.inl R M N, a✝.2.1), a✝.1 ∘ₗ LinearMap.inr R M N, a✝.2.2)

def QuadraticForm.toDualProd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : QuadraticMap.prod Q (-Q) →qᵢ 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.

@[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) : Q.toDualProd i = ((QuadraticMap.associated Q) i.1 + (QuadraticMap.associated Q) i.2, i.1 - i.2)

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

theorem LinearMap.BilinForm.linearIndependent_of_pairwise_le_zero {ι : Type u_4} {R : Type u_5} {M : Type u_6} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hB : (BilinMap.toQuadraticMap B).PosDef) (f : Module.Dual R M) (v : ι → M) (hp : ∀ (i : ι), 0 < f (v i)) (hn : Pairwise fun (i j : ι) => (B (v i)) (v j) ≤ 0) : LinearIndependent R v

Vectors which subtend obtuse angles with each other and all lie in the same half-space are linearly independent.

This is [serre1965](Ch. V, §9, Lemma 4).