@[reducible, inline]

abbrev ZMAT : Type

A bunch of definitions and lemmas used in defining the Sato subgroup.

Equations

• ZMAT = Matrix (Fin 3) (Fin 3) ℤ

@[reducible, inline]

abbrev Z3_raw : Type

Equations

• Z3_raw = (Fin 3 → ℤ)

def to_MAT (A : ZMAT) : MAT

Equations

• to_MAT A = Matrix.map A ⇑(Int.castRingHom ℝ)

theorem to_MAT_inj : Function.Injective to_MAT

theorem to_MAT_transp {A : Matrix (Fin 3) (Fin 3) ℤ} : to_MAT A.transpose = Matrix.transpose (to_MAT A)

theorem to_MAT_mul {A B : ZMAT} : to_MAT (A * B) = to_MAT A * to_MAT B

theorem to_MAT_prod (L : List ZMAT) : to_MAT L.prod = (List.map to_MAT L).prod

theorem to_MAT_pow {A : ZMAT} {N : ℕ} : to_MAT (A ^ N) = to_MAT A ^ N

def mod7_Z (v : Z3_raw) : Z3_raw

Equations

• mod7_Z v = ![v 0 % 7, v 1 % 7, v 2 % 7]

theorem mod7_Z_additive (v u : Z3_raw) : mod7_Z (v + u) = mod7_Z (mod7_Z v + mod7_Z u)

theorem mod7_Z_idempotent (v : Z3_raw) : mod7_Z (mod7_Z v) = mod7_Z v

theorem mod_lemma_Z (A : ZMAT) (v : Z3_raw) : mod7_Z (Matrix.mulVec A (mod7_Z v)) = mod7_Z (Matrix.mulVec A v)

theorem drop_eq_last {α : Type u_1} (M : ℕ) (L : List α) {X : α} : L.length = M + 1 ∧ L.getLast? = some X → List.drop M L = [X]

theorem diagonal_const_comm (d : ℝ) (k : ℕ) (M : MAT) : (Matrix.diagonal fun (x : Fin 3) => d) ^ k * M = M * (Matrix.diagonal fun (x : Fin 3) => d) ^ k

theorem zip_lemma (N : ℕ) (mats : List MAT) (d : ℝ) : mats.length = N → (Matrix.diagonal fun (x : Fin 3) => d) ^ N * mats.prod = (List.map (fun (M : MAT) => (Matrix.diagonal fun (x : Fin 3) => d) * M) mats).prod

def sev_mat_Z : Matrix (Fin 3) (Fin 3) ℤ

Equations

• sev_mat_Z = Matrix.diagonal fun (x : Fin 3) => 7

def sev_mat : MAT

Equations

• sev_mat = to_MAT sev_mat_Z

noncomputable def seventh_mat : Matrix (Fin 3) (Fin 3) ℝ

Equations

• seventh_mat = Matrix.diagonal fun (x : Fin 3) => 7⁻¹

theorem sev_mat_Z_mod_is_zero_lemma (N : ℕ) : N ≠ 0 → mod7_Z ((sev_mat_Z ^ N).col 0) = 0

theorem inv7lemma {N : ℕ} : sev_mat ^ N * seventh_mat ^ N = 1

theorem sevsevlem : (7⁻¹ • 7⁻¹ • fun (x : Fin 3) => 49) = fun (x : Fin 3) => 1

theorem isreduced_of_take_of_reduced {α : Type u} (L : List (α × Bool)) (n : ℕ) : FreeGroup.IsReduced L → FreeGroup.IsReduced (List.take n L)

The entire remainder of the module is devoted to the proof of a -- fact used in the definition of the Sato subgroup: -- That wiithout loss of generality we can assume a member of the -- kernel ends in σ lemma wolog_zero {G : Type} [Group G] (h : FG2 →* G) (a : FG2) : (a ≠ 1) ∧ (h a = 1) → ∃a2 : FG2, (a2 ≠ 1) ∧ (h a2 = 1) ∧ (FreeGroup.toWord a2).getLast? = some (0, true)

theorem isreduced_of_drop_of_reduced {α : Type u} (L : List (α × Bool)) (n : ℕ) : FreeGroup.IsReduced L → FreeGroup.IsReduced (List.drop n L)

theorem isreduced_of_append_of_reduced_mismatching_boundary {α : Type u} {L M : List (α × Bool)} (p1 p2 : α × Bool) (pl : L.getLast? = some p1) (ph : M.head? = some p2) : FreeGroup.IsReduced L ∧ FreeGroup.IsReduced M ∧ (p1.1 = p2.1 → p1.2 = p2.2) → FreeGroup.IsReduced (L ++ M)

