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.
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)
Instances For
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
.