mul_listTransvecRow_last_row — Mathlib

English

There exist lists L and L' of transvections such that the product (L.map toMatrix).prod * M * (L'.map toMatrix).prod is block-diagonal, whenever the last coefficient of M in the bottom-right entry is nonzero.

Русский

Существуют списки транспектаций L и L' так, что произведение становится блочно-диагональным, если нижний правый элемент M не равен нулю.

LaTeX

$$$\exists L\,L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜),\; (L.map toMatrix).prod * M * (L'.map toMatrix).prod \text{ isTwoBlockDiagonal} \ & (M(inr\,unit)(inr\,unit) \neq 0)$$$

Lean4

/-- Multiplying by all the matrices in `listTransvecRow M` kills all the coefficients in the
last row but the last one. -/
theorem mul_listTransvecRow_last_row (hM : M (inr unit) (inr unit) ≠ 0) (i : Fin r) :
    (M * (listTransvecRow M).prod) (inr unit) (inl i) = 0 :=
  by
  suffices H :
    ∀ k : ℕ,
      k ≤ r → (M * ((listTransvecRow M).take k).prod) (inr unit) (inl i) = if k ≤ i then M (inr unit) (inl i) else 0
    by
    have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
    rw [← List.take_length (l := listTransvecRow M), A]
    have : ¬r ≤ i := by simp
    simpa only [this, ite_eq_right_iff] using H r le_rfl
  intro k hk
  induction k with
  | zero => simp only [if_true, Matrix.mul_one, List.take_zero, zero_le', List.prod_nil]
  | succ n IH =>
    have hnr : n < r := hk
    let n' : Fin r := ⟨n, hnr⟩
    have A :
      (listTransvecRow M)[n]? =
        ↑(transvection (inr unit) (inl n') (-M (inr unit) (inl n') / M (inr unit) (inr unit))) :=
      by simp only [n', listTransvecRow, hnr, dif_pos, List.getElem?_ofFn]
    simp only [List.take_succ, A, ← Matrix.mul_assoc, List.prod_append, Matrix.mul_one, List.prod_cons, List.prod_nil,
      Option.toList_some]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]
      have : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_le]
      simp only [h, mul_transvection_apply_same, if_false, mul_listTransvecRow_last_col_take _ _ hnr.le, hni.le, this,
        if_true, IH hnr.le]
      field_simp
      ring
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
      simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq, not_false_eq_true]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp [hi, n.le_succ.trans hi]
      · rw [if_neg, if_neg]
        · simpa only [not_le] using hi
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi

Похожие утверждения