OAI/GroupTheory/Hyperbolic/MatrixRank.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release075.det_abs_le_prod_row_norm line 11
2. theorem OAI.Release075.exists_row_basis line 24

   Source documentation

   A matrix has a spanning independent subset of its rows, with the expected size.

   theorem exists_row_basis {ι κ K : Type*} [Fintype ι] [Fintype κ] [Field K]
       (M : Matrix ι κ K) :
       ∃ S : Finset ι, S.card = M.rank ∧
         LinearIndependent K (fun i : S => M i.val) ∧
         ∀ i, ∃ c : S → K, M i = ∑ j : S, c j • M j.val := by
   …

3. theorem OAI.Release075.pow_sub_card_dvd_det line 57

   Source documentation

   Factoring a common divisor from all rows outside a specified set.

   theorem pow_sub_card_dvd_det {ι : Type*} [Fintype ι] [DecidableEq ι]
       (A : Matrix ι ι ℤ) (S : Finset ι) (q : ℤ)
       (h : ∀ i, i ∉ S → ∀ j, q ∣ A i j) :
       q ^ (Fintype.card ι - S.card) ∣ A.det := by
   …

4. theorem OAI.Release075.pow_card_sub_rank_dvd_det line 84

   Source documentation

   The integral determinant detects the rank lost in reduction modulo a prime.

   theorem pow_card_sub_rank_dvd_det {ι : Type*} [Fintype ι] [DecidableEq ι]
       (A : Matrix ι ι ℤ) (q : ℕ) [Fact q.Prime] :
       (q : ℤ) ^ (Fintype.card ι - (A.map (Int.cast : ℤ → ZMod q)).rank) ∣ A.det := by
   …

5. theorem OAI.Release075.exists_full_rank_minor line 129

   Source documentation

   A full-rank minor exists over a field; both index maps are injective.

   theorem exists_full_rank_minor {ι κ K : Type*} [Fintype ι] [Fintype κ] [Field K]
       (M : Matrix ι κ K) :
       ∃ (f : Fin M.rank → ι) (g : Fin M.rank → κ),
         Function.Injective f ∧ Function.Injective g ∧ (M.submatrix f g).det ≠ 0 := by
   …

6. theorem OAI.Release075.det_sq_le_pow_of_row_sq_le line 153

   Source documentation

   The squared form of Hadamard's inequality avoids fractional exponents.

   theorem det_sq_le_pow_of_row_sq_le {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ)
       (r : ℝ) (hrow : ∀ i, ∑ j, A i j ^ 2 ≤ r) : A.det ^ 2 ≤ r ^ n := by
   …

7. theorem OAI.Release075.nonsingular_rank_reduction_half line 172

   Source documentation

   A nonsingular integer matrix loses less than half its rank modulo a prime larger than the common squared row-norm bound.

   theorem nonsingular_rank_reduction_half {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ)
       (hdet : A.det ≠ 0) (r : ℝ) (hr : 1 ≤ r)
       (hrow : ∀ i, ∑ j, (A i j : ℝ) ^ 2 ≤ r)
       (q : ℕ) [Fact q.Prime] (hqr : r < q) :
       n ≤ 2 * (A.map (Int.cast : ℤ → ZMod q)).rank := by
   …

8. theorem OAI.Release075.rank_reduction_half line 201
9. theorem OAI.Release075.trace_sq_le_rank_mul_trace_sq line 236

   Source documentation

   The trace-rank inequality used on a Gram matrix in the finite quotient.

   theorem trace_sq_le_rank_mul_trace_sq {ι : Type*} [Fintype ι]
       (A : Matrix ι ι ℝ) (hA : A.IsHermitian) :
       A.trace ^ 2 ≤ (A.rank : ℝ) * (A * A).trace := by
   …

10. theorem OAI.Release075.rank_add_le line 260

    Source documentation

    Subadditivity of matrix rank over a field.

    theorem rank_add_le {ι κ K : Type*} [Fintype ι] [Fintype κ] [Field K]
        (A B : Matrix ι κ K) : (A + B).rank ≤ A.rank + B.rank := by
    …

