QuadraticForm R M
and Subtype BilinForm.IsSymm
are distinct notions in characteristic 2 #
The main result of this file is 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
.
@[simp]
theorem
Counterexample.B_apply
(F : Type u_1)
[CommRing F]
(x : F × F)
(y : F × F)
:
BilinForm.bilin (Counterexample.B F) x y = x.fst * y.snd + x.snd * y.fst
theorem
Counterexample.BilinForm.not_injOn_toQuadraticForm_isSymm :
¬∀ {R M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Set.InjOn BilinForm.toQuadraticForm {B | BilinForm.IsSymm B}
BilinForm.toQuadraticForm
is not injective on symmetric bilinear forms.
This disproves a weaker version of QuadraticForm.associated_left_inverse
.