OAI/Algebra/DepthFive/BidegreeNonempty.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.exists_bidegree_exponent line 10

   Source documentation

   One variable on each side gives an explicit monomial of every bidegree.

   theorem exists_bidegree_exponent {σ : Type*} (isV : σ → Bool)
       (v u : σ) (hv : isV v = true) (hu : isV u = false) (a b : ℕ) :
       ∃ d : σ →₀ ℕ, Finsupp.weight (bidegreeWeight isV) d = (a, b) := by
   …

   Mentions: OAI.Problem335.bidegreeWeight

2. theorem OAI.Problem335.nonempty_bidegree_exponents line 17

   Source documentation

   The finite exponent-index subtype used by restricted operator matrices is inhabited.

   theorem nonempty_bidegree_exponents {σ : Type*} (isV : σ → Bool)
       (v u : σ) (hv : isV v = true) (hu : isV u = false) (a b : ℕ) :
       Nonempty {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight isV) d = (a, b)} := by
   …

   Mentions: OAI.Problem335.bidegreeWeight

3. theorem OAI.Problem335.exists_ne_zero_mem_bidegree line 25

   Source documentation

   The bidegree submodule contains a nonzero polynomial whenever both groups contain a variable.

   theorem exists_ne_zero_mem_bidegree {σ K : Type*} [CommSemiring K] [Nontrivial K]
       (isV : σ → Bool) (v u : σ) (hv : isV v = true) (hu : isV u = false)
       (a b : ℕ) :
       ∃ p : MvPolynomial σ K, p ∈ bidegreeSubmodule isV a b ∧ p ≠ 0 := by
   …

   Mentions: OAI.Problem335.bidegreeSubmodule

4. theorem OAI.Problem335.bidegreeSubmodule_nontrivial line 35

   Source documentation

   Nontriviality of the source and target homogeneous spaces.

   theorem bidegreeSubmodule_nontrivial {σ K : Type*} [CommSemiring K] [Nontrivial K]
       (isV : σ → Bool) (v u : σ) (hv : isV v = true) (hu : isV u = false)
       (a b : ℕ) : Nontrivial (bidegreeSubmodule (K := K) isV a b) := by
   …

   Mentions: OAI.Problem335.bidegreeSubmodule

5. theorem OAI.Problem335.bidegreeSubmodule_finrank_pos line 44

   Source documentation

   The source dimension cancelled in the rank comparison is strictly positive.

   theorem bidegreeSubmodule_finrank_pos {σ K : Type*} [Finite σ] [Field K]
       (isV : σ → Bool) (v u : σ) (hv : isV v = true) (hu : isV u = false)
       (a b : ℕ) : 0 < Module.finrank K (bidegreeSubmodule (K := K) isV a b) := by
   …

   Mentions: OAI.Problem335.bidegreeSubmodule