Conversion between set-indexed block-like matrices and type-indexed block matrices

These conversions are used in 1-sum, 2-sum, and 3-sum of standard representations.

def Matrix.toMatrixUnionUnion {α : Type u_1} {β : Type u_2} {R : Type u_3} {T₁ T₂ : Set α} {S₁ S₂ : Set β} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(b : β) → Decidable (b ∈ S₁)] [(b : β) → Decidable (b ∈ S₂)] (A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) R) : Matrix (↑(T₁ ∪ T₂)) (↑(S₁ ∪ S₂)) R

Convert a block matrix to a matrix over set unions.

Equations

• A.toMatrixUnionUnion x✝ = (A ∘ Subtype.toSum) x✝ ∘ Subtype.toSum

theorem Matrix.toMatrixUnionUnion_transpose {α : Type u_1} {β : Type u_2} {R : Type u_3} {T₁ T₂ : Set α} {S₁ S₂ : Set β} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(b : β) → Decidable (b ∈ S₁)] [(b : β) → Decidable (b ∈ S₂)] (A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) R) : A.toMatrixUnionUnion.transpose = A.transpose.toMatrixUnionUnion

Transposing a converted matrix gives the same result as converting a transposed matrix.

theorem Matrix.IsTotallyUnimodular.toMatrixUnionUnion {α : Type u_1} {β : Type u_2} {R : Type u_3} {T₁ T₂ : Set α} {S₁ S₂ : Set β} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(b : β) → Decidable (b ∈ S₁)] [(b : β) → Decidable (b ∈ S₂)] [CommRing R] {A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) R} (hA : A.IsTotallyUnimodular) : A.toMatrixUnionUnion.IsTotallyUnimodular

A totally unimodular block matrix stays totally unimodular after converting to a matrix over set unions.

theorem Matrix.IsSigningOf.toMatrixUnionUnion {α : Type u_1} {β : Type u_2} {R : Type u_3} {T₁ T₂ : Set α} {S₁ S₂ : Set β} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(b : β) → Decidable (b ∈ S₁)] [(b : β) → Decidable (b ∈ S₂)] [LinearOrderedRing R] {A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) R} {U : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) Z2} (hAU : A.IsSigningOf U) : A.toMatrixUnionUnion.IsSigningOf U.toMatrixUnionUnion

A signing block matrix stays a signing of a matrix after converting both matrices to be indexed by set unions.

def Matrix.toMatrixElemElem {α : Type u_1} {β : Type u_2} {R : Type u_3} {T₁ T₂ : Set α} {S₁ S₂ : Set β} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(b : β) → Decidable (b ∈ S₁)] [(b : β) → Decidable (b ∈ S₂)] {T : Set α} {S : Set β} (A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) R) (hT : T = T₁ ∪ T₂) (hS : S = S₁ ∪ S₂) : Matrix (↑T) (↑S) R

Convert a block matrix to a matrix over set unions named as single indexing sets.

Equations

• A.toMatrixElemElem hT hS = ⋯ ▸ ⋯ ▸ A.toMatrixUnionUnion

theorem Matrix.toMatrixElemElem_apply {α : Type u_1} {β : Type u_2} {R : Type u_3} {T₁ T₂ : Set α} {S₁ S₂ : Set β} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(b : β) → Decidable (b ∈ S₁)] [(b : β) → Decidable (b ∈ S₂)] {T : Set α} {S : Set β} (A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) R) (hT : T = T₁ ∪ T₂) (hS : S = S₁ ∪ S₂) (i : ↑T) (j : ↑S) : A.toMatrixElemElem hT hS i j = A (hT ▸ i).toSum (hS ▸ j).toSum

Direct characterization of Matrix.toMatrixElemElem entries.

theorem Matrix.IsTotallyUnimodular.toMatrixElemElem {α : Type u_1} {β : Type u_2} {R : Type u_3} {T₁ T₂ : Set α} {S₁ S₂ : Set β} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(b : β) → Decidable (b ∈ S₁)] [(b : β) → Decidable (b ∈ S₂)] {T : Set α} {S : Set β} [CommRing R] {A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) R} (hA : A.IsTotallyUnimodular) (hT : T = T₁ ∪ T₂) (hS : S = S₁ ∪ S₂) : (A.toMatrixElemElem hT hS).IsTotallyUnimodular

A totally unimodular block matrix stays totally unimodular after converting to a matrix over set unions named as single indexing sets.

theorem Matrix.IsSigningOf.toMatrixElemElem {α : Type u_1} {β : Type u_2} {R : Type u_3} {T₁ T₂ : Set α} {S₁ S₂ : Set β} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(b : β) → Decidable (b ∈ S₁)] [(b : β) → Decidable (b ∈ S₂)] {T : Set α} {S : Set β} [LinearOrderedRing R] {A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) R} {U : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) Z2} (hAU : A.IsSigningOf U) (hT : T = T₁ ∪ T₂) (hS : S = S₁ ∪ S₂) : (A.toMatrixElemElem hT hS).IsSigningOf (U.toMatrixElemElem hT hS)

A signing block matrix stays a signing of a matrix after converting both matrices to be indexed by set unions named as single indexing sets.