Small exterior-coordinate layer

Only the exterior degrees used by the manuscript are represented here. In characteristic two an alternating two-form is a symmetric zero-diagonal matrix, and the signs in the coordinate wedge formulas disappear. These explicit bilinear maps avoid constructing or deciding equality in a large general-purpose exterior algebra.

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.LinearForm : Type

Coefficients of a linear form in the eight input variables.

Equations

• UnrestrictedBooleanMul.N4.LinearForm = (Fin 8 → UnrestrictedBooleanMul.F₂)

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.TwoForm : Type

Two-index coordinate arrays used to represent exterior two-forms.

Equations

• UnrestrictedBooleanMul.N4.TwoForm = (Fin 8 → Fin 8 → UnrestrictedBooleanMul.F₂)

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.ThreeForm : Type

Three-index coordinate arrays used to represent exterior three-forms.

Equations

• UnrestrictedBooleanMul.N4.ThreeForm = (Fin 8 → Fin 8 → Fin 8 → UnrestrictedBooleanMul.F₂)

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.FourForm : Type

Four-index coordinate arrays used to represent exterior four-forms.

Equations

• UnrestrictedBooleanMul.N4.FourForm = (Fin 8 → Fin 8 → Fin 8 → Fin 8 → UnrestrictedBooleanMul.F₂)

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.FiveForm : Type

Five-index coordinate arrays used to represent exterior five-forms.

Equations

• UnrestrictedBooleanMul.N4.FiveForm = (Fin 8 → Fin 8 → Fin 8 → Fin 8 → Fin 8 → UnrestrictedBooleanMul.F₂)

def UnrestrictedBooleanMul.N4.vectorWedgeN {n : ℕ} (u v : Fin n → F₂) : Fin n → Fin n → F₂

Dimension-polymorphic versions used for quotient and tail arguments.

Equations

• UnrestrictedBooleanMul.N4.vectorWedgeN u v i j = u i * v j + u j * v i

def UnrestrictedBooleanMul.N4.vectorWedgeTwoN {n : ℕ} (u : Fin n → F₂) (q : Fin n → Fin n → F₂) : Fin n → Fin n → Fin n → F₂

Coordinates of a vector wedged with a two-form, in arbitrary finite dimension.

Equations

• UnrestrictedBooleanMul.N4.vectorWedgeTwoN u q i j k = u i * q j k + u j * q i k + u k * q i j

theorem UnrestrictedBooleanMul.N4.decomposable_of_vectorWedgeTwoN_zero {n : ℕ} (u : Fin n → F₂) (q : Fin n → Fin n → F₂) (hu : u ≠ 0) (h : vectorWedgeTwoN u q = 0) : ∃ (v : Fin n → F₂), q = vectorWedgeN u v

If wedging a nonzero vector with an alternating two-form vanishes, that two-form has the vector as a decomposable factor.

def UnrestrictedBooleanMul.N4.vectorWedge (u v : LinearForm) : TwoForm

Exterior product of two vectors.

Equations

• UnrestrictedBooleanMul.N4.vectorWedge u v i j = u i * v j + u j * v i

def UnrestrictedBooleanMul.N4.vectorWedgeTwo (u : LinearForm) (q : TwoForm) : ThreeForm

Exterior product of a vector and a two-form.

Equations

• UnrestrictedBooleanMul.N4.vectorWedgeTwo u q i j k = u i * q j k + u j * q i k + u k * q i j

theorem UnrestrictedBooleanMul.N4.vectorWedgeTwo_repeated_left (x y : LinearForm) : vectorWedgeTwo x (vectorWedge x y) = 0

theorem UnrestrictedBooleanMul.N4.vectorWedgeTwo_repeated_right (x y : LinearForm) : vectorWedgeTwo y (vectorWedge x y) = 0

theorem UnrestrictedBooleanMul.N4.vectorWedgeTwo_smul_left (a : F₂) (x : LinearForm) (q : TwoForm) : vectorWedgeTwo (a • x) q = a • vectorWedgeTwo x q

theorem UnrestrictedBooleanMul.N4.mem_support_of_vectorWedgeTwo_zero (u x y : LinearForm) (hxy : vectorWedge x y ≠ 0) (h : vectorWedgeTwo u (vectorWedge x y) = 0) : ∃ (a : F₂) (b : F₂), u = a • x + b • y

A vector annihilating a nonzero decomposable two-form belongs to its two-dimensional support. This is the coordinate form of exactness of the Koszul complex in degree one.

def UnrestrictedBooleanMul.N4.wedgeTwo (q c : TwoForm) : FourForm

Exterior product of two two-forms. The six terms remember which of the two input forms receives each pair.

Equations

• UnrestrictedBooleanMul.N4.wedgeTwo q c i j k l = q i j * c k l + q i k * c j l + q i l * c j k + c i j * q k l + c i k * q j l + c i l * q j k

def UnrestrictedBooleanMul.N4.wedgeThreeTwo (h : ThreeForm) (q : TwoForm) : FiveForm

Exterior product of a cubic and a two-form.

Equations

• One or more equations did not get rendered due to their size.

def UnrestrictedBooleanMul.N4.vectorWedgeFour (u : LinearForm) (w : FourForm) : FiveForm

Exterior product of a vector and a four-form.

Equations

