Documentation

LeanPool.Koethe.Mortality.FormalWord

Formal letters, specialization, and one scalar minor equation #

A formal letter is either a fixed vector or an independently indexed hole. The common-zero theorem is applied to the coefficients of a single pivot minor. Its equation count is the full word length plus one.

source
@[reducible, inline]
abbrev KoetheCounterexample.Mortality.FormalLetter (k : Type u_1) (N : ℕ) :
Type u_1

A formal letter: a fixed letter vector, or a hole indexed by one of N variable blocks.

Equations
Instances For
    source
    noncomputable def KoetheCounterexample.Mortality.letterCoeffs {k : Type u_1} {N : ℕ} [Field k] :
    FormalLetter k N → Fin 3 → HoleRing k N

    The three coefficients of a formal letter, as elements of the hole ring.

    Equations
    Instances For
      source
      def KoetheCounterexample.Mortality.letterDegree {k : Type u_1} {N : ℕ} :
      FormalLetter k N → Fin N → ℕ

      The multidegree of a formal letter: zero for a fixed letter, one unit of its block for a hole.

      Equations
      Instances For
        source
        def KoetheCounterexample.Mortality.specializeLetter {k : Type u_1} {N : ℕ} (x : Fin N × Fin 3 → k) :
        FormalLetter k N → Triple k

        Specialize a formal letter at an assignment of the hole variables.

        Equations
        Instances For
          source
          noncomputable def KoetheCounterexample.Mortality.formalProd {k : Type u_1} {N d : ℕ} [Field k] (P : Pencil k d) (w : List (FormalLetter k N)) :
          Matrix (Fin (d + 1)) (Fin (d + 1)) (Polynomial (HoleRing k N))

          The forward product of the pencil lifted along a formal word.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem KoetheCounterexample.Mortality.specializeLetter_inl {k : Type u_1} {N : ℕ} (x : Fin N × Fin 3 → k) (a : Triple k) :
            specializeLetter x (Sum.inl a) = a
            source
            @[simp]
            theorem KoetheCounterexample.Mortality.letterDegree_inl {k : Type u_1} {N : ℕ} (a : Triple k) :
            letterDegree (Sum.inl a) = 0
            source
            @[simp]
            theorem KoetheCounterexample.Mortality.letterDegree_inr {k : Type u_1} {N : ℕ} (b : Fin N) :
            letterDegree (Sum.inr b) = blockUnit b
            source
            theorem KoetheCounterexample.Mortality.constantWord_degree {k : Type u_1} {N : ℕ} (w : List (Triple k)) :
            (List.map letterDegree (List.map Sum.inl w)).sum = 0
            source
            theorem KoetheCounterexample.Mortality.specialize_constantWord {k : Type u_1} {N : ℕ} (x : Fin N × Fin 3 → k) (w : List (Triple k)) :
            List.map (specializeLetter x) (List.map Sum.inl w) = w
            source
            theorem KoetheCounterexample.Mortality.letterCoeffs_hom {k : Type u_1} {N : ℕ} [Field k] (a : FormalLetter k N) (j : Fin 3) :
            KoetheMultiProjective.IsMultiHomogeneous (letterCoeffs a j) (letterDegree a)
            source
            theorem KoetheCounterexample.Mortality.formalProd_hom {k : Type u_1} {N d : ℕ} [Field k] (P : Pencil k d) (w : List (FormalLetter k N)) :
            MatrixCoeffHom (formalProd P w) (List.map letterDegree w).sum
            source
            theorem KoetheCounterexample.Mortality.formalMinor_natDegree_le {k : Type u_1} {N d r : ℕ} [Field k] (P : Pencil k d) (w : List (FormalLetter k N)) (I J : Fin r → Fin (d + 1)) (hI : Function.Injective I) :
            ((formalProd P w).submatrix I J).det.natDegree ≤ w.length
            source
            theorem KoetheCounterexample.Mortality.specialize_lift {k : Type u_1} {N d : ℕ} [Field k] (P : Pencil k d) (a : FormalLetter k N) (x : Fin N × Fin 3 → k) :
            (P.lift (letterCoeffs a)).map ⇑(Polynomial.mapRingHom (MvPolynomial.eval x)) = P.eval (specializeLetter x a)
            source
            theorem KoetheCounterexample.Mortality.specialize_formalProd {k : Type u_1} {N d : ℕ} [Field k] (P : Pencil k d) (w : List (FormalLetter k N)) (x : Fin N × Fin 3 → k) :
            (formalProd P w).map ⇑(Polynomial.mapRingHom (MvPolynomial.eval x)) = P.wordProd (List.map (specializeLetter x) w)
            source
            theorem KoetheCounterexample.Mortality.exists_specialization_minor_zero {k : Type u_1} {N d r : ℕ} [Field k] [IsAlgClosed k] (P : Pencil k d) (w : List (FormalLetter k N)) (I J : Fin r → Fin (d + 1)) (hI : Function.Injective I) (hN : 0 < N) (hr : 0 < r) (hsize : w.length + 1 ≤ 2 * N) (hdegree : (List.map letterDegree w).sum = fun (x : Fin N) => 1) :
            ∃ (x : Fin N × Fin 3 → k), (∀ (b : Fin N), (fun (j : Fin 3) => x (b, j)) ≠ 0) ∧ ((P.wordProd (List.map (specializeLetter x) w)).submatrix I J).det = 0

            A formal word in which every hole block occurs once has a specialization with no zero block that kills any specified minor, provided the number of coefficient equations is at most twice the number of blocks.