Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore: renaming all Column to Col #19825

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - chore: renaming all Column to Col #19825

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
358766c
chore: Matrix.fromCols, Matrix.updateCol, Matrix.toCol
madvorak Dec 9, 2024
501d14a
Update Mathlib/Data/Matrix/ColumnRowPartitioned.lean
madvorak Dec 9, 2024
89e821f
deprecated
madvorak Dec 9, 2024
809417d
deprecated
madvorak Dec 10, 2024
48358f8
originally there was a typo, so we need to preserve
madvorak Dec 10, 2024
d9839d9
fix
madvorak Dec 11, 2024
35c77c8
upDate
madvorak Dec 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
110 changes: 55 additions & 55 deletions Mathlib/Data/Matrix/ColumnRowPartitioned.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import Mathlib.LinearAlgebra.Matrix.NonsingularInverse

This file provides the basic definitions of matrices composed from columns and rows.
The concatenation of two matrices with the same row indices can be expressed as
`A = fromColumns A₁ A₂` the concatenation of two matrices with the same column indices
`A = fromCols A₁ A₂` the concatenation of two matrices with the same column indices
can be expressed as `B = fromRows B₁ B₂`.

We then provide a few lemmas that deal with the products of these with each other and
Expand All @@ -34,14 +34,14 @@ def fromRows (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) : Matrix (m₁

/-- Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a
bigger matrix indexed by [m × (n₁ ⊕ n₂)] -/
def fromColumns (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) : Matrix m (n₁ ⊕ n₂) R :=
def fromCols (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) : Matrix m (n₁ ⊕ n₂) R :=
kim-em marked this conversation as resolved.
Show resolved Hide resolved
of fun i => Sum.elim (B₁ i) (B₂ i)

/-- Given a column partitioned matrix extract the first column -/
def toColumns₁ (A : Matrix m (n₁ ⊕ n₂) R) : Matrix m n₁ R := of fun i j => (A i (Sum.inl j))
def toCols₁ (A : Matrix m (n₁ ⊕ n₂) R) : Matrix m n₁ R := of fun i j => (A i (Sum.inl j))

/-- Given a column partitioned matrix extract the second column -/
def toColumns₂ (A : Matrix m (n₁ ⊕ n₂) R) : Matrix m n₂ R := of fun i j => (A i (Sum.inr j))
def toCols₂ (A : Matrix m (n₁ ⊕ n₂) R) : Matrix m n₂ R := of fun i j => (A i (Sum.inr j))

/-- Given a row partitioned matrix extract the first row -/
def toRows₁ (A : Matrix (m₁ ⊕ m₂) n R) : Matrix m₁ n R := of fun i j => (A (Sum.inl i) j)
Expand All @@ -58,12 +58,12 @@ lemma fromRows_apply_inr (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i :
(fromRows A₁ A₂) (Sum.inr i) j = A₂ i j := rfl

@[simp]
lemma fromColumns_apply_inl (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₁) :
(fromColumns A₁ A₂) i (Sum.inl j) = A₁ i j := rfl
lemma fromCols_apply_inl (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₁) :
(fromCols A₁ A₂) i (Sum.inl j) = A₁ i j := rfl

@[simp]
lemma fromColumns_apply_inr (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₂) :
(fromColumns A₁ A₂) i (Sum.inr j) = A₂ i j := rfl
lemma fromCols_apply_inr (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₂) :
(fromCols A₁ A₂) i (Sum.inr j) = A₂ i j := rfl

@[simp]
lemma toRows₁_apply (A : Matrix (m₁ ⊕ m₂) n R) (i : m₁) (j : n) :
Expand All @@ -82,24 +82,24 @@ lemma toRows₂_fromRows (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
toRows₂ (fromRows A₁ A₂) = A₂ := rfl

@[simp]
lemma toColumns₁_apply (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₁) :
(toColumns₁ A) i j = A i (Sum.inl j) := rfl
lemma toCols₁_apply (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₁) :
(toCols₁ A) i j = A i (Sum.inl j) := rfl

@[simp]
lemma toColumns₂_apply (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₂) :
(toColumns₂ A) i j = A i (Sum.inr j) := rfl
lemma toCols₂_apply (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₂) :
(toCols₂ A) i j = A i (Sum.inr j) := rfl

@[simp]
lemma toColumns₁_fromColumns (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
toColumns₁ (fromColumns A₁ A₂) = A₁ := rfl
lemma toCols₁_fromCols (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
toCols₁ (fromCols A₁ A₂) = A₁ := rfl

@[simp]
lemma toColumns₂_fromColumns (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
toColumns₂ (fromColumns A₁ A₂) = A₂ := rfl
lemma toCols₂_fromCols (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
toCols₂ (fromCols A₁ A₂) = A₂ := rfl

@[simp]
lemma fromColumns_toColumns (A : Matrix m (n₁ ⊕ n₂) R) :
fromColumns A.toColumns₁ A.toColumns₂ = A := by
lemma fromCols_toCols (A : Matrix m (n₁ ⊕ n₂) R) :
fromCols A.toCols₁ A.toCols₂ = A := by
ext i (j | j) <;> simp

@[simp]
Expand All @@ -111,29 +111,29 @@ lemma fromRows_inj : Function.Injective2 (@fromRows R m₁ m₂ n) := by
simp only [funext_iff, ← Matrix.ext_iff]
aesop

lemma fromColumns_inj : Function.Injective2 (@fromColumns R m n₁ n₂) := by
lemma fromCols_inj : Function.Injective2 (@fromCols R m n₁ n₂) := by
intros x1 x2 y1 y2
simp only [funext_iff, ← Matrix.ext_iff]
aesop

lemma fromColumns_ext_iff (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R)
lemma fromCols_ext_iff (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R)
(B₂ : Matrix m n₂ R) :
fromColumns A₁ A₂ = fromColumns B₁ B₂ ↔ A₁ = B₁ ∧ A₂ = B₂ := fromColumns_inj.eq_iff
fromCols A₁ A₂ = fromCols B₁ B₂ ↔ A₁ = B₁ ∧ A₂ = B₂ := fromCols_inj.eq_iff

lemma fromRows_ext_iff (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix m₁ n R)
(B₂ : Matrix m₂ n R) :
fromRows A₁ A₂ = fromRows B₁ B₂ ↔ A₁ = B₁ ∧ A₂ = B₂ := fromRows_inj.eq_iff

/-- A column partitioned matrix when transposed gives a row partitioned matrix with columns of the
initial matrix transposed to become rows. -/
lemma transpose_fromColumns (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
transpose (fromColumns A₁ A₂) = fromRows (transpose A₁) (transpose A₂) := by
lemma transpose_fromCols (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
transpose (fromCols A₁ A₂) = fromRows (transpose A₁) (transpose A₂) := by
ext (i | i) j <;> simp

/-- A row partitioned matrix when transposed gives a column partitioned matrix with rows of the
initial matrix transposed to become columns. -/
lemma transpose_fromRows (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
transpose (fromRows A₁ A₂) = fromColumns (transpose A₁) (transpose A₂) := by
transpose (fromRows A₁ A₂) = fromCols (transpose A₁) (transpose A₂) := by
ext i (j | j) <;> simp

section Neg
Expand All @@ -148,22 +148,22 @@ lemma fromRows_neg (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :

/-- Negating a matrix partitioned by columns is equivalent to negating each of the columns. -/
@[simp]
lemma fromColumns_neg (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) :
-fromColumns A₁ A₂ = fromColumns (-A₁) (-A₂) := by
lemma fromCols_neg (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) :
-fromCols A₁ A₂ = fromCols (-A₁) (-A₂) := by
ext i (j | j) <;> simp

end Neg

@[simp]
lemma fromColumns_fromRows_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R)
lemma fromCols_fromRows_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R)
(B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
fromColumns (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ := by
fromCols (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ := by
ext (_ | _) (_ | _) <;> simp

@[simp]
lemma fromRows_fromColumn_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R)
madvorak marked this conversation as resolved.
Show resolved Hide resolved
(B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
fromRows (fromColumns B₁₁ B₁₂) (fromColumns B₂₁ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ := by
fromRows (fromCols B₁₁ B₁₂) (fromCols B₂₁ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ := by
ext (_ | _) (_ | _) <;> simp

section Semiring
Expand All @@ -176,8 +176,8 @@ lemma fromRows_mulVec [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n
ext (_ | _) <;> rfl

@[simp]
lemma vecMul_fromColumns [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :
v ᵥ* fromColumns B₁ B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) := by
lemma vecMul_fromCols [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :
v ᵥ* fromCols B₁ B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) := by
ext (_ | _) <;> rfl

@[simp]
Expand All @@ -188,52 +188,52 @@ lemma sum_elim_vecMul_fromRows [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁
simp [Matrix.vecMul, fromRows, dotProduct]

@[simp]
lemma fromColumns_mulVec_sum_elim [Fintype n₁] [Fintype n₂]
lemma fromCols_mulVec_sum_elim [Fintype n₁] [Fintype n₂]
(A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) :
fromColumns A₁ A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂ := by
fromCols A₁ A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂ := by
ext
simp [Matrix.mulVec, fromColumns]
simp [Matrix.mulVec, fromCols]

@[simp]
lemma fromRows_mul [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :
fromRows A₁ A₂ * B = fromRows (A₁ * B) (A₂ * B) := by
ext (_ | _) _ <;> simp [mul_apply]

@[simp]
lemma mul_fromColumns [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
A * fromColumns B₁ B₂ = fromColumns (A * B₁) (A * B₂) := by
lemma mul_fromCols [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
A * fromCols B₁ B₂ = fromCols (A * B₁) (A * B₂) := by
ext _ (_ | _) <;> simp [mul_apply]

@[simp]
lemma fromRows_zero : fromRows (0 : Matrix m₁ n R) (0 : Matrix m₂ n R) = 0 := by
ext (_ | _) _ <;> simp

@[simp]
lemma fromColumns_zero : fromColumns (0 : Matrix m n₁ R) (0 : Matrix m n₂ R) = 0 := by
lemma fromCols_zero : fromCols (0 : Matrix m n₁ R) (0 : Matrix m n₂ R) = 0 := by
ext _ (_ | _) <;> simp

/-- A row partitioned matrix multiplied by a column partitioned matrix gives a 2 by 2 block
matrix. -/
lemma fromRows_mul_fromColumns [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R)
lemma fromRows_mul_fromCols [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R)
(B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
(fromRows A₁ A₂) * (fromColumns B₁ B₂) =
(fromRows A₁ A₂) * (fromCols B₁ B₂) =
fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) := by
ext (_ | _) (_ | _) <;> simp

/-- A column partitioned matrix multiplied by a row partitioned matrix gives the sum of the "outer"
products of the block matrices. -/
lemma fromColumns_mul_fromRows [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R)
lemma fromCols_mul_fromRows [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R)
(B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
fromColumns A₁ A₂ * fromRows B₁ B₂ = (A₁ * B₁ + A₂ * B₂) := by
fromCols A₁ A₂ * fromRows B₁ B₂ = (A₁ * B₁ + A₂ * B₂) := by
ext
simp [mul_apply]

/-- A column partitioned matrix multipiled by a block matrix results in a column partitioned
matrix. -/
lemma fromColumns_mul_fromBlocks [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R)
lemma fromCols_mul_fromBlocks [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R)
(B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
(fromColumns A₁ A₂) * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ =
fromColumns (A₁ * B₁₁ + A₂ * B₂₁) (A₁ * B₁₂ + A₂ * B₂₂) := by
(fromCols A₁ A₂) * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ =
fromCols (A₁ * B₁₁ + A₂ * B₂₁) (A₁ * B₁₂ + A₂ * B₂₂) := by
ext _ (_ | _) <;> simp [mul_apply]

/-- A block matrix multiplied by a row partitioned matrix gives a row partitioned matrix. -/
Expand All @@ -252,23 +252,23 @@ variable [CommRing R]
/-- Multiplication of a matrix by its inverse is commutative.
This is the column and row partitioned matrix form of `Matrix.mul_eq_one_comm`.

The condition `e : n ≃ n₁ ⊕ n₂` states that `fromColumns A₁ A₂` and `fromRows B₁ B₂` are "square".
The condition `e : n ≃ n₁ ⊕ n₂` states that `fromCols A₁ A₂` and `fromRows B₁ B₂` are "square".
-/
lemma fromColumns_mul_fromRows_eq_one_comm
lemma fromCols_mul_fromRows_eq_one_comm
[Fintype n₁] [Fintype n₂] [Fintype n] [DecidableEq n] [DecidableEq n₁] [DecidableEq n₂]
(e : n ≃ n₁ ⊕ n₂)
(A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
fromColumns A₁ A₂ * fromRows B₁ B₂ = 1 ↔ fromRows B₁ B₂ * fromColumns A₁ A₂ = 1 :=
fromCols A₁ A₂ * fromRows B₁ B₂ = 1 ↔ fromRows B₁ B₂ * fromCols A₁ A₂ = 1 :=
mul_eq_one_comm_of_equiv e

/-- The lemma `fromColumns_mul_fromRows_eq_one_comm` specialized to the case where the index sets n₁
/-- The lemma `fromCols_mul_fromRows_eq_one_comm` specialized to the case where the index sets n₁
and n₂, are the result of subtyping by a predicate and its complement. -/
lemma equiv_compl_fromColumns_mul_fromRows_eq_one_comm
lemma equiv_compl_fromCols_mul_fromRows_eq_one_comm
[Fintype n] [DecidableEq n] (p : n → Prop) [DecidablePred p]
(A₁ : Matrix n {i // p i} R) (A₂ : Matrix n {i // ¬p i} R)
(B₁ : Matrix {i // p i} n R) (B₂ : Matrix {i // ¬p i} n R) :
fromColumns A₁ A₂ * fromRows B₁ B₂ = 1 ↔ fromRows B₁ B₂ * fromColumns A₁ A₂ = 1 :=
fromColumns_mul_fromRows_eq_one_comm (id (Equiv.sumCompl p).symm) A₁ A₂ B₁ B₂
fromCols A₁ A₂ * fromRows B₁ B₂ = 1 ↔ fromRows B₁ B₂ * fromCols A₁ A₂ = 1 :=
fromCols_mul_fromRows_eq_one_comm (id (Equiv.sumCompl p).symm) A₁ A₂ B₁ B₂

end CommRing

Expand All @@ -277,16 +277,16 @@ variable [Star R]

/-- A column partitioned matrix in a Star ring when conjugate transposed gives a row partitioned
matrix with the columns of the initial matrix conjugate transposed to become rows. -/
lemma conjTranspose_fromColumns_eq_fromRows_conjTranspose (A₁ : Matrix m n₁ R)
lemma conjTranspose_fromCols_eq_fromRows_conjTranspose (A₁ : Matrix m n₁ R)
(A₂ : Matrix m n₂ R) :
conjTranspose (fromColumns A₁ A₂) = fromRows (conjTranspose A₁) (conjTranspose A₂) := by
conjTranspose (fromCols A₁ A₂) = fromRows (conjTranspose A₁) (conjTranspose A₂) := by
ext (_ | _) _ <;> simp

/-- A row partitioned matrix in a Star ring when conjugate transposed gives a column partitioned
matrix with the rows of the initial matrix conjugate transposed to become columns. -/
lemma conjTranspose_fromRows_eq_fromColumns_conjTranspose (A₁ : Matrix m₁ n R)
lemma conjTranspose_fromRows_eq_fromCols_conjTranspose (A₁ : Matrix m₁ n R)
(A₂ : Matrix m₂ n R) : conjTranspose (fromRows A₁ A₂) =
fromColumns (conjTranspose A₁) (conjTranspose A₂) := by
fromCols (conjTranspose A₁) (conjTranspose A₂) := by
ext _ (_ | _) <;> simp

end Star
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Data/Matrix/Notation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -381,9 +381,9 @@ theorem submatrix_updateRow_succAbove (A : Matrix (Fin m.succ) n' α) (v : n'

/-- Updating a column then removing it is the same as removing it. -/
@[simp]
theorem submatrix_updateColumn_succAbove (A : Matrix m' (Fin n.succ) α) (v : m' → α) (f : o' → m')
(i : Fin n.succ) : (A.updateColumn i v).submatrix f i.succAbove = A.submatrix f i.succAbove :=
ext fun _r s => updateColumn_ne (Fin.succAbove_ne i s)
theorem submatrix_updateCol_succAbove (A : Matrix m' (Fin n.succ) α) (v : m' → α) (f : o' → m')
(i : Fin n.succ) : (A.updateCol i v).submatrix f i.succAbove = A.submatrix f i.succAbove :=
ext fun _r s => updateCol_ne (Fin.succAbove_ne i s)

end Submatrix

Expand Down
Loading
Loading