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.
Equations
- counterexample.B F = bilin_form.lin_mul_lin (linear_map.fst F F F) (linear_map.snd F F F) + bilin_form.lin_mul_lin (linear_map.snd F F F) (linear_map.fst F F F)
theorem
counterexample.B_ne_zero
(F : Type u_1)
[nontrivial F]
[comm_ring F]
[char_p F 2] :
counterexample.B F ≠ 0
theorem
counterexample.bilin_form.not_inj_on_to_quadratic_form_is_symm
:
¬∀ {R M : Type u} [_inst_4 : semiring R] [_inst_5 : add_comm_monoid M] [_inst_6 : module R M], set.inj_on bilin_form.to_quadratic_form {B : bilin_form R M | B.is_symm}
bilin_form.to_quadratic_form is not injective on symmetric bilinear forms.
This disproves a weaker version of quadratic_form.associated_left_inverse.