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.

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

Instances For
    theorem Counterexample.B_apply (F : Type u_1) [CommRing F] (x : F × F) (y : F × F) :
    ((Counterexample.B F) x) y = x.1 * y.2 + x.2 * y.1
    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.BilinForm.toQuadraticForm {B : LinearMap.BilinForm R M | LinearMap.IsSymm B}

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

    This disproves a weaker version of QuadraticForm.associated_left_inverse.