11. theorem OAI.Release075.rank_sum_le line 266
12. def OAI.Release075.regularMatrix line 276

    Source documentation

    The left regular permutation representation over any coefficient semiring.

    def regularMatrix {F R : Type*} [Group F] [Fintype F] [DecidableEq F] [Semiring R] :
        F →* Matrix F F R := Matrix.permMatrixHom.comp (MulAction.toPermHom F F)

13. theorem OAI.Release075.regularMatrix_apply line 279
14. theorem OAI.Release075.regularMatrix_transpose line 285
15. theorem OAI.Release075.regularMatrix_trace line 291
16. def OAI.Release075.flattenMatrix line 302

    Source documentation

    Flatten a rectangular matrix of blocks, with the block index first.

    def flattenMatrix {ι κ α β R : Type*} (A : Matrix ι κ (Matrix α β R)) :
        Matrix (ι × α) (κ × β) R := fun i j => A i.1 j.1 i.2 j.2

17. theorem OAI.Release075.flattenMatrix_apply line 305
18. theorem OAI.Release075.flattenMatrix_mul line 309
19. theorem OAI.Release075.flattenMatrix_transpose line 316
20. theorem OAI.Release075.flattenMatrix_trace line 320
21. def OAI.Release075.quotientMatrix line 326

    Source documentation

    The block regular-representation matrix attached to one line label.

    def quotientMatrix {ι F R : Type*} [Group F] [Fintype F] [DecidableEq F]
        [Semiring R] (g : ι → ι → F) : Matrix (ι × F) (ι × F) R :=
    …

