Module

SignPolynomialMonomials.lean

Nyll.SchemeTheory.RingTheory.SignPolynomialMonomials

5 declarations indexed from sourceView source ↗

Module documentation

Even monomials are products of quadratic monomials

This supplies the concrete monomial factorization needed by Stacks Project, Tag 0BTE, including the case of zero variables.

Imports8

Mathlib.Algebra.MvPolynomial.Basic
Mathlib.Algebra.Algebra.Subalgebra.Lattice
Mathlib.Data.Multiset.Basic
Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Mathlib.Data.Finsupp.Multiset
Mathlib.Data.Finsupp.Weight
Mathlib.Data.List.Induction
Mathlib.Algebra.Ring.Parity

Imported by2

def

quadraticSubalgebra

L31 ↗

SchemeTheory.SignPolynomial.quadraticSubalgebra

Documentation

The literal subalgebra generated by the pairwise products of variables.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)

Lean source · statement

def quadraticSubalgebra : Subalgebra k (MvPolynomial (Fin n) k)

theorem

quadratic_mem

L35 ↗

SchemeTheory.SignPolynomial.quadratic_mem

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)

Lean source · statement

theorem quadratic_mem (i j : Fin n) :
    (X i : MvPolynomial (Fin n) k) * X j ∈ quadraticSubalgebra k n

theorem

list_prod_X_mem

L39 ↗

SchemeTheory.SignPolynomial.list_prod_X_mem

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)

Lean source · full declaration

theorem list_prod_X_mem (l : List (Fin n)) (hl : Even l.length) :
    (l.map (fun i : Fin n => (X i : MvPolynomial (Fin n) k))).prod ∈
      quadraticSubalgebra k n := by
  revert hl
  induction l using List.twoStepInduction with
  | nil =>
      intro _hl
      exact (quadraticSubalgebra k n).one_mem
  | singleton i =>
      intro hl
      exact False.elim (Nat.not_even_one hl)
  | cons_cons i j l ih _ =>
      intro hl
      have hl' : Even l.length := by
        simpa only [List.length_cons, Nat.succ_eq_add_one, Nat.even_add_one, not_not] using hl
      simpa only [List.map_cons, List.prod_cons, mul_assoc] using
        (quadraticSubalgebra k n).mul_mem (quadratic_mem k n i j) (ih hl')

theorem

list_prod_X_eq_monomial

L57 ↗

SchemeTheory.SignPolynomial.list_prod_X_eq_monomial

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)

Lean source · full declaration

theorem list_prod_X_eq_monomial (d : Fin n →₀ ℕ) :
    (d.toMultiset.toList.map (fun i : Fin n => (X i : MvPolynomial (Fin n) k))).prod =
      monomial d 1 := by
  calc
    _ = (d.toMultiset.map (fun i : Fin n => (X i : MvPolynomial (Fin n) k))).prod := by
      rw [← Multiset.prod_coe, ← Multiset.map_coe, Multiset.coe_toList]
    _ = (Finsupp.mapDomain (fun i : Fin n => (X i : MvPolynomial (Fin n) k)) d).prod
        (fun p e => p ^ e) := by
      rw [Finsupp.toMultiset_map, Finsupp.prod_toMultiset]
    _ = d.prod (fun i e => (X i : MvPolynomial (Fin n) k) ^ e) :=
      Finsupp.prod_mapDomain_index (fun p => pow_zero p) (fun p a b => pow_add p a b)
    _ = monomial d 1 := (MvPolynomial.monic_monomial_eq d).symm

theorem

monomial_mem_quadraticSubalgebra

L71 ↗

SchemeTheory.SignPolynomial.monomial_mem_quadraticSubalgebra

Documentation

Every even-degree monomial belongs to the quadratic-generator subalgebra.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)

Lean source · statement

theorem monomial_mem_quadraticSubalgebra (d : Fin n →₀ ℕ) (c : k)
    (hd : Even d.degree) : monomial d c ∈ quadraticSubalgebra k n

Module documentation

Even monomials are products of quadratic monomials

Declarations

quadraticSubalgebra

quadratic_mem

list_prod_X_mem

list_prod_X_eq_monomial

monomial_mem_quadraticSubalgebra