Adjoining a pendant vertex to a matrix

This file defines the matrix obtained by adjoining one further vertex, joined by a single edge to a chosen vertex of an integer matrix. The construction is independent of finite type and is used to assemble Cartan matrices of diagrams with a pendant vertex.

Main definitions

• TauCeti.adjoinPendant: adjoin a new vertex, indexed by none, to a chosen vertex of a matrix.

Main results

• TauCeti.adjoinPendant_submatrix_some: deleting the new vertex recovers the original matrix.
• TauCeti.adjoinPendant_transpose: adjoining a pendant vertex commutes with transposition.
• TauCeti.adjoinPendant_diag and TauCeti.adjoinPendant_apply_le_zero_of_ne: adjoining a pendant vertex preserves the diagonal and off-diagonal sign conditions of a generalized Cartan matrix.

def TauCeti.adjoinPendant {α : Type u_1} [DecidableEq α] (M : Matrix α α ℤ) (i : α) : Matrix (Option α) (Option α) ℤ

Adjoining a pendant vertex. The diagram of TauCeti.adjoinPendant M i is the diagram of M together with one further vertex, written none, joined to the vertex i by a single edge and to nothing else.

Equations

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

@[simp]

theorem TauCeti.adjoinPendant_none_none {α : Type u_1} [DecidableEq α] {M : Matrix α α ℤ} {i : α} : adjoinPendant M i none none = 2

@[simp]

theorem TauCeti.adjoinPendant_none_some {α : Type u_1} [DecidableEq α] {M : Matrix α α ℤ} {i : α} (j : α) : adjoinPendant M i none (some j) = if j = i then -1 else 0

The pendant vertex is joined to i alone.

@[simp]

theorem TauCeti.adjoinPendant_some_none {α : Type u_1} [DecidableEq α] {M : Matrix α α ℤ} {i : α} (j : α) : adjoinPendant M i (some j) none = if j = i then -1 else 0

The pendant vertex is joined to i alone.

@[simp]

theorem TauCeti.adjoinPendant_some_some {α : Type u_1} [DecidableEq α] {M : Matrix α α ℤ} {i : α} (j k : α) : adjoinPendant M i (some j) (some k) = M j k

Adjoining a vertex changes no entry of the original matrix.

@[simp]

theorem TauCeti.adjoinPendant_submatrix_some {α : Type u_1} [DecidableEq α] {M : Matrix α α ℤ} {i : α} : (adjoinPendant M i).submatrix some some = M

Deleting the pendant vertex again recovers the original matrix.

@[simp]

theorem TauCeti.adjoinPendant_transpose {α : Type u_1} [DecidableEq α] {M : Matrix α α ℤ} {i : α} : (adjoinPendant M i).transpose = adjoinPendant M.transpose i

The pendant edge is a single edge, so transposition leaves it alone and reverses only the edges of M.

theorem TauCeti.adjoinPendant_diag {α : Type u_1} [DecidableEq α] {M : Matrix α α ℤ} {i : α} (hM : ∀ (j : α), M j j = 2) (v : Option α) : adjoinPendant M i v v = 2

Adjoining a pendant vertex keeps the diagonal entries equal to 2, as a generalized Cartan matrix needs them.

theorem TauCeti.adjoinPendant_apply_le_zero_of_ne {α : Type u_1} [DecidableEq α] {M : Matrix α α ℤ} {i : α} (hM : ∀ (j k : α), j ≠ k → M j k ≤ 0) {v w : Option α} (hvw : v ≠ w) : adjoinPendant M i v w ≤ 0

Adjoining a pendant vertex keeps the off-diagonal entries nonpositive.