A form that is both symmetric and alternating

Away from characteristic two a bilinear form cannot be both symmetric and alternating without being zero: symmetry and alternation give B x y = B y x and B x y = -B y x, so 2 * B x y = 0, and cancelling the 2 leaves B x y = 0.

That cancellation is all the hypothesis on the ring there is: 2 has to be regular, and nothing is asked of any other element, so the statement covers rings with zero divisors elsewhere. Over a field, or over any domain, IsRegular.of_ne_zero supplies the hypothesis from (2 : R) ≠ 0.

Main results

• TauCeti.BilinForm.eq_zero_of_isSymm_of_isAlt: a symmetric alternating form over a ring in which 2 is regular is zero.
• TauCeti.BilinForm.nondegenerate_smul_iff: scalar multiplication by a regular element preserves nondegeneracy.
• TauCeti.BilinForm.nondegenerate_neg_iff: negating a bilinear form preserves nondegeneracy.
• Module.Basis.dualBasis_smul_apply: the dual basis of a scalar multiple of a form.
• LinearMap.BilinForm.IsSymm.apply_add_self: polarization of a symmetric bilinear form.

theorem LinearMap.BilinForm.IsSymm.apply_add_self {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) (x y : M) : (B (x + y)) (x + y) = (B x) x + (B y) y + 2 * (B x) y

Polarization of a symmetric bilinear form over a commutative semiring.

theorem TauCeti.BilinForm.eq_zero_of_isSymm_of_isAlt {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (h2 : IsLeftRegular 2) {B : LinearMap.BilinForm R M} (hsymm : B.IsSymm) (halt : B.IsAlt) : B = 0

Away from characteristic two a symmetric alternating form is zero: symmetry and alternation force 2 * B x y = 0, and a regular 2 cancels.

@[simp]

theorem TauCeti.BilinForm.nondegenerate_smul_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {c : R} (hc : IsRegular c) : (c • B).Nondegenerate ↔ B.Nondegenerate

A scalar multiple of a bilinear form by a regular element is nondegenerate if and only if the original form is nondegenerate.

@[simp]

theorem TauCeti.BilinForm.nondegenerate_neg_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} : (-B).Nondegenerate ↔ B.Nondegenerate

Negating a bilinear form preserves nondegeneracy.

@[simp]

theorem Module.Basis.dualBasis_smul_apply {K : Type u_1} {V : Type u_2} {ι : Type u_3} [Field K] [AddCommGroup V] [Module K V] [Finite ι] [DecidableEq ι] (b : Basis ι K V) (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (c : K) (hc : c ≠ 0) (i : ι) : ((c • B).dualBasis ⋯ b) i = c⁻¹ • (B.dualBasis hB b) i

The basis dual to b for a nonzero scalar multiple c • B of a nondegenerate bilinear form is c⁻¹ times the basis dual to b for B.