This file provides notation used in the project and conversions between set-theoretical and type-theoretical definitions.

@[reducible, inline]

abbrev Z2 : Type

The finite field on two elements; write Z2 for "value" type but Fin 2 for "indexing" type.

Equations

• Z2 = ZMod 2

def «term_ᕃ_» : Lean.TrailingParserDescr

Roughly speaking a ᕃ A is A ∪ {a}.

Equations

• «term_ᕃ_» = Lean.ParserDescr.trailingNode `term_ᕃ_ 66 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᕃ ") (Lean.ParserDescr.cat `term 66))

def «term_⫗_» : Lean.TrailingParserDescr

Writing X ⫗ Y is slightly more general than writing X ∩ Y = ∅.

Equations

• «term_⫗_» = Lean.ParserDescr.trailingNode `term_⫗_ 61 62 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⫗ ") (Lean.ParserDescr.cat `term 62))

def HasSubset.Subset.elem {α : Type u_1} {X : Set α} {Y : Set α} (hXY : X ⊆ Y) (x : ↑X) : ↑Y

Given X ⊆ Y cast an element of X as an element of Y.

Equations

• hXY.elem x = ⟨↑x, ⋯⟩

def Subtype.toSum {α : Type u_1} {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (i : ↑(X ∪ Y)) : ↑X ⊕ ↑Y

Convert (X ∪ Y).Elem to X.Elem ⊕ Y.Elem.

Equations

• Subtype.toSum i = if hiX : ↑i ∈ X then Sum.inl ⟨↑i, hiX⟩ else if hiY : ↑i ∈ Y then Sum.inr ⟨↑i, hiY⟩ else ⋯.elim

def Sum.toUnion {α : Type u_1} {X : Set α} {Y : Set α} (i : ↑X ⊕ ↑Y) : ↑(X ∪ Y)

Convert X.Elem ⊕ Y.Elem to (X ∪ Y).Elem.

Equations

• i.toUnion = Sum.casesOn i ⋯.elem ⋯.elem

theorem toSum_toUnion {α : Type u_1} {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (i : ↑(X ∪ Y)) : (Subtype.toSum i).toUnion = i

Converting (X ∪ Y).Elem to X.Elem ⊕ Y.Elem and back to (X ∪ Y).Elem gives the original element.

theorem toUnion_toSum {α : Type u_1} {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (hXY : X ⫗ Y) (i : ↑X ⊕ ↑Y) : Subtype.toSum i.toUnion = i

Converting X.Elem ⊕ Y.Elem to (X ∪ Y).Elem and back to X.Elem ⊕ Y.Elem gives the original element, assuming that X and Y are disjoint.

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

Convert a block matrix to a matrix over set unions.

Equations

• C.toMatrixUnionUnion x = (C ∘ Subtype.toSum) x ∘ Subtype.toSum

def Matrix.toMatrixSumSum {α : Type u_1} {T₁ : Set α} {T₂ : Set α} {S₁ : Set α} {S₂ : Set α} {β : Type u_2} (C : Matrix (↑(T₁ ∪ T₂)) (↑(S₁ ∪ S₂)) β) : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β

Convert a matrix over set unions to a block matrix.

Equations

• C.toMatrixSumSum x = (C ∘ Sum.toUnion) x ∘ Sum.toUnion

theorem toMatrixUnionUnion_toMatrixSumSum {α : Type u_1} {T₁ : Set α} {T₂ : Set α} {S₁ : Set α} {S₂ : Set α} {β : Type u_2} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] (hT : T₁ ⫗ T₂) (hS : S₁ ⫗ S₂) (C : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β) : C.toMatrixUnionUnion.toMatrixSumSum = C

Converting a block matrix to a matrix over set unions and back to a block matrix gives the original matrix, assuming that both said unions are disjoint.

theorem toMatrixSumSum_toMatrixUnionUnion {α : Type u_1} {T₁ : Set α} {T₂ : Set α} {S₁ : Set α} {S₂ : Set α} {β : Type u_2} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] (C : Matrix (↑(T₁ ∪ T₂)) (↑(S₁ ∪ S₂)) β) : C.toMatrixSumSum.toMatrixUnionUnion = C

Converting a matrix over set unions to a block matrix and back to a matrix over set unions gives the original matrix.

theorem Matrix.TU.toMatrixUnionUnion {α : Type u_1} {T₁ : Set α} {T₂ : Set α} {S₁ : Set α} {S₂ : Set α} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] {C : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) ℚ} (hC : C.TU) : C.toMatrixUnionUnion.TU

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