Abstract Binary Tower Core

Core definitions and existence data for the abstract binary tower construction.

structure BinaryTower.BinaryTowerResult (F : Type u_1) (k : ℕ) : Type u_1

• vec : List.Vector F (k + 1)
• instField : Field F
• instFintype : Fintype F
• specialElement : F
• specialElementNeZero : NeZero self.specialElement
• firstElementOfVecIsSpecialElement [_root_.Inhabited F] : (↑self.vec).headI = self.specialElement
• instIrreduciblePoly : Irreducible (definingPoly self.specialElement)
• sumZeroIffEq (x y : F) : x + y = 0 ↔ x = y
• fieldFintypeCard : Fintype.card F = 2 ^ 2 ^ k
• traceMapEvalAtRootsIs1 : TraceMapProperty F self.specialElement k

structure BinaryTower.BinaryTowerInductiveStepResult (k : ℕ) (prevBTField : Type u_1) (prevBTResult : BinaryTowerResult prevBTField k) [instPrevBTFieldIsField : Field prevBTField] (prevPoly : Polynomial prevBTField) (F : Type u_1) : Type u_1

• binaryTowerResult : BinaryTowerResult F (k + 1)
• eq_adjoin : F = AdjoinRoot prevPoly
• u_is_root : ⋯.mp self.binaryTowerResult.specialElement = AdjoinRoot.root prevPoly
• eval_defining_poly_at_root : ⋯.mp self.binaryTowerResult.specialElement ^ 2 + ⋯.mp self.binaryTowerResult.specialElement * (AdjoinRoot.of prevPoly) prevBTResult.specialElement + 1 = 0

noncomputable def BinaryTower.binary_tower_inductive_step (k : ℕ) (prevBTField : Type u_1) [Field prevBTField] (prevBTResult : BinaryTowerResult prevBTField k) : (F : Type u_1) ×' BinaryTowerInductiveStepResult k prevBTField prevBTResult (definingPoly prevBTResult.specialElement) F

def BinaryTower.BinaryTowerAux (k : ℕ) : (F : Type) ×' BinaryTowerResult F k

def BinaryTower.BTField (k : ℕ) : Type

theorem BinaryTower.BTField_is_BTFieldAux (k : ℕ) : BTField k = (BinaryTowerAux k).fst

@[implicit_reducible]

noncomputable instance BinaryTower.BTFieldIsField (k : ℕ) : Field (BTField k)

@[implicit_reducible]

noncomputable instance BinaryTower.CommRing (k : ℕ) : _root_.CommRing (BTField k)

instance BinaryTower.Nontrivial (k : ℕ) : _root_.Nontrivial (BTField k)

@[implicit_reducible]

noncomputable instance BinaryTower.Inhabited (k : ℕ) : _root_.Inhabited (BTField k)

@[implicit_reducible]

noncomputable instance BinaryTower.instInhabitedFstBinaryTowerResultBinaryTowerAux {k : ℕ} : _root_.Inhabited (BinaryTowerAux k).fst

instance BinaryTower.BTFieldNeZero1 (k : ℕ) : NeZero 1

@[implicit_reducible]

noncomputable instance BinaryTower.BTField_Fintype (k : ℕ) : Fintype (BTField k)

@[simp]

def BinaryTower.BTFieldCard (k : ℕ) : Fintype.card (BTField k) = 2 ^ 2 ^ k

instance BinaryTower.BTFieldIsDomain (k : ℕ) : IsDomain (BTField k)

instance BinaryTower.BTFieldNoZeroDiv (k : ℕ) : NoZeroDivisors (BTField k)

@[simp]

def BinaryTower.sumZeroIffEq (k : ℕ) (x y : BTField k) : x + y = 0 ↔ x = y

instance BinaryTower.BTFieldChar2 (k : ℕ) : CharP (BTField k) 2

@[simp]

theorem BinaryTower.BTField_0_is_GF_2 : BTField 0 = (GF(2))

noncomputable def BinaryTower.list (k : ℕ) : List.Vector (BTField k) (k + 1)

noncomputable def BinaryTower.Z (k : ℕ) : BTField k

Z k is the generator of BTField k

instance BinaryTower.instNeZeroBTFieldZ {k : ℕ} : NeZero (Z k)

noncomputable def BinaryTower.poly (k : ℕ) : Polynomial (BTField k)

theorem BinaryTower.poly_natDegree_eq_2 (k : ℕ) : (poly k).natDegree = 2

theorem BinaryTower.BTField.cast_BTField_eq (k m : ℕ) (h_eq : k = m) : BTField k = BTField m

theorem BinaryTower.BTField.cast_mul (m n : ℕ) {x y : BTField m} (h_eq : m = n) : cast ⋯ (x * y) = cast ⋯ x * cast ⋯ y

noncomputable def BinaryTower.𝕏 (k : ℕ) : BTField (k + 1)

adjoined root of poly k, generator of successor field BTField (k+1)

theorem BinaryTower.BTField_succ_eq_adjoinRoot (k : ℕ) : AdjoinRoot (poly k) = BTField (k + 1)

@[implicit_reducible]

instance BinaryTower.coe_field_adjoinRoot (k : ℕ) : Coe (AdjoinRoot (poly k)) (BTField (k + 1))

@[simp]

theorem BinaryTower.Z_succ_eq_adjointRoot_root (k : ℕ) : Z (k + 1) = AdjoinRoot.root (poly k)

theorem BinaryTower.list_0 : list 0 = 1 ::ᵥ List.Vector.nil

@[simp]

theorem BinaryTower.list_eq (k : ℕ) : list (k + 1) = Z (k + 1) ::ᵥ List.Vector.map (⇑(AdjoinRoot.of (poly k))) (list k)

@[simp]

theorem BinaryTower.eval_poly_at_root (k : ℕ) : Z (k + 1) ^ 2 + Z (k + 1) * ⋯.mp ((AdjoinRoot.of (poly k)) (Z k)) + 1 = 0

@[simp]

theorem BinaryTower.poly_form (k : ℕ) : poly k = Polynomial.X ^ 2 + (Polynomial.C (Z k) * Polynomial.X + 1)

@[simp]

theorem BinaryTower.eval_mapped_poly_at_root (k : ℕ) : Polynomial.eval₂ (AdjoinRoot.of (poly k)) (Z (k + 1)) (poly k) = 0

@[simp]

theorem BinaryTower.list_length (k : ℕ) : (list k).length = k + 1

@[simp]

theorem BinaryTower.list_nonempty (k : ℕ) : ↑(list k) ≠ []

instance BinaryTower.polyIrreducibleFact (n : ℕ) : Fact (Irreducible (poly n))

theorem BinaryTower.poly_ne_zero (n : ℕ) : poly n ≠ 0