theorem isReduced_of_replicate {a : chartype} {k : ℕ} : FreeGroup.IsReduced (List.replicate k a)

theorem isReduced_of_invRev_of_isReduced {w : List chartype} : FreeGroup.IsReduced w → FreeGroup.IsReduced (FreeGroup.invRev w)

theorem reduce_invRev_right_cancel {L : List chartype} : FreeGroup.reduce (L ++ FreeGroup.invRev L) = []

def TailPred_f (w : List chartype) (n : ℕ) : Bool

Equations

• TailPred_f w n = (decide (n ≤ w.length) && decide (List.drop (w.length - n) w = List.replicate n (0, false)))

@[reducible, inline]

abbrev lSet_type_f (w : List chartype) : Type

Equations

• lSet_type_f w = Fin (w.length + 1)

def S_f (w : List chartype) : Finset (lSet_type_f w)

Equations

• S_f w = {n : lSet_type_f w | TailPred_f w ↑n = true}

theorem TP_holds_of_zero_f (w : List chartype) : TailPred_f w 0 = true

theorem ne_S_f (w : List chartype) : (S_f w).Nonempty

def max_fin_f (w : List chartype) : lSet_type_f w

Equations

• max_fin_f w = (S_f w).max' ⋯

def n_trail_sinv_f (w : List chartype) : ℤ

Equations

• n_trail_sinv_f w = ↑↑(max_fin_f w)

def trailing_as_nat_f (w : List chartype) : ℕ

Equations

• trailing_as_nat_f w = (n_trail_sinv_f w).toNat

def leading_s_as_nat_f (w : List chartype) : ℕ

Equations

• leading_s_as_nat_f w = trailing_as_nat_f (FreeGroup.invRev w)

def leading_others_as_nat_f (w : List chartype) : ℕ

Equations

• leading_others_as_nat_f w = (↑w.length - n_trail_sinv_f w).toNat

def all_sinv_f (w : List chartype) : Prop

Equations

• all_sinv_f w = (n_trail_sinv_f w = ↑w.length)

def last_is_sigma_f (w : List chartype) : Prop

Equations

• last_is_sigma_f w = (w.getLast? = some (0, true))

def all_s_f (w : List chartype) : Prop

Equations

• all_s_f w = (w = List.replicate w.length (0, true))

def first_is_sinv_f (w : List chartype) : Prop

Equations

• first_is_sinv_f w = (w.head? = some (0, false))

theorem if_not_all_sinv_w (w : List chartype) : w ≠ [] ∧ FreeGroup.IsReduced w ∧ ¬all_sinv_f w ∧ ¬last_is_sigma_f w → ∃ (wc : List chartype), w = wc ++ List.replicate (trailing_as_nat_f w) (0, false) ∧ FreeGroup.IsReduced wc ∧ ∃ (b : Bool), wc.getLast? = some (1, b)

theorem all_sinv_equiv (w : List chartype) : all_sinv_f w → w = List.replicate w.length (0, false)

theorem leading_trailing {w : List (Fin 2 × Bool)} : trailing_as_nat_f (FreeGroup.invRev w) = leading_s_as_nat_f w

theorem collapse_replics_1 (nf nt : ℕ) : FreeGroup.reduce (List.replicate nf (σchar, false) ++ List.replicate nt (σchar, true)) = if nf = nt then [] else if nf > nt then List.replicate (nf - nt) (σchar, false) else List.replicate (nt - nf) (σchar, true)

theorem collapse_replics_2 (n : ℕ) : FreeGroup.reduce (List.replicate n (σchar, false) ++ List.replicate (n + 1) (σchar, true)) = [(σchar, true)]

theorem if_not_all_init_s_w (w : List chartype) : w ≠ [] ∧ FreeGroup.IsReduced w ∧ ¬all_s_f w ∧ ¬first_is_sinv_f w → ∃ (wc : List chartype), w = List.replicate (leading_s_as_nat_f w) (0, true) ++ wc ∧ FreeGroup.IsReduced wc ∧ ∃ (b : Bool), wc.head? = some (1, b)

theorem wolog_zero {G : Type} [Group G] (h : FG2 →* G) (a : FG2) : a ≠ 1 ∧ h a = 1 → ∃ (a2 : FG2), a2 ≠ 1 ∧ h a2 = 1 ∧ (FreeGroup.toWord a2).getLast? = some (0, true)