From 1619e6ae525f14c3493c26154aa40b42c8649e1f Mon Sep 17 00:00:00 2001
From: madvorak <martin.dvorak@matfyz.cz>
Date: Thu, 31 Oct 2024 15:47:25 +0100
Subject: [PATCH] feat: totally unimodular matrices

---
 Mathlib.lean                                  |  1 +
 .../Matrix/Determinant/TotallyUnimodular.lean | 96 +++++++++++++++++++
 2 files changed, 97 insertions(+)
 create mode 100644 Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 9ff29007e3369..ea53ffb651e0e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3175,6 +3175,7 @@ import Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
 import Mathlib.LinearAlgebra.Matrix.Circulant
 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
 import Mathlib.LinearAlgebra.Matrix.Determinant.Misc
+import Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
 import Mathlib.LinearAlgebra.Matrix.Diagonal
 import Mathlib.LinearAlgebra.Matrix.DotProduct
 import Mathlib.LinearAlgebra.Matrix.Dual
diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean b/Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
new file mode 100644
index 0000000000000..df19f894f0bb4
--- /dev/null
+++ b/Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2024 Martin Dvorak. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Martin Dvorak, Vladimir Kolmogorov, Ivan Sergeev
+-/
+import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
+
+/-!
+# Totally unimodular matrices
+
+This file defines totally unimodular matrices and provides basic API for them.
+
+## Main definitions
+
+ - `Matrix.IsTotallyUnimodular`: a matrix is totally unimodular iff every square submatrix
+    (not necessarily contiguous) has determinant `0` or `1` or `-1`.
+
+## Main results
+
+ - `Matrix.IsTotallyUnimodular_iff`: a matrix is totally unimodular iff every square submatrix
+    (possibly with repeated rows and/or repeated columns) has determinant `0` or `1` or `-1`.
+ - `Matrix.IsTotallyUnimodular.apply`: entry in a totally unimodular matrix is `0` or `1` or `-1`.
+
+-/
+
+open scoped Matrix
+
+variable {m n R : Type*} [CommRing R]
+
+/-- Is the matrix `A` totally unimodular? -/
+def Matrix.IsTotallyUnimodular (A : Matrix m n R) : Prop :=
+  ∀ k : ℕ, ∀ f : Fin k → m, ∀ g : Fin k → n, f.Injective → g.Injective →
+    (A.submatrix f g).det = 0 ∨
+    (A.submatrix f g).det = 1 ∨
+    (A.submatrix f g).det = -1
+
+lemma Matrix.IsTotallyUnimodular_iff (A : Matrix m n R) : A.IsTotallyUnimodular ↔
+    ∀ k : ℕ, ∀ f : Fin k → m, ∀ g : Fin k → n,
+      (A.submatrix f g).det = 0 ∨
+      (A.submatrix f g).det = 1 ∨
+      (A.submatrix f g).det = -1
+    := by
+  constructor <;> intro hA
+  · intro k f g
+    if hf : f.Injective then
+      if hg : g.Injective then
+        exact hA k f g hf hg
+      else
+        left
+        unfold Function.Injective at hg
+        push_neg at hg
+        obtain ⟨i, j, hqij, hij⟩ := hg
+        apply Matrix.det_zero_of_column_eq hij
+        intro
+        simp [hqij]
+    else
+      left
+      unfold Function.Injective at hf
+      push_neg at hf
+      obtain ⟨i, j, hpij, hij⟩ := hf
+      apply Matrix.det_zero_of_row_eq
+      · exact hij
+      show (A (f i)) ∘ (g ·) = (A (f j)) ∘ (g ·)
+      rw [hpij]
+  · intro _ _ _ _ _
+    apply hA
+
+lemma Matrix.IsTotallyUnimodular.apply {A : Matrix m n R} (hA : A.IsTotallyUnimodular)
+    (i : m) (j : n) :
+    A i j = 0 ∨ A i j = 1 ∨ A i j = -1 := by
+  let f : Fin 1 → m := (fun _ => i)
+  let g : Fin 1 → n := (fun _ => j)
+  convert hA 1 f g (Function.injective_of_subsingleton f) (Function.injective_of_subsingleton g) <;>
+  exact (det_fin_one (A.submatrix f g)).symm
+
+lemma Matrix.IsTotallyUnimodular.submatrix {A : Matrix m n R} (hA : A.IsTotallyUnimodular) {k : ℕ}
+    (f : Fin k → m) (g : Fin k → n) :
+    (A.submatrix f g).IsTotallyUnimodular := by
+  intro _ _ _ _ _
+  rw [Matrix.submatrix_submatrix]
+  rw [Matrix.IsTotallyUnimodular_iff] at hA
+  apply hA
+
+lemma Matrix.IsTotallyUnimodular.transpose {A : Matrix m n R} (hA : A.IsTotallyUnimodular) :
+    Aᵀ.IsTotallyUnimodular := by
+  intro _ _ _ _ _
+  simp only [←Matrix.transpose_submatrix, Matrix.det_transpose]
+  apply hA <;> assumption
+
+lemma Matrix.mapEquiv_IsTotallyUnimodular {X' Y' : Type*}
+    (A : Matrix m n R) (eX : X' ≃ m) (eY : Y' ≃ n) :
+    Matrix.IsTotallyUnimodular ((A · ∘ eY) ∘ eX) ↔ A.IsTotallyUnimodular := by
+  rw [Matrix.IsTotallyUnimodular_iff, Matrix.IsTotallyUnimodular_iff]
+  constructor <;> intro hA k f g
+  · simpa [Matrix.submatrix] using hA k (eX.symm ∘ f) (eY.symm ∘ g)
+  · simpa [Matrix.submatrix] using hA k (eX ∘ f) (eY ∘ g)