22. theorem OAI.Release075.quotientMatrix_gram line 330
23. theorem OAI.Release075.quotientMatrix_gram_trace line 339
24. theorem OAI.Release075.quotientMatrix_gram_sq_trace line 348

    Source documentation

    The second trace expansion, before counting degenerate rectangles.

    theorem quotientMatrix_gram_sq_trace {ι F R : Type*} [Fintype ι] [Group F]
        [Fintype F] [DecidableEq F] [Semiring R] (g : ι → ι → F) :
        ((quotientMatrix (R := R) g * (quotientMatrix g).transpose) *
    …

    Mentions: OAI.Release075.quotientMatrix

25. def OAI.Release075.RectanglesSurvive line 364

    Source documentation

    Nondegenerate rectangular words survive in the finite group.

    def RectanglesSurvive {ι F : Type*} [Group F] (g : ι → ι → F) : Prop :=
    …

26. theorem OAI.Release075.quotientMatrix_gram_sq_trace_of_rectangles line 369

    Source documentation

    The exact count 2r^3-r^2 of degenerate index choices.

    theorem quotientMatrix_gram_sq_trace_of_rectangles {ι F R : Type*} [Fintype ι]
        [Group F] [Fintype F] [DecidableEq F] [CommRing R]
        (g : ι → ι → F) (hg : RectanglesSurvive g) :
        ((quotientMatrix (R := R) g * (quotientMatrix g).transpose) *
    …

    Mentions: OAI.Release075.RectanglesSurvive, OAI.Release075.quotientMatrix

27. theorem OAI.Release075.quotientMatrix_row_sq line 396

    Source documentation

    Each integral row has exactly one unit entry per block column.

    theorem quotientMatrix_row_sq {ι F : Type*} [Fintype ι] [Group F]
        [Fintype F] [DecidableEq F] (g : ι → ι → F) (i : ι × F) :
        ∑ j, ((quotientMatrix (R := ℤ) g i j : ℤ) : ℝ) ^ 2 = Fintype.card ι := by
    …

    Mentions: OAI.Release075.quotientMatrix

28. theorem OAI.Release075.quotientMatrix_map line 403

    Source documentation

    Casting the integral matrix gives the corresponding coefficient representation.

    theorem quotientMatrix_map {ι F R : Type*} [Group F] [Fintype F]
        [DecidableEq F] [Ring R] (g : ι → ι → F) :
        (quotientMatrix (R := ℤ) g).map (Int.cast : ℤ → R) = quotientMatrix (R := R) g := by
    …

    Mentions: OAI.Release075.quotientMatrix

29. theorem OAI.Release075.quotientMatrix_rank_real_lower line 409
30. theorem OAI.Release075.quotientMatrix_rank_mod_lower line 444
31. def OAI.Release075.diagonalBlocks line 459

    Source documentation

    Block direct sum with the line-label index first.

    def diagonalBlocks {I ι κ K : Type*} [DecidableEq I] [Zero K]
        (Y : I → Matrix ι κ K) : Matrix (I × ι) (I × κ) K :=
    …

32. theorem OAI.Release075.sum_rank_le_rank_diagonalBlocks line 464

    Source documentation

    The lower rank bound for a direct sum, proved by its full-rank block minors.

    theorem sum_rank_le_rank_diagonalBlocks {I ι κ K : Type*} [Fintype I]
        [Fintype ι] [Fintype κ] [DecidableEq I] [Field K]
        (Y : I → Matrix ι κ K) : (∑ i, (Y i).rank) ≤ (diagonalBlocks Y).rank := by
    …

    Mentions: OAI.Release075.diagonalBlocks

33. theorem OAI.Release075.rank_neg line 491
34. def OAI.Release075.weightedMatrix line 497

    Source documentation

    The rank-one scalar matrix f fᵀ tensored with a matrix.

    def weightedMatrix {I ι κ K : Type*} [Mul K] (f : I → K) (Z : Matrix ι κ K) :
        Matrix (I × ι) (I × κ) K := Matrix.of fun x y => f x.1 * f y.1 * Z x.2 y.2

35. theorem OAI.Release075.weightedMatrix_rank_le line 501

    Source documentation

    A rank-one tensor weight never increases rank.

    theorem weightedMatrix_rank_le {I ι κ K : Type*} [Fintype I] [Fintype ι]
        [Fintype κ] [Field K] (f : I → K) (Z : Matrix ι κ K) :
        (weightedMatrix f Z).rank ≤ Z.rank := by
    …

    Mentions: OAI.Release075.weightedMatrix

36. theorem OAI.Release075.tensor_certificate line 516

    Source documentation

    Exchanging the incidence sums turns the punctured-line certificate into a block-diagonal matrix identity. The coefficient order in each matrix is unchanged.

    theorem tensor_certificate {P I ι κ K : Type*} [Fintype P] [Fintype I]
        [DecidableEq I] [Field K] (inc : P → Finset I) (f : P → I → K)
        (Y : I → Matrix ι κ K)
        (hline : ∀ i j k, (∑ z, if i ∈ inc z then f z j * f z k else 0) =
          -(if j = i ∧ k = i then 1 else 0)) :
        (∑ z, weightedMatrix (f z) (∑ i ∈ inc z, Y i)) = -diagonalBlocks Y := by
    …

    Mentions: OAI.Release075.weightedMatrix, OAI.Release075.diagonalBlocks

37. theorem OAI.Release075.rank_budget_of_line_certificate line 538
38. theorem OAI.Release075.quotientMatrix_sum_rank_le line 553

    Source documentation

    A local Cartesian block factors through one copy of the finite regular module.

    theorem quotientMatrix_sum_rank_le {ι s t F K : Type*} [Fintype ι]
        [Fintype s] [Fintype t] [Group F] [Fintype F] [DecidableEq F] [Field K]
        (L : ι → s → F) (R : ι → t → F) :
        (∑ j : s, ∑ k : t, quotientMatrix (R := K) (fun u v => (L u j)⁻¹ * R v k)).rank ≤
    …

    Mentions: OAI.Release075.quotientMatrix

39. theorem OAI.Release075.quotientMatrix_sum_reindex line 581

    Source documentation

    An arbitrary relabeling of a Cartesian block does not affect its summed regular-representation matrix. Opposite-index shifts are permitted independently.

    theorem quotientMatrix_sum_reindex {ι B s t F K : Type*} [Fintype B]
        [Fintype s] [Fintype t] [Group F] [Fintype F] [DecidableEq F] [Semiring K]
        (g : B → ι → ι → F) (L : ι → s → F) (R : ι → t → F)
        (e : ι → ι → B ≃ s × t)
        (h : ∀ i u v, g i u v = (L u (e u v i).1)⁻¹ * R v (e u v i).2) :
        (∑ i, quotientMatrix (R := K) (g i)) =
    …

    Mentions: OAI.Release075.quotientMatrix

40. theorem OAI.Release075.polynomial_sum_eq_zero line 595

    Source documentation

    A polynomial below the finite-field power-sum threshold has zero total sum.

    theorem polynomial_sum_eq_zero {K : Type*} [Field K] [Fintype K]
        (p : Polynomial K) (hdeg : p.natDegree < Fintype.card K - 1) :
        ∑ x, p.eval x = 0 := by
    …

41. def OAI.Release075.gridLagrange line 605
42. theorem OAI.Release075.gridLagrange_self line 609
43. theorem OAI.Release075.gridLagrange_other line 617
44. def OAI.Release075.gridLagrangeLine line 627

    Source documentation

    Restriction of the grid Lagrange basis along the parametrized affine line.

    noncomputable def gridLagrangeLine {T K : Type*} [Fintype T] [Field K] [DecidableEq K]
        (S : Finset K) (a b v : T → K) : Polynomial K :=
    …

45. theorem OAI.Release075.gridLagrangeLine_eval line 633
46. theorem OAI.Release075.gridLagrangeLine_natDegree_le line 645
47. theorem OAI.Release075.polygon_weight_line_sum line 668

    Source documentation

    Every entry of the rank-one weight matrix has zero sum over a full line.

    theorem polygon_weight_line_sum {T K : Type*} [Fintype T] [Field K] [Fintype K]
        [DecidableEq K] (S : Finset K) (a a' b v : T → K)
        (ha : ∀ t, a t ∈ S) (ha' : ∀ t, a' t ∈ S)
        (hdeg : 2 * (Fintype.card T * (S.card - 1)) < Fintype.card K - 1) :
        (∑ x : K, gridLagrange S a (fun t => b t + x * v t) *
          gridLagrange S a' (fun t => b t + x * v t)) = 0 := by
    …

    Mentions: OAI.Release075.gridLagrange

48. theorem OAI.Release075.exists_finite_separating_family line 681

    Source documentation

    Finite separating families can be combined into one finite target.

    theorem exists_finite_separating_family {G : Type u} {ι : Type v} [Group G] [Fintype ι]
        [Group.ResiduallyFinite G] (w : ι → G) (hw : ∀ i, w i ≠ 1) :
        ∃ (Q : Type (max u v)) (_ : Group Q) (_ : Fintype Q) (φ : G →* Q), ∀ i, φ (w i) ≠ 1 := by
    …

49. def OAI.Release075.affineLineMap line 695

    Source documentation

    Standard affine parametrization, with the marked point at parameter zero.

    def affineLineMap {T K : Type*} [Field K] (a v : T → K) (x : K) : T → K :=
    …

50. theorem OAI.Release075.affineLineMap_injective line 698
51. def OAI.Release075.puncturedLine line 707

    Source documentation

    The geometric affine line punctured only at its own marked point.

    noncomputable def puncturedLine {T K : Type*} [Fintype T] [Field K] [Fintype K]
        (a v : T → K) : Finset (T → K) := by
    …

52. theorem OAI.Release075.puncturedLine_sum line 713

    Source documentation

    Summation on a punctured line subtracts exactly the value at its own mark.

    theorem puncturedLine_sum {T K R : Type*} [Fintype T] [Field K] [Fintype K]
        [AddCommGroup R] (a v : T → K) (hv : v ≠ 0) (w : (T → K) → R) :
        (∑ z ∈ puncturedLine a v, w z) = (∑ x, w (affineLineMap a v x)) - w a := by
    …

    Mentions: OAI.Release075.puncturedLine, OAI.Release075.affineLineMap

53. def OAI.Release075.lineIncidence line 721
54. theorem OAI.Release075.grid_line_certificate line 728

    Source documentation

    The exact finite-field punctured-line matrix certificate, with no asymptotic or characteristic assumption beyond its explicit degree threshold.

    theorem grid_line_certificate {T I K : Type*} [Fintype T] [Fintype I]
        [DecidableEq T] [DecidableEq I] [Field K] [Fintype K] [DecidableEq K]
        (S : Finset K) (a v : I → T → K) (ha : ∀ i t, a i t ∈ S)
        (hinj : Function.Injective a) (hv : ∀ i, v i ≠ 0)
        (hdeg : 2 * (Fintype.card T * (S.card - 1)) < Fintype.card K - 1) :
        ∀ i j k, (∑ z, if i ∈ lineIncidence a v z then
          gridLagrange S (a j) z * gridLagrange S (a k) z else 0) =
          -(if j = i ∧ k = i then 1 else 0) := by
    …

    Mentions: OAI.Release075.lineIncidence, OAI.Release075.gridLagrange

55. theorem OAI.Release075.two_block_sizes line 753
56. structure OAI.Release075.CartesianBlock line 764
57. instance OAI.Release075.(instance at line 774) line 774
58. instance OAI.Release075.(instance at line 775) line 775
59. def OAI.Release075.CartesianBlock.shifted line 778

    Source documentation

    Opposite-index shifts are bijections of the block coordinates.

    def CartesianBlock.shifted {I : Type*} {r : ℕ} (b : CartesianBlock I r)
        (u v : Fin r) : b.labels ≃ ZMod b.s × ZMod b.t :=
    …

    Mentions: OAI.Release075.CartesianBlock

60. theorem OAI.Release075.CartesianBlock.quotient_rank_le line 783
61. theorem OAI.Release075.exists_two_cartesian_blocks line 798

    Source documentation

    Every sufficiently large finite set has the two Cartesian blocks required by the construction; the coordinate bijections are chosen without deleting labels.

    theorem exists_two_cartesian_blocks {I : Type*} [DecidableEq I] (r : ℕ) (hr : 0 < r)
        (A : Finset I) (hA : 4 * r ^ 2 ≤ A.card) :
        ∃ b₀ b₁ : CartesianBlock I r,
          Disjoint b₀.labels b₁.labels ∧ b₀.labels ∪ b₁.labels = A := by
    …

    Mentions: OAI.Release075.CartesianBlock

62. theorem OAI.Release075.finite_quotient_rank_obstruction line 823

    Source documentation

    The numerical rank contradiction. The exceptional incidences are retained; the ambient dimension, not a deletion, bounds their matrices.

    theorem finite_quotient_rank_obstruction {P I F : Type*} [Fintype P] [Fintype I]
        [DecidableEq I] [Group F] [Fintype F] [DecidableEq F]
        (r q : ℕ) [Fact q.Prime] (hq : r < q)
        (inc : P → Finset I) (f : P → I → ZMod q) (E : Finset P)
        (g : I → Fin r → Fin r → F) (hg : ∀ i, RectanglesSurvive (g i))
        (hline : ∀ i j k, (∑ z, if i ∈ inc z then f z j * f z k else 0) =
          -(if j = i ∧ k = i then 1 else 0))
        (hlocal : ∀ z, z ∉ E → (∑ i ∈ inc z, quotientMatrix (R := ZMod q) (g i)).rank ≤
    …

    Mentions: OAI.Release075.RectanglesSurvive, OAI.Release075.quotientMatrix

63. def OAI.Release075.CartesianBlock.Relations line 865

    Source documentation

    The exact defining relation of a single block, retaining the order L⁻¹R.

    def CartesianBlock.Relations {I G : Type*} [Group G] {r : ℕ}
        (b : CartesianBlock I r) (g : I → Fin r → Fin r → G) : Prop :=
    …

    Mentions: OAI.Release075.CartesianBlock

64. theorem OAI.Release075.CartesianBlock.Relations.map line 872
65. theorem OAI.Release075.two_block_quotient_rank_le line 880
66. theorem OAI.Release075.exists_finite_preserving_rectangles line 897

    Source documentation

    All specified nontrivial rectangular words can be preserved in one finite image if the group is residually finite.

    theorem exists_finite_preserving_rectangles {I : Type u} {G : Type v} [Fintype I] [Group G]
        [Group.ResiduallyFinite G] {r : ℕ} (g : I → Fin r → Fin r → G)
        (hg : ∀ i, RectanglesSurvive (g i)) :
        ∃ (Q : Type (max u v)) (_ : Group Q) (_ : Fintype Q) (φ : G →* Q),
          ∀ i, RectanglesSurvive (fun u v => φ (g i u v)) := by
    …

    Mentions: OAI.Release075.RectanglesSurvive

67. theorem OAI.Release075.not_residuallyFinite_of_line_blocks line 914