Documentation

Counterexamples.QuadraticForm

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
Instances For
    @[simp]
    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.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.