OAI/Algebra/DepthFive/BidegreeBasis.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.bidegreeMonomialBasis line 12

   Source documentation

   Ordinary monomial basis of a fixed bidegree subspace.

   def bidegreeMonomialBasis (K : Type u) [CommSemiring K]
       {σ : Type v} (side : σ → Bool) (a b : ℕ) :
       Module.Basis {m : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) m = (a, b)} K
         (bidegreeSubmodule (K := K) side a b) :=
   …

   Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.bidegreeSubmodule

2. theorem OAI.Problem335.bidegreeMonomialBasis_repr line 22
3. theorem OAI.Problem335.bidegreeMonomialBasis_apply line 29
4. instance OAI.Problem335.bidegreeMonomialFintype line 47

   Source documentation

   Finite monomial indexing for bidegree spaces over a finite variable set.

   instance bidegreeMonomialFintype {σ : Type v} [Finite σ]
       (side : σ → Bool) (a b : ℕ) :
       Fintype {m : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) m = (a, b)} :=
   …

   Mentions: OAI.Problem335.bidegreeWeight

5. theorem OAI.Problem335.bidegree_toMatrix_apply line 53

   Source documentation

   Matrix entries in the ordinary bidegree monomial bases are polynomial coefficients.

   theorem bidegree_toMatrix_apply (K : Type u) [CommSemiring K]
       {σ : Type v} [Finite σ] [DecidableEq σ] (side : σ → Bool) (a b c d : ℕ)
       (F : bidegreeSubmodule (K := K) side a b →ₗ[K]
   …

   Mentions: OAI.Problem335.bidegreeSubmodule