BidegreeDimension.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.splitBidegreeExponents line 14

Source documentation

Split a finite exponent vector into its derivative and multiplication coordinates.

def splitBidegreeExponents {σ : Type u} [Fintype σ] (side : σ → Bool) :
    (σ →₀ ℕ) ≃ ({i : σ // side i = true} →₀ ℕ) ×
      ({i : σ // side i = false} →₀ ℕ) := by
…

theorem OAI.Problem335.weight_splitBidegreeExponents line 37

Source documentation

The bidegree is the pair of total degrees of the restricted exponent vectors.

theorem weight_splitBidegreeExponents {σ : Type u} [Fintype σ]
    (side : σ → Bool) (m : σ →₀ ℕ) :
    Finsupp.weight (bidegreeWeight side) m =
      ((splitBidegreeExponents side m).1.degree,
       (splitBidegreeExponents side m).2.degree) := by
…

Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.splitBidegreeExponents

def OAI.Problem335.bidegreeFinsuppExponentsEquiv line 60

Source documentation

A fixed bidegree fiber is the product of two ordinary degree fibers.

def bidegreeFinsuppExponentsEquiv {σ : Type u} [Fintype σ] (side : σ → Bool) (a b : ℕ) :
    {m : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) m = (a, b)} ≃
      {m : {i : σ // side i = true} →₀ ℕ // m.degree = a} ×
      {m : {i : σ // side i = false} →₀ ℕ // m.degree = b} :=
…

Mentions: OAI.Problem335.bidegreeWeight

theorem OAI.Problem335.card_bidegree_finsupp_exponents line 80

Source documentation

Counting bidegree monomials separates into the two variable groups.

theorem card_bidegree_finsupp_exponents {σ : Type u} [Fintype σ]
    (side : σ → Bool) (a b : ℕ) :
    Nat.card {m : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) m = (a, b)} =
      Nat.multichoose (Fintype.card {i : σ // side i = true}) a *
      Nat.multichoose (Fintype.card {i : σ // side i = false}) b := by
…

Mentions: OAI.Problem335.bidegreeWeight

theorem OAI.Problem335.bidegreeSubmodule_finrank line 89
Source documentation
Exact finite dimension of the polynomial subspace used by the mixed operator.
```
theorem bidegreeSubmodule_finrank (K : Type u) [Field K]
    {σ : Type v} [Fintype σ] (side : σ → Bool) (a b : ℕ) :
    Module.finrank K (bidegreeSubmodule (K := K) side a b) =
…
```
Mentions: OAI.Problem335.bidegreeSubmodule

theorem OAI.Problem335.bidegreeSubmodule_finrank_choose line 102

Source documentation

Stars-and-bars form, with no nonemptiness hypothesis needed.

theorem bidegreeSubmodule_finrank_choose (K : Type u) [Field K]
    {σ : Type v} [Fintype σ] (side : σ → Bool) (a b : ℕ) :
    Module.finrank K (bidegreeSubmodule (K := K) side a b) =
…

Mentions: OAI.Problem335.bidegreeSubmodule