Documentation

TauCeti.CommutativeAlgebra.MatrixFactorization.Polynomial

Polynomial matrix factorizations #

The rank-one factorization of X ^ (i + j) has differentials X ^ i and X ^ j. Its two components are finite free modules over the polynomial ring. For i ≤ n, the variant powerXOfLE is the rank-one factorization of the potential X ^ n with differentials X ^ i and X ^ (n - i).

source
noncomputable def TauCeti.MatrixFactorization.powerX (S : Type u) [CommRing S] (i j : ℕ) :
MatrixFactorization (Polynomial S) (Polynomial.X ^ (i + j))

The polynomial factorization S[X] --X^i--> S[X] --X^j--> S[X] of X^(i+j), obtained from rankOne. See powerXOfLE for the factorization indexed by X^n.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.MatrixFactorization.powerX_d₀ (S : Type u) [CommRing S] (i j : ℕ) :
    (powerX S i j).obj.d₀ = Polynomial.X ^ i • CategoryTheory.CategoryStruct.id ↧(Polynomial S)
    source
    @[simp]
    theorem TauCeti.MatrixFactorization.powerX_d₁ (S : Type u) [CommRing S] (i j : ℕ) :
    (powerX S i j).obj.d₁ = Polynomial.X ^ j • CategoryTheory.CategoryStruct.id ↧(Polynomial S)
    source
    @[simp]
    theorem TauCeti.MatrixFactorization.powerX_X₀ (S : Type u) [CommRing S] (i j : ℕ) :
    (powerX S i j).obj.X₀ = ↧(Polynomial S)
    source
    @[simp]
    theorem TauCeti.MatrixFactorization.powerX_X₁ (S : Type u) [CommRing S] (i j : ℕ) :
    (powerX S i j).obj.X₁ = ↧(Polynomial S)
    source
    noncomputable def TauCeti.MatrixFactorization.powerXOfLE (S : Type u) [CommRing S] {i n : ℕ} (h : i ≤ n) :
    MatrixFactorization (Polynomial S) (Polynomial.X ^ n)

    The polynomial factorization S[X] --X^i--> S[X] --X^(n-i)--> S[X] of X^n, for i ≤ n, obtained from rankOne.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.MatrixFactorization.powerXOfLE_d₀ (S : Type u) [CommRing S] {i n : ℕ} (h : i ≤ n) :
      (powerXOfLE S h).obj.d₀ = Polynomial.X ^ i • CategoryTheory.CategoryStruct.id ↧(Polynomial S)
      source
      @[simp]
      theorem TauCeti.MatrixFactorization.powerXOfLE_d₁ (S : Type u) [CommRing S] {i n : ℕ} (h : i ≤ n) :
      (powerXOfLE S h).obj.d₁ = Polynomial.X ^ (n - i) • CategoryTheory.CategoryStruct.id ↧(Polynomial S)
      source
      @[simp]
      theorem TauCeti.MatrixFactorization.powerXOfLE_X₀ (S : Type u) [CommRing S] {i n : ℕ} (h : i ≤ n) :
      (powerXOfLE S h).obj.X₀ = ↧(Polynomial S)
      source
      @[simp]
      theorem TauCeti.MatrixFactorization.powerXOfLE_X₁ (S : Type u) [CommRing S] {i n : ℕ} (h : i ≤ n) :
      (powerXOfLE S h).obj.X₁ = ↧(Polynomial S)