Documentation

Q2Presentation.Quadratic.Polarization

Polarizations of F₂ quadratic forms (checkpoint-F10 support) #

Every quadratic form q : QuadF2 V on a finite-dimensional F₂-space admits a (non-equivariant) polarization: a bilinear B with diagonal q and symmetrization the polar form. Construction: fix finBasis, set B(e_i,e_j) := polar(e_i,e_j) for i < j, q(e_i) for i = j, 0 for i > j. This eliminates the equivariant-refinement component of the leaf-#1 crux (PROGRESS.md, F10 finding): downstream consumes only the diagonal and the symmetrization of phi.

source
theorem Q2Presentation.Quadratic.QuadF2.polar_self_eq_zero {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (x : V) :
(q.polar x) x = 0

Char-2: the polar form vanishes on the diagonal.

source
def Q2Presentation.Quadratic.polarizationCoeff {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [FiniteDimensional (ZMod 2) V] (q : QuadF2 V) (i j : Fin (Module.finrank (ZMod 2) V)) :
ZMod 2

The triangular coefficient matrix of the polarization, over finBasis.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Q2Presentation.Quadratic.polarization {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [FiniteDimensional (ZMod 2) V] (q : QuadF2 V) :
    V →ₗ[ZMod 2] V →ₗ[ZMod 2] ZMod 2

    The polarization bilinear map, via double Basis.constr.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Q2Presentation.Quadratic.polarization_basis {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [FiniteDimensional (ZMod 2) V] (q : QuadF2 V) (i j : Fin (Module.finrank (ZMod 2) V)) :
      ((polarization q) ((Module.finBasis (ZMod 2) V) i)) ((Module.finBasis (ZMod 2) V) j) = polarizationCoeff q i j
      source
      theorem Q2Presentation.Quadratic.polarization_add_flip {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [FiniteDimensional (ZMod 2) V] (q : QuadF2 V) :
      polarization q + (polarization q).flip = q.polar

      The polar law: the symmetrization of the polarization is the polar form. Proved as an equality of bilinear maps on basis pairs (Basis.ext twice), using polar_comm and the char-2 diagonal vanishing.

      source
      theorem Q2Presentation.Quadratic.polarization_polar {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [FiniteDimensional (ZMod 2) V] (q : QuadF2 V) (m m' : V) :
      ((polarization q) m) m' + ((polarization q) m') m = (q.polar m) m'
      source
      def Q2Presentation.Quadratic.polarizationDiagDefect {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [FiniteDimensional (ZMod 2) V] (q : QuadF2 V) :
      V →ₗ[ZMod 2] ZMod 2

      The diagonal defect of the polarization, as a linear map (additivity uses the polar law; F₂-linearity is automatic from additivity).

      Equations
      Instances For
        source
        theorem Q2Presentation.Quadratic.polarizationDiagDefect_eq_zero {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [FiniteDimensional (ZMod 2) V] (q : QuadF2 V) :
        polarizationDiagDefect q = 0

        The diagonal defect vanishes on the basis, hence everywhere.

        source
        theorem Q2Presentation.Quadratic.polarization_diagonal {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [FiniteDimensional (ZMod 2) V] (q : QuadF2 V) (m : V) :
        ((polarization q) m) m = q.form m

        The diagonal law: the polarization's diagonal is the quadratic form.