Remark 1: Base Field

For the remainder of this manuscript we will only consider vector spaces over the field $\mathbb{F}_2$. All tensor products, linear maps, and homology computations are taken over $\mathbb{F}_2$ unless stated otherwise.

Main Definitions

• 𝔽₂: abbreviation for ZMod 2, the field with two elements

Main Results

• 𝔽₂.field: ZMod 2 is a field
• 𝔽₂.charTwo: ZMod 2 has characteristic 2
• 𝔽₂.fintype: ZMod 2 is finite with cardinality 2
• 𝔽₂.neg_eq_self: in characteristic 2, negation is the identity
• 𝔽₂.add_self_eq_zero: in characteristic 2, a + a = 0

Base field definition

@[reducible, inline]

abbrev 𝔽₂ : Type

𝔽₂ is the field with two elements, ZMod 2. All vector spaces, tensor products, linear maps, and homology computations in this paper are over 𝔽₂.

Equations

• 𝔽₂ = ZMod 2

Field and finiteness instances

instance 𝔽₂.prime_two : Fact (Nat.Prime 2)

instance 𝔽₂.field : Field 𝔽₂

Equations

• 𝔽₂.field = ZMod.instField 2

instance 𝔽₂.fintype : Fintype 𝔽₂

Equations

• 𝔽₂.fintype = ZMod.fintype 2

instance 𝔽₂.charTwo : CharP 𝔽₂ 2

Basic properties of 𝔽₂ arithmetic

theorem 𝔽₂.card_eq : Fintype.card 𝔽₂ = 2

In 𝔽₂, the cardinality is 2.

theorem 𝔽₂.neg_eq_self (a : 𝔽₂) : -a = a

In 𝔽₂, every element equals its own negation.

theorem 𝔽₂.add_self_eq_zero (a : 𝔽₂) : a + a = 0

In 𝔽₂, a + a = 0 for all a.

theorem 𝔽₂.sub_eq_add (a b : 𝔽₂) : a - b = a + b

In 𝔽₂, subtraction equals addition.