Matrix characteristic polynomial helpers

This file restores upstream helper lemmas for block diagonal characteristic polynomials.

def Equiv.prodSubtypeSndEquivProdSubtype {α : Type u_2} {β : Type u_3} {p : β → Prop} : { s : α × β // p s.2 } ≃ α × { b : β // p b }

A subtype of a product that depends only on the second component.

Equations

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

@[simp]

theorem Equiv.prodSubtypeSndEquivProdSubtype_symm_apply_coe {α : Type u_2} {β : Type u_3} {p : β → Prop} (x : α × { b : β // p b }) : ↑(prodSubtypeSndEquivProdSubtype.symm x) = (x.1, ↑x.2)

@[simp]

theorem Equiv.prodSubtypeSndEquivProdSubtype_apply {α : Type u_2} {β : Type u_3} {p : β → Prop} (x : { s : α × β // p s.2 }) : prodSubtypeSndEquivProdSubtype x = ((↑x).1, ⟨(↑x).2, ⋯⟩)

def thing' {α : Type u_2} {β : Type u_3} (b : β) : { i : α × β // i.2 = b } ≃ α

The fiber of a product projection over a fixed second coordinate.

Equations

• thing' b = Equiv.prodSubtypeSndEquivProdSubtype.trans (Equiv.prodUnique α { i : β // i = b })

@[simp]

theorem thing'_symm_apply_coe {α : Type u_2} {β : Type u_3} (b : β) (a✝ : α) : ↑((thing' b).symm a✝) = (a✝, ↑default)

@[simp]

theorem thing'_apply {α : Type u_2} {β : Type u_3} (b : β) (a✝ : { s : α × β // s.2 = b }) : (thing' b) a✝ = (↑a✝).1

theorem Matrix.blockDiagonal_toSquareBlock {F : Type u_1} [Field F] {r : ℕ} {n : Type u_2} (A : Fin r → Matrix n n F) {i : Fin r} : (blockDiagonal A).toSquareBlock Prod.snd i = (reindex (thing' i).symm (thing' i).symm) (A i)

theorem Matrix.blockDiagonal_charpoly_aux {F : Type u_1} [Field F] {r : ℕ} {n : Type u_2} [DecidableEq n] [Fintype n] (A : Fin r → Matrix n n F) {i : Fin r} : ((blockDiagonal A).toSquareBlock Prod.snd i).charpoly = (A i).charpoly

theorem Matrix.blockDiagonal_charpoly {F : Type u_1} [Field F] {r : ℕ} {n : Type u_2} [DecidableEq n] [Fintype n] (A : Fin r → Matrix n n F) : (blockDiagonal A).charpoly = ∏ i : Fin r, (A i).charpoly

theorem Matrix.blockDiagonal_const_charpoly {F : Type u_1} [Field F] (r n : ℕ) (A : Matrix (Fin n) (Fin n) F) : (blockDiagonal fun (x : Fin r) => A).charpoly = A.charpoly ^ r

theorem Matrix.reindex_diagonal_charpoly {F : Type u_1} [Field F] (r n m : ℕ) (eq : m = r * n) (A : Matrix (Fin n) (Fin n) F) : ((reindexAlgEquiv F F (finProdFinEquiv.trans (finCongr ⋯))) ((blockDiagonalRingHom (Fin n) (Fin r) F) fun (x : Fin r) => A)).charpoly = A.charpoly ^ r