• UnrestrictedBooleanMul.N4.vectorWedgeFour u w i j k l m = u i * w j k l m + u j * w i k l m + u k * w i j l m + u l * w i j k m + u m * w i j k l

theorem UnrestrictedBooleanMul.N4.wedgeThreeTwo_vectorWedgeTwo (u : LinearForm) (q c : TwoForm) : wedgeThreeTwo (vectorWedgeTwo u q) c = vectorWedgeFour u (wedgeTwo q c)

Associativity in the only exterior degrees needed by the feedback annihilator. Keeping the statement in coordinates makes it independent of a large general-purpose exterior-algebra construction.

theorem UnrestrictedBooleanMul.N4.wedgeThreeTwo_vectorWedgeTwo_eq_zero {u : LinearForm} {q c : TwoForm} (hqc : wedgeTwo q c = 0) : wedgeThreeTwo (vectorWedgeTwo u q) c = 0

theorem UnrestrictedBooleanMul.N4.wedgeTwo_add_right (q c d : TwoForm) : wedgeTwo q (c + d) = wedgeTwo q c + wedgeTwo q d

theorem UnrestrictedBooleanMul.N4.wedgeTwo_add_left (q c d : TwoForm) : wedgeTwo (q + c) d = wedgeTwo q d + wedgeTwo c d

theorem UnrestrictedBooleanMul.N4.wedge_decomposable_repeated_left (x y z : LinearForm) : wedgeTwo (vectorWedge x y) (vectorWedge x z) = 0

A two-plane wedges trivially with every decomposable two-form having a repeated factor from that plane.

theorem UnrestrictedBooleanMul.N4.wedge_decomposable_repeated_right (x y z : LinearForm) : wedgeTwo (vectorWedge x y) (vectorWedge z y) = 0

theorem UnrestrictedBooleanMul.N4.wedge_place_firstJet_zero (x u y v : LinearForm) : wedgeTwo (vectorWedge x y) (vectorWedge x v + vectorWedge u y) = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.wedgeTwo_self (q : TwoForm) : wedgeTwo q q = 0

def UnrestrictedBooleanMul.N4.placeA : Fin 3 → LinearForm

The three rational A-side place vectors: zero, one, infinity.

Equations

• UnrestrictedBooleanMul.N4.placeA = ![![1, 0, 0, 0, 0, 0, 0, 0], ![1, 1, 1, 1, 0, 0, 0, 0], ![0, 0, 0, 1, 0, 0, 0, 0]]

def UnrestrictedBooleanMul.N4.placeB : Fin 3 → LinearForm

The three rational B-side place vectors: zero, one, infinity.

Equations

• UnrestrictedBooleanMul.N4.placeB = ![![0, 0, 0, 0, 1, 0, 0, 0], ![0, 0, 0, 0, 1, 1, 1, 1], ![0, 0, 0, 0, 0, 0, 0, 1]]

def UnrestrictedBooleanMul.N4.rationalPlaceTwo (θ : Fin 3) : TwoForm

Exterior product of the two input evaluations at a rational place.

Equations

• UnrestrictedBooleanMul.N4.rationalPlaceTwo θ = UnrestrictedBooleanMul.N4.vectorWedge (UnrestrictedBooleanMul.N4.placeA θ) (UnrestrictedBooleanMul.N4.placeB θ)

def UnrestrictedBooleanMul.N4.rationalTwo (α : Fin 3 → F₂) : TwoForm

Linear combination of the two-forms of the three rational places.

Equations

• UnrestrictedBooleanMul.N4.rationalTwo α = ∑ θ : Fin 3, α θ • UnrestrictedBooleanMul.N4.rationalPlaceTwo θ

theorem UnrestrictedBooleanMul.N4.dependent_of_vectorWedge_zero {n : ℕ} (u v : Fin n → F₂) (h : ∀ (i j : Fin n), u i * v j + u j * v i = 0) : u = 0 ∨ v = 0 ∨ u = v

Ordinary vector dependence over F₂, derived algebraically from the vanishing of every 2 × 2 minor.

theorem UnrestrictedBooleanMul.N4.rational_wedge_coord_01 (α β : Fin 3 → F₂) : wedgeTwo (rationalTwo α) (rationalTwo β) 0 1 4 6 = α 0 * β 1 + α 1 * β 0

theorem UnrestrictedBooleanMul.N4.rational_wedge_coord_12 (α β : Fin 3 → F₂) : wedgeTwo (rationalTwo α) (rationalTwo β) 1 3 5 7 = α 1 * β 2 + α 2 * β 1

theorem UnrestrictedBooleanMul.N4.rational_wedge_coord_mid (α β : Fin 3 → F₂) : wedgeTwo (rationalTwo α) (rationalTwo β) 0 3 4 7 = α 0 * β 1 + α 1 * β 0 + (α 0 * β 2 + α 2 * β 0) + (α 1 * β 2 + α 2 * β 1)

theorem UnrestrictedBooleanMul.N4.rational_wedge_zero_dependent (α β : Fin 3 → F₂) (h : wedgeTwo (rationalTwo α) (rationalTwo β) = 0) : α = 0 ∨ β = 0 ∨ α = β

The three pair wedges of rational places are independent. Equivalently, two forms in their span have zero exterior product exactly when their coefficient vectors are dependent.