Combining maximal-minor divisibility across row blocks.

noncomputable def CCDN.residueRows {c s : ℕ} (label : Fin s → Fin c) (i : Fin c) : Fin (Fintype.card { j : Fin s // label j = i }) → Fin s

An enumeration of the rows j with label j = i, the i-th block of the partition of the rows determined by label.

Equations

• CCDN.residueRows label i j = ↑((Fintype.equivFin { j : Fin s // label j = i }).symm j)

theorem CCDN.residueRows_label {c s : ℕ} (label : Fin s → Fin c) (i : Fin c) (j : Fin (Fintype.card { j : Fin s // label j = i })) : label (residueRows label i j) = i

Every row enumerated by residueRows label i has label i.

theorem CCDN.sum_residue_class_sizes {c s : ℕ} (label : Fin s → Fin c) : ∑ i : Fin c, Fintype.card { j : Fin s // label j = i } = s

The sizes of the classes of a labelling label : Fin s → Fin c add up to s.

theorem CCDN.minorGcd_eq_gcd_plucker {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι ℤ) : Int.Matrix.minorGcd A = Finset.univ.gcd (exteriorPower.plucker m A.row)

Int.Matrix.minorGcd is the gcd of the Plücker coordinates of the rows. The vendored definition is not exposed; this module imports its body (import all) so that the rest of the library can rewrite with this lemma instead.

theorem CCDN.residue_prime_powers_dvd_minorGcd {c s N : ℕ} (A : Matrix (Fin s) (Fin N) ℤ) (label : Fin s → Fin c) (p : ℤ) (e : Fin c → ℕ) (he : ∀ (i : Fin c) (j : Fin (Fintype.card { j : Fin s // label j = i }) → Fin N), p ^ e i ∣ (A.submatrix (residueRows label i) j).det) : p ^ ∑ i : Fin c, e i ∣ Int.Matrix.minorGcd A

If the rows of an integer matrix A are partitioned into blocks by label, and for each block i the power p ^ e i divides every maximal minor of the block's rows, then p ^ (∑ i, e i) divides the gcd of the maximal minors of A.