QuadraticForm R M and Subtype LinearMap.IsSymm are distinct notions in characteristic 2

The main result of this file is LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm.

The counterexample we use is $B (x, y) (x', y') ↦ xy' + x'y$ where x y x' y' : ZMod 2.

def Counterexample.B (F : Type u_1) [CommRing F] : LinearMap.BilinForm F (F × F)

The bilinear form we will use as a counterexample, over some field F of characteristic two.

Equations

• Counterexample.B F = (LinearMap.mul F F).compl₁₂ (LinearMap.fst F F F) (LinearMap.snd F F F) + (LinearMap.mul F F).compl₁₂ (LinearMap.snd F F F) (LinearMap.fst F F F)

@[simp]

theorem Counterexample.B_apply (F : Type u_1) [CommRing F] (x y : F × F) : ((Counterexample.B F) x) y = x.1 * y.2 + x.2 * y.1

theorem Counterexample.isSymm_B (F : Type u_1) [CommRing F] : LinearMap.IsSymm (Counterexample.B F)

theorem Counterexample.isAlt_B (F : Type u_1) [CommRing F] [CharP F 2] : LinearMap.IsAlt (Counterexample.B F)

theorem Counterexample.B_ne_zero (F : Type u_1) [CommRing F] [Nontrivial F] : Counterexample.B F ≠ 0

theorem Counterexample.LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm : ¬∀ {R M : Type u} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], Set.InjOn LinearMap.BilinMap.toQuadraticMap {B : LinearMap.BilinMap R M R | LinearMap.IsSymm B}

LinearMap.BilinForm.toQuadraticForm is not injective on symmetric bilinear forms.

This disproves a weaker version of QuadraticForm.associated_left_inverse.