Documentation

Hironaka.AnalyticSpace.Oka.Coeff

The coefficient matrix of a row of polynomials #

In the third step of the proof of Oka's coherence theorem [Fre17, Ch. I, 10.3], the entries of the given row are Weierstrass polynomials in the distinguished variable, and the relations among them of bounded degree in that variable are read as the kernel of a matrix over the base whose entries are the coefficients of the polynomials ("our given map F induces an π’ͺ(V)-linear map π’ͺ(V)[z_n : m]^p β†’ π’ͺ(V)[z_n : m + d]"). Over a commutative ring R (the base stalk, or the ring of sections over an open subset of the base), for the polynomial polyOfCoeff c = Ξ£_k C (c k) X^k with coefficient vector c (Hironaka/AnalyticSpace/Oka/PolySection.lean), this module defines

These are the algebraic identities behind the core step hasLocalGeneratorsOn_polyRow (Hironaka.AnalyticSpace.Oka.Core), whose hypothesis hIH is the induction hypothesis on the base applied to coeffMatSec; they are not in the sources as separate statements.

source
theorem AnalyticSpace.polyOfCoeff_coeff {R : Type u_1} [CommRing R] {N : β„•} (Q : Polynomial R) (hQ : Q.natDegree < N) :
(polyOfCoeff fun (k : Fin N) => Q.coeff ↑k) = Q

A polynomial of degree < N is the polynomial of its first N coefficients.

source
def AnalyticSpace.coeffMat {R : Type u_1} [CommRing R] {q : β„•} (P : Fin q β†’ Polynomial R) (L N : β„•) :
Fin L β†’ Fin q Γ— Fin N β†’ R

Freitag's induced matrix [Fre17, Ch. I, 10.3]: the (l, (j, k)) entry is the coefficient of X^{lβˆ’k} in P_j (zero if k > l).

Equations
Instances For
    source
    theorem AnalyticSpace.coeff_sum_mul_polyOfCoeff {R : Type u_1} [CommRing R] {q N : β„•} (P : Fin q β†’ Polynomial R) (c : Fin q β†’ Fin N β†’ R) (l : β„•) :
    (βˆ‘ j : Fin q, P j * polyOfCoeff (c j)).coeff l = βˆ‘ jk : Fin q Γ— Fin N, (if ↑jk.2 ≀ l then (P jk.1).coeff (l - ↑jk.2) else 0) * c jk.1 jk.2

    The l-th coefficient of Ξ£_j P_j Β· polyOfCoeff (c j) is the l-th entry of coeffMat P Β· c.

    source
    theorem AnalyticSpace.natDegree_sum_mul_polyOfCoeff_lt {R : Type u_1} [CommRing R] {q N d : β„•} (P : Fin q β†’ Polynomial R) (hP : βˆ€ (j : Fin q), (P j).natDegree < d) (c : Fin q β†’ Fin N β†’ R) (hN : 0 < N) :
    (βˆ‘ j : Fin q, P j * polyOfCoeff (c j)).natDegree < d + N
    source
    theorem AnalyticSpace.sum_mul_polyOfCoeff_eq_zero_iff {R : Type u_1} [CommRing R] {q N d : β„•} (P : Fin q β†’ Polynomial R) (hP : βˆ€ (j : Fin q), (P j).natDegree < d) (c : Fin q β†’ Fin N β†’ R) (hN : 0 < N) :
    βˆ‘ j : Fin q, P j * polyOfCoeff (c j) = 0 ↔ βˆ€ (l : Fin (d + N)), βˆ‘ jk : Fin q Γ— Fin N, coeffMat P (d + N) N l jk * c jk.1 jk.2 = 0

    For P_j of degree < d and 0 < N, the relation Ξ£_j P_j Β· polyOfCoeff (c j) = 0 is the system of d + N coefficient equations coeffMat P (d + N) N Β· c = 0.

    source
    def AnalyticSpace.coeffMat' {R : Type u_1} [CommRing R] {q : β„•} (P : Fin q β†’ Polynomial R) (L N : β„•) :
    Fin L β†’ Fin (q * N) β†’ R

    The coefficient matrix with the pairs (j, k) reindexed by finProdFinEquiv, as a Fin-indexed matrix.

    Equations
    Instances For
      source
      def AnalyticSpace.flatCoeff {R : Type u_1} {q N : β„•} (c : Fin q β†’ Fin N β†’ R) :
      Fin (q * N) β†’ R

      The reindexed coefficient vector (j, k) ↦ c j k.

      Equations
      Instances For
        source
        theorem AnalyticSpace.flatCoeff_apply {R : Type u_1} {q N : β„•} (c : Fin q β†’ Fin N β†’ R) (jk : Fin q Γ— Fin N) :
        flatCoeff c (finProdFinEquiv jk) = c jk.1 jk.2
        source
        theorem AnalyticSpace.sum_mul_polyOfCoeff_eq_zero_iff_mem_relKer {R : Type u_1} [CommRing R] {q N d : β„•} (P : Fin q β†’ Polynomial R) (hP : βˆ€ (j : Fin q), (P j).natDegree < d) (c : Fin q β†’ Fin N β†’ R) (hN : 0 < N) :
        βˆ‘ j : Fin q, P j * polyOfCoeff (c j) = 0 ↔ flatCoeff c ∈ Manifold.relKer (coeffMat' P (d + N) N)

        For P_j of degree < d and 0 < N, Ξ£_j P_j Β· polyOfCoeff (c j) = 0 iff the flattened coefficient vector is a relation of the reindexed matrix.

        source
        noncomputable def AnalyticSpace.coeffMatSec {K : Type} [RCLike K] {m q d : β„•} {V : TopologicalSpace.Opens (Kn K m)} (pc : Fin q β†’ Fin d β†’ ↑((sheafKn K m).presheaf.obj (Opposite.op V))) (L N : β„•) :
        Fin L β†’ Fin (q * N) β†’ ↑((sheafKn K m).presheaf.obj (Opposite.op V))

        The matrix of sections over the base whose germs form the coefficient matrix of the row of polynomials j ↦ polyOfCoeff (germ ∘ pc j) (each of degree < d): the entry (l, (j, k)) is pc j (l βˆ’ k) if k ≀ l < k + d, else 0.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem AnalyticSpace.germ_coeffMatSec {K : Type} [RCLike K] {m q d : β„•} {V : TopologicalSpace.Opens (Kn K m)} (pc : Fin q β†’ Fin d β†’ ↑((sheafKn K m).presheaf.obj (Opposite.op V))) (L N : β„•) {b : Kn K m} (hb : b ∈ V) (l : Fin L) (i : Fin (q * N)) :
          (CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V b hb)) (coeffMatSec pc L N l i) = coeffMat' (fun (j : Fin q) => polyOfCoeff fun (k : Fin d) => (CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V b hb)) (pc j k)) L N l i

          The germs of coeffMatSec form the coefficient matrix of the polynomials with the germs of the coefficients.