@[reducible, inline]

abbrev Zn (n : ℕ) [NeZero n] : Type

Equations

• Zn n = (Fin n → ℤ)

@[reducible, inline]

abbrev Zn_dual (n : ℕ) [NeZero n] : Type

Equations

• Zn_dual n = Module.Dual ℤ (Zn n)

def e_transpose {n : ℕ} [NeZero n] (k : Fin n) : Zn_dual n

Equations

• e_transpose k = { toFun := fun (t : Zn n) => t k, map_add' := ⋯, map_smul' := ⋯ }

def Ae {n : ℕ} [NeZero n] (k : Fin n) : Zn n

Equations

• Ae k t = if t = k then 2 else if ↑k + 1 = ↑t ∨ ↑t + 1 = ↑k then -1 else 0

structure SignedInterval (n : ℕ) : Type

• i : Fin n
• j : Fin n
• hij : self.i ≤ self.j
• ε : Bool

def SignedInterval.sign {n : ℕ} (J : SignedInterval n) : ℤ

Equations

• J.sign = if J.ε = true then 1 else -1

def α {n : ℕ} [NeZero n] (J : SignedInterval n) : Zn n

Equations

• α J = J.sign • ∑ k ∈ Finset.Icc J.i J.j, Ae k

def α_dual {n : ℕ} [NeZero n] (J : SignedInterval n) : Zn_dual n

Equations

• α_dual J = J.sign • ∑ k ∈ Finset.Icc J.i J.j, e_transpose k

def s {n : ℕ} [NeZero n] (J K : SignedInterval n) : SignedInterval n

The reflection permutation for signed intervals. For positive intervals J = [i,j] and K = [k,l]:

• If (i,j) = (k,l): returns -[k,l]
• If i = l+1: returns [k,j] (merge: K then J)
• If k = j+1: returns [i,l] (merge: J then K)
• If i = k, j > l: returns -[l+1, j]
• If i = k, j < l: returns [j+1, l]
• If i < k, j = l: returns -[i, k-1]
• If i > k, j = l: returns [k, i-1]
• Otherwise: returns [k,l] Then s_{-J} = s_J and s_J(-K) = -s_J(K).

Equations

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

@[reducible, inline]

noncomputable abbrev Zn_pairing (n : ℕ) [NeZero n] : Zn n →ₗ[ℤ] Zn_dual n →ₗ[ℤ] ℤ

Equations

• Zn_pairing n = Module.Dual.eval ℤ (Zn n)

theorem SignedInterval.ext' {n : ℕ} {J K : SignedInterval n} (hi : J.i = K.i) (hj : J.j = K.j) (hε : J.ε = K.ε) : J = K

theorem SignedInterval.ext'_iff {n : ℕ} {J K : SignedInterval n} : J = K ↔ J.i = K.i ∧ J.j = K.j ∧ J.ε = K.ε

theorem s_involutive {n : ℕ} [NeZero n] (J K : SignedInterval n) : s J (s J K) = K

theorem Ae_sum_eq {n : ℕ} [NeZero n] (p q : Fin n) (hpq : p ≤ q) (t : Fin n) : (∑ u ∈ Finset.Icc p q, Ae u) t = (((if t = p then 1 else 0) + if t = q then 1 else 0) - if ↑t + 1 = ↑p then 1 else 0) - if ↑q + 1 = ↑t then 1 else 0

theorem α_eval {n : ℕ} [NeZero n] (J : SignedInterval n) (t : Fin n) : α J t = J.sign * ((((if t = J.i then 1 else 0) + if t = J.j then 1 else 0) - if ↑t + 1 = ↑J.i then 1 else 0) - if ↑J.j + 1 = ↑t then 1 else 0)

theorem α_dual_eval {n : ℕ} [NeZero n] (J : SignedInterval n) (f : Zn n) : (α_dual J) f = J.sign * ∑ v ∈ Finset.Icc J.i J.j, f v

theorem pairing_formula {n : ℕ} [NeZero n] (J K : SignedInterval n) : ((Zn_pairing n) (α K)) (α_dual J) = J.sign * K.sign * ((((if J.i = K.i then 1 else 0) + if J.j = K.j then 1 else 0) - if ↑J.i = ↑K.j + 1 then 1 else 0) - if ↑K.i = ↑J.j + 1 then 1 else 0)

theorem pairing_self {n : ℕ} [NeZero n] (J : SignedInterval n) : ((Zn_pairing n) (α J)) (α_dual J) = 2

theorem pairing_eq_two_iff_eq {n : ℕ} [NeZero n] (J K : SignedInterval n) : ((Zn_pairing n) (α K)) (α_dual J) = 2 ↔ K = J

theorem α_injective {n : ℕ} [NeZero n] : Function.Injective α

theorem α_dual_injective {n : ℕ} [NeZero n] : Function.Injective α_dual

theorem root_coroot_two' {n : ℕ} [NeZero n] (J : SignedInterval n) : ((Zn_pairing n) (α J)) (α_dual J) = 2

theorem reflectionPerm_root_eval {n : ℕ} [NeZero n] (J K : SignedInterval n) (t : Fin n) : (α K - ((Zn_pairing n) (α K)) (α_dual J) • α J) t = α (s J K) t

theorem reflectionPerm_root' {n : ℕ} [NeZero n] (J K : SignedInterval n) : α K - ((Zn_pairing n) (α K)) (α_dual J) • α J = α (s J K)

theorem pairing_symm {n : ℕ} [NeZero n] (J K : SignedInterval n) : ((Zn_pairing n) (α J)) (α_dual K) = ((Zn_pairing n) (α K)) (α_dual J)

theorem reflectionPerm_coroot_single {n : ℕ} [NeZero n] (J K : SignedInterval n) (t : Fin n) : ((α_dual K - ((Zn_pairing n) (α J)) (α_dual K) • α_dual J) ∘ₗ LinearMap.single ℤ (fun (x : Fin n) => ℤ) t) 1 = (α_dual (s J K) ∘ₗ LinearMap.single ℤ (fun (x : Fin n) => ℤ) t) 1

theorem reflectionPerm_coroot' {n : ℕ} [NeZero n] (J K : SignedInterval n) : α_dual K - ((Zn_pairing n) (α J)) (α_dual K) • α_dual J = α_dual (s J K)

noncomputable def An (n : ℕ) [NeZero n] : RootPairing (SignedInterval n) ℤ (Zn n) (Zn_dual n)

Equations

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

@[implicit_reducible]

instance finite (n : ℕ) [NeZero n] : Fintype (SignedInterval n)

Equations

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

theorem An_is_finite (n : ℕ) [NeZero n] : Finite (SignedInterval n)

theorem An_is_reduced (n : ℕ) [NeZero n] : (An n).IsReduced

theorem An_is_crystallographic (n : ℕ) [NeZero n] : (An n).IsCrystallographic