Documentation

MIPRE.Foundations.CL.Canonical

Canonical complements and canonical linear maps #

The paper's preliminaries.tex, sec:linear-spaces: two different "perps", both needed by the seeded CL low-degree test, whose questions are (uโ‚€, s) and (uโ‚€, s, v) with uโ‚€ = L^Ln_v(u) the canonical representative of a line.

The paper defines the canonical complement by reduced row echelon form. This file uses the equivalent characterization rk:cancomp credits to a referee, which is what makes the construction formalizable and its well-definedness immediate: with uโฑผ = dim (S โŠ“ span {eแตข : i โ‰ฅ j}), the complement is {eโฑผ : uโฑผ = u_{j+1}}. It depends on the subspace S = span F alone, with no echelon form, no choice of basis and no ordering of F to quotient by --- so canonLin, the projector onto that complement parallel to S (def:cl-canonical), is a function of S, which is exactly what rk:cancomp has to argue.

pivots S is the paper's set J of pivot columns, and #(pivots S) = dim S (card_pivots): the two characterizations agree.

Coordinate subspaces cut out by vanishing #

source
def MIPRE.CL.coordSub {F : Type u_1} [Field F] {n : โ„•} (J : Finset (Fin n)) :
Submodule F (Fin n โ†’ F)

coordSub J, the vectors vanishing on J: the span of {eโฑผ : j โˆ‰ J}.

Equations
  • MIPRE.CL.coordSub J = { carrier := {x : Fin n โ†’ F | โˆ€ j โˆˆ J, x j = 0}, add_mem' := โ‹ฏ, zero_mem' := โ‹ฏ, smul_mem' := โ‹ฏ }
Instances For
    source
    @[simp]
    theorem MIPRE.CL.mem_coordSub {F : Type u_1} [Field F] {n : โ„•} {J : Finset (Fin n)} {x : Fin n โ†’ F} :
    x โˆˆ coordSub J โ†” โˆ€ j โˆˆ J, x j = 0
    source
    def MIPRE.CL.projTo {F : Type u_1} [Field F] {n : โ„•} (J : Finset (Fin n)) :
    (Fin n โ†’ F) โ†’โ‚—[F] โ†ฅJ โ†’ F

    The projection onto the coordinates in J.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.CL.projTo_apply {F : Type u_1} [Field F] {n : โ„•} (J : Finset (Fin n)) (x : Fin n โ†’ F) (j : โ†ฅJ) :
      (projTo J) x j = x โ†‘j
      source
      theorem MIPRE.CL.ker_projTo {F : Type u_1} [Field F] {n : โ„•} (J : Finset (Fin n)) :
      (projTo J).ker = coordSub J
      source
      theorem MIPRE.CL.surjective_projTo {F : Type u_1} [Field F] {n : โ„•} (J : Finset (Fin n)) :
      Function.Surjective โ‡‘(projTo J)
      source
      theorem MIPRE.CL.finrank_coordSub {F : Type u_1} [Field F] {n : โ„•} (J : Finset (Fin n)) :
      Module.finrank F โ†ฅ(coordSub J) = n - J.card

      The tail subspaces and the pivot set #

      source
      def MIPRE.CL.tail {F : Type u_1} [Field F] (n j : โ„•) :
      Submodule F (Fin n โ†’ F)

      tail j = span {eแตข : i โ‰ฅ j}, the vectors whose coordinates below j vanish.

      Equations
      Instances For
        source
        @[simp]
        theorem MIPRE.CL.mem_tail {F : Type u_1} [Field F] {n j : โ„•} {x : Fin n โ†’ F} :
        x โˆˆ tail n j โ†” โˆ€ (i : Fin n), โ†‘i < j โ†’ x i = 0
        source
        @[simp]
        theorem MIPRE.CL.tail_zero {F : Type u_1} [Field F] {n : โ„•} :
        tail n 0 = โŠค
        source
        @[simp]
        theorem MIPRE.CL.tail_card {F : Type u_1} [Field F] {n : โ„•} :
        tail n n = โŠฅ
        source
        theorem MIPRE.CL.tail_mono {F : Type u_1} [Field F] {n j k : โ„•} (h : j โ‰ค k) :
        tail n k โ‰ค tail n j
        source
        noncomputable def MIPRE.CL.dimTail {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) (j : โ„•) :
        โ„•

        uโฑผ = dim (S โŠ“ tail j), the dimension sequence of rk:cancomp.

        Equations
        Instances For
          source
          @[irreducible]
          noncomputable def MIPRE.CL.pivots {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
          Finset (Fin n)

          The pivot set J of S: the indices at which the dimension sequence drops.

          Equations
          Instances For
            source
            theorem MIPRE.CL.mem_pivots {F : Type u_1} [Field F] {n : โ„•} {S : Submodule F (Fin n โ†’ F)} {j : Fin n} :
            j โˆˆ pivots S โ†” dimTail S (โ†‘j + 1) < dimTail S โ†‘j
            source
            theorem MIPRE.CL.dimTail_antitone {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) {j k : โ„•} (h : j โ‰ค k) :
            dimTail S k โ‰ค dimTail S j
            source
            theorem MIPRE.CL.tail_eq_bot {F : Type u_1} [Field F] {n j : โ„•} (h : n โ‰ค j) :
            tail n j = โŠฅ
            source
            theorem MIPRE.CL.dimTail_le_succ {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) (j : โ„•) :
            dimTail S j โ‰ค dimTail S (j + 1) + 1
            source
            @[simp]
            theorem MIPRE.CL.dimTail_zero {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
            dimTail S 0 = Module.finrank F โ†ฅS
            source
            @[simp]
            theorem MIPRE.CL.dimTail_top {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
            dimTail S n = 0
            source
            theorem MIPRE.CL.card_filter_lt_succ_of_mem {n : โ„•} (P : Finset (Fin n)) {j : โ„•} (hj : j < n) (hp : โŸจj, hjโŸฉ โˆˆ P) :
            {i โˆˆ P | โ†‘i < j + 1}.card = {i โˆˆ P | โ†‘i < j}.card + 1

            Counting the pivots below j + 1, for an arbitrary index set, in the two cases separately. Stated for a variable Finset, and with no if, on purpose: pivots S is a Finset.filter over a Nat inequality between finranks, so it carries a Decidable instance that cannot be evaluated, and either letting simp see through it or asking rw to unify it against a Classical instance costs a whnf timeout.

            source
            theorem MIPRE.CL.card_filter_lt_succ_of_notMem {n : โ„•} (P : Finset (Fin n)) {j : โ„•} (hj : j < n) (hp : โŸจj, hjโŸฉ โˆ‰ P) :
            {i โˆˆ P | โ†‘i < j + 1} = {i โˆˆ P | โ†‘i < j}
            source
            theorem MIPRE.CL.filter_lt_of_le {n : โ„•} (P : Finset (Fin n)) {j : โ„•} (hj : n โ‰ค j) :
            {i โˆˆ P | โ†‘i < j} = P
            source
            theorem MIPRE.CL.dimTail_add_card_pivots {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) (j : โ„•) :
            dimTail S j + {i โˆˆ pivots S | โ†‘i < j}.card = Module.finrank F โ†ฅS
            source
            theorem MIPRE.CL.card_pivots {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
            (pivots S).card = Module.finrank F โ†ฅS

            The canonical complement and the canonical linear map #

            source
            noncomputable def MIPRE.CL.canonCompl {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
            Submodule F (Fin n โ†’ F)

            The canonical complement of S (def:canonical-complement): the span of the standard basis vectors off the pivot set.

            Equations
            Instances For
              source
              theorem MIPRE.CL.isCompl_canonCompl {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
              IsCompl S (canonCompl S)

              lem:canonical-complement: S and its canonical complement are complementary.

              source
              noncomputable def MIPRE.CL.canonLin {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
              (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F

              The canonical linear map with kernel S (def:cl-canonical): the projector onto the canonical complement of S, parallel to S. It is a function of S alone, which is what rk:cancomp argues.

              Equations
              Instances For
                source
                @[simp]
                theorem MIPRE.CL.ker_canonLin {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
                (canonLin S).ker = S

                The canonical linear map has kernel exactly S: it is "the canonical linear map with kernel S" of def:cl-canonical.

                source
                @[simp]
                theorem MIPRE.CL.range_canonLin {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
                (canonLin S).range = canonCompl S
                source
                theorem MIPRE.CL.sub_canonLin_mem {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) (x : Fin n โ†’ F) :
                x - (canonLin S) x โˆˆ S

                A point differs from its canonical representative by an element of S. For a line --- S = span {w} --- this is the statement that the base point the seeded test reports lies on the line through the sampled point, which is what lets a line answer be evaluated at the point.

                The dot product and orthogonal complements #

                The paper's other perp: the orthogonal complement for the standard dot product. Over a finite field it need not be a direct-sum complement, but lem:perp_perp holds over every field.

                source
                def MIPRE.CL.dotForm (F : Type u_2) [Field F] (n : โ„•) :
                LinearMap.BilinForm F (Fin n โ†’ F)

                The standard dot product on Fin n โ†’ F, as a bilinear form.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem MIPRE.CL.dotForm_apply {F : Type u_1} [Field F] {n : โ„•} (x y : Fin n โ†’ F) :
                  ((dotForm F n) x) y = โˆ‘ i : Fin n, x i * y i
                  source
                  theorem MIPRE.CL.dotForm_comm {F : Type u_1} [Field F] {n : โ„•} (x y : Fin n โ†’ F) :
                  ((dotForm F n) x) y = ((dotForm F n) y) x
                  source
                  theorem MIPRE.CL.dotForm_isRefl {F : Type u_1} [Field F] {n : โ„•} :
                  (dotForm F n).IsRefl
                  source
                  theorem MIPRE.CL.dotForm_nondegenerate {F : Type u_1} [Field F] {n : โ„•} :
                  (dotForm F n).Nondegenerate
                  source
                  def MIPRE.CL.perp {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
                  Submodule F (Fin n โ†’ F)

                  The orthogonal complement of S for the dot product. Over a finite field this need not be a complement of S --- span{(1,1)} over ๐”ฝโ‚‚ is orthogonal to itself --- which is exactly why the canonical complement above exists.

                  Equations
                  Instances For
                    source
                    theorem MIPRE.CL.mem_perp {F : Type u_1} [Field F] {n : โ„•} {S : Submodule F (Fin n โ†’ F)} {x : Fin n โ†’ F} :
                    x โˆˆ perp S โ†” โˆ€ y โˆˆ S, โˆ‘ i : Fin n, y i * x i = 0
                    source
                    theorem MIPRE.CL.finrank_perp {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
                    Module.finrank F โ†ฅ(perp S) = n - Module.finrank F โ†ฅS

                    lem:perp_perp, first part: dim S + dim Sแ—ฎ = n.

                    source
                    theorem MIPRE.CL.perp_perp {F : Type u_1} [Field F] {n : โ„•} (S : Submodule F (Fin n โ†’ F)) :
                    perp (perp S) = S

                    lem:perp_perp, second part: the dot-product perp is an involution on subspaces, over every field.

                    L^โŠฅ #

                    source
                    noncomputable def MIPRE.CL.lperp {F : Type u_1} [Field F] {n : โ„•} (L : (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) :
                    (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F

                    L^โŠฅ of def:Lperp: the canonical linear map whose kernel is (ker L)แ—ฎ.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem MIPRE.CL.ker_lperp {F : Type u_1} [Field F] {n : โ„•} (L : (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) :
                      (lperp L).ker = perp L.ker

                      lem:L_perp_perp: ker (L^โŠฅ) = (ker L)แ—ฎ.