English
If A is totally unimodular and each row of B is zero except for at most a single 1 or a single −1, then fromRows A B is totally unimodular.
Русский
Если A тотально унимодулярна и каждая строка B содержит нули, за исключением одной единицы или одной −1, тогда fromRows A B тоже тотально унимодулярна.
LaTeX
$$IsTotallyUnimodular((fromRows A B))$$
Lean4
/-- If `A` is totally unimodular and each row of `B` is all zeros except for at most a single `1` or
a single `-1` then `fromRows A B` is totally unimodular. -/
theorem fromRows_unitlike [DecidableEq n] {A : Matrix m n R} {B : Matrix m' n R} (hA : A.IsTotallyUnimodular)
(hB : Nonempty n → ∀ i : m', ∃ j : n, ∃ s : SignType, B i = Pi.single j s.cast) :
(fromRows A B).IsTotallyUnimodular := by
intro k f g hf hg
induction k with
| zero => use 1; simp
| succ k
ih =>
specialize
hB
⟨g 0⟩
-- Either `f` is `inr` somewhere or `inl` everywhere
obtain ⟨i, j, hfi⟩ | ⟨f', rfl⟩ : (∃ i j, f i = .inr j) ∨ (∃ f', f = .inl ∘ f') :=
by
simp_rw [← Sum.isRight_iff, or_iff_not_imp_left, not_exists, Bool.not_eq_true, Sum.isRight_eq_false,
Sum.isLeft_iff]
intro hfr
choose f' hf' using hfr
exact ⟨f', funext hf'⟩
· have hAB := det_succ_row ((fromRows A B).submatrix f g) i
simp only [submatrix_apply, hfi, fromRows_apply_inr] at hAB
obtain ⟨j', s, hj'⟩ := hB j
· simp only [hj'] at hAB
by_cases hj'' : ∃ x, g x = j'
· obtain ⟨x, rfl⟩ := hj''
rw [Fintype.sum_eq_single x fun y hxy => ?_, Pi.single_eq_same] at hAB
· rw [hAB]
change _ ∈ MonoidHom.mrange SignType.castHom.toMonoidHom
refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_
· apply pow_mem
exact ⟨-1, by simp⟩
· exact ih _ _ (hf.comp Fin.succAbove_right_injective) (hg.comp Fin.succAbove_right_injective)
· simp [Pi.single_eq_of_ne, hg.ne_iff.mpr hxy]
· rw [not_exists] at hj''
use 0
simpa [hj''] using hAB.symm
· rw [isTotallyUnimodular_iff] at hA
apply hA
