Shifted square-zero tags

noncomputable def LatinQuarter.markedConstant {N : Type u_1} {k h : ℕ} (e : Fin k ⊕ Fin h ≃ N) (c s : N) : ZMod 2

The k dummy entries occupy distinct rows and columns, indexed by the left summand of e.

Equations

• LatinQuarter.markedConstant e c s = if (e.symm c).isLeft = true ∧ c = s then 1 else 0

noncomputable def LatinQuarter.shiftedTags {N : Type u_1} {k h : ℕ} (e : Fin k ⊕ Fin h ≃ N) : Matrix N N (TagRing (N × N))

Square-zero bookkeeping variables with a chosen diagonal block marked by ones.

Equations

• LatinQuarter.shiftedTags e c s = LatinQuarter.tag (c, s) + (algebraMap (ZMod 2) (LatinQuarter.TagRing (N × N))) (LatinQuarter.markedConstant e c s)

theorem LatinQuarter.shiftedTags_square {N : Type u_1} {k h : ℕ} (e : Fin k ⊕ Fin h ≃ N) (c s : N) : squareHom (shiftedTags e c s) = (algebraMap (ZMod 2) (TagRing (N × N))) (markedConstant e c s)

theorem LatinQuarter.shifted_tags_product_vanishes {N : Type u_1} {ι : Type u_2} [Fintype ι] {k h : ℕ} (e : Fin k ⊕ Fin h ≃ N) (α : ι → Type u_3) [(i : ι) → Fintype (α i)] [(i : ι) → DecidableEq (α i)] (r c : (i : ι) → α i → N) (hbudget : h * h < ∑ i : ι, (Fintype.card (α i) - k)) : ∏ i : ι, ((shiftedTags e).submatrix (r i) (c i)).det = 0

A version of the vanishing lemma allowing arbitrary finite sets of selected rows and columns in each minor.