Square-free polynomial coefficients

noncomputable def LatinQuarter.repeatedTagIdeal (κ : Type u_1) : Ideal (MvPolynomial κ (ZMod 2))

The discarded monomials: those divisible by the square of a tag.

Equations

• LatinQuarter.repeatedTagIdeal κ = Ideal.span ((fun (d : κ →₀ ℕ) => (MvPolynomial.monomial d) 1) '' Set.range fun (j : κ) => Finsupp.single j 2)

theorem LatinQuarter.squarefree_coeff_zero_of_mem {κ : Type u_1} {p : MvPolynomial κ (ZMod 2)} (hp : p ∈ repeatedTagIdeal κ) {d : κ →₀ ℕ} (hd : ∀ (j : κ), d j ≤ 1) : p.coeff d = 0

Discarding repeated tags cannot affect any square-free coefficient.

theorem LatinQuarter.repeatedTagIdeal_ne_top (κ : Type u_1) : repeatedTagIdeal κ ≠ ⊤

@[reducible, inline]

abbrev LatinQuarter.TagRing (κ : Type u_1) : Type u_1

Polynomials modulo two, with the square of every tag set to zero.

Equations

• LatinQuarter.TagRing κ = (MvPolynomial κ (ZMod 2) ⧸ LatinQuarter.repeatedTagIdeal κ)

instance LatinQuarter.instNontrivialTagRing (κ : Type u_1) : Nontrivial (TagRing κ)

instance LatinQuarter.instCharPTagRingOfNatNat (κ : Type u_1) : CharP (TagRing κ) 2

noncomputable def LatinQuarter.tag {κ : Type u_1} (j : κ) : TagRing κ

The image of a polynomial variable in the square-zero bookkeeping quotient.

Equations

• LatinQuarter.tag j = (Ideal.Quotient.mk (LatinQuarter.repeatedTagIdeal κ)) (MvPolynomial.X j)

@[simp]

theorem LatinQuarter.tag_sq {κ : Type u_1} (j : κ) : tag j * tag j = 0

theorem LatinQuarter.squarefree_coeff_zero_of_quotient_zero {κ : Type u_1} {p : MvPolynomial κ (ZMod 2)} (hp : (Ideal.Quotient.mk (repeatedTagIdeal κ)) p = 0) {d : κ →₀ ℕ} (hd : ∀ (j : κ), d j ≤ 1) : p.coeff d = 0

A zero polynomial in the bookkeeping ring has zero square-free coefficients in the original polynomial ring.

theorem LatinQuarter.coeff_prod_add_constants {ι : Type u_1} {κ : Type u_2} [Fintype ι] (f : ι → κ) (a : ι → ZMod 2) (d : κ →₀ ℕ) (hd : ∑ j ∈ d.support, d j = Fintype.card ι) : (∏ i : ι, (MvPolynomial.X (f i) + MvPolynomial.C (a i))).coeff d = (∏ i : ι, MvPolynomial.X (f i)).coeff d

Adding constants to m individual tags does not change a coefficient of total degree m. This also allows zero constants.

noncomputable def LatinQuarter.allTagsExponent (κ : Type u_1) [Fintype κ] : κ →₀ ℕ

The exponent vector for the product of all tags, once each.

Equations

• LatinQuarter.allTagsExponent κ = ∑ j : κ, Finsupp.single j 1

@[simp]

theorem LatinQuarter.allTagsExponent_apply {κ : Type u_1} [Fintype κ] (j : κ) : (allTagsExponent κ) j = 1

@[simp]

theorem LatinQuarter.allTagsExponent_support {κ : Type u_1} [Fintype κ] : (allTagsExponent κ).support = Finset.univ

theorem LatinQuarter.allTagsExponent_degree {κ : Type u_1} [Fintype κ] : ∑ j ∈ (allTagsExponent κ).support, (allTagsExponent κ) j = Fintype.card κ

theorem LatinQuarter.coeff_allTags_product {κ : Type u_1} [Fintype κ] : (∏ j : κ, MvPolynomial.X j).coeff (allTagsExponent κ) = 1