Documentation

Counterexamples.QuadraticForm

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.

source
def Counterexample.B (F : Type u_1) [CommRing F] :
BilinForm F (F × F)

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

Instances For
    source
    @[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
    source
    theorem Counterexample.isSymm_B (F : Type u_1) [CommRing F] :
    BilinForm.IsSymm (Counterexample.B F)
    source
    theorem Counterexample.isAlt_B (F : Type u_1) [CommRing F] [CharP F 2] :
    BilinForm.IsAlt (Counterexample.B F)
    source
    theorem Counterexample.B_ne_zero (F : Type u_1) [Nontrivial F] [CommRing F] :
    Counterexample.B F ≠ 0
    source
    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.