mathlib3 documentation

mathlib-counterexamples / quadratic_form

quadratic_form R M and subtype bilin_form.is_symm are distinct notions in characteristic 2 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The main result of this file is bilin_form.not_inj_on_to_quadratic_form_is_symm.

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) [nontrivial F] [comm_ring F] [char_p F 2] :
bilin_form F (F × F)

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

theorem counterexample.B_apply (F : Type u_1) [nontrivial F] [comm_ring F] [char_p F 2] (x y : F × F) :
(counterexample.B F) x y = x.fst * y.snd + x.snd * y.fst

bilin_form.to_quadratic_form is not injective on symmetric bilinear forms.

This disproves a weaker version of quadratic_form.associated_left_inverse.