MatrixLimits.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Basis coordinates, maximal minors, and limits of finite matrices

def OAI.Nagata.Workers.W11.basisJetMatrix line 22
Source documentation
The matrix of a linear jet map is its values on a genuine domain basis.
```
def basisJetMatrix (e : Basis ι K V) (J : V →ₗ[K] (κ → K)) : Matrix κ ι K :=
…
```
theorem OAI.Nagata.Workers.W11.basisJetMatrix_mulVec_repr line 27
Source documentation
Evaluating the basis matrix on a coordinate vector recovers the original linear map, by the finite basis expansion of the vector.
```
theorem basisJetMatrix_mulVec_repr (e : Basis ι K V) (J : V →ₗ[K] (κ → K)) (v : V) :
    (basisJetMatrix e J).mulVec (e.repr v) = J v := by
…
```
Mentions: OAI.Nagata.Workers.W11.basisJetMatrix
theorem OAI.Nagata.Workers.W11.injective_of_basisJetMatrix line 36
Source documentation
Injectivity of the numerical matrix implies injectivity of the original linear jet map in its genuine vector space.
```
theorem injective_of_basisJetMatrix (e : Basis ι K V) (J : V →ₗ[K] (κ → K))
    (h : Function.Injective (basisJetMatrix e J).mulVec) : Function.Injective J := by
…
```
Mentions: OAI.Nagata.Workers.W11.basisJetMatrix
theorem OAI.Nagata.Workers.W11.basisJetMatrix_nonzero_kernel line 48
Source documentation
A nonzero kernel vector of the original jet map becomes a nonzero kernel coordinate vector. This proves the noncancellation bridge for a genuine basis.
```
theorem basisJetMatrix_nonzero_kernel (e : Basis ι K V) (J : V →ₗ[K] (κ → K))
    (v : V) (hv : v ≠ 0) (hJ : J v = 0) :
    ∃ c : ι → K, c ≠ 0 ∧ (basisJetMatrix e J).mulVec c = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W11.basisJetMatrix

theorem OAI.Nagata.Workers.W11.tendsto_det_of_entrywise line 78

Source documentation

Entrywise convergence of finite square complex matrices implies convergence of their determinants. The parameter filter can in particular be 𝓝[>] 0.

theorem tendsto_det_of_entrywise {l : Filter α}
    {B : α → Matrix ι ι ℂ} {B₀ : Matrix ι ι ℂ}
    (hB : ∀ i j, Tendsto (fun t => B t i j) l (𝓝 (B₀ i j))) :
    Tendsto (fun t => (B t).det) l (𝓝 B₀.det) := by
…

theorem OAI.Nagata.Workers.W11.eventually_det_ne_zero_of_entrywise line 87

Source documentation

A nonzero limiting determinant remains nonzero eventually.

theorem eventually_det_ne_zero_of_entrywise {l : Filter α}
    {B : α → Matrix ι ι ℂ} {B₀ : Matrix ι ι ℂ}
    (hB : ∀ i j, Tendsto (fun t => B t i j) l (𝓝 (B₀ i j)))
    (h₀ : B₀.det ≠ 0) : ∀ᶠ t in l, (B t).det ≠ 0 :=
…

theorem OAI.Nagata.Workers.W11.eventually_injective_of_entrywise line 95

Source documentation

A square matrix family with nonzero limiting determinant is eventually injective as a map on coefficient vectors.

theorem eventually_injective_of_entrywise {l : Filter α}
    {B : α → Matrix ι ι ℂ} {B₀ : Matrix ι ι ℂ}
    (hB : ∀ i j, Tendsto (fun t => B t i j) l (𝓝 (B₀ i j)))
    (h₀ : B₀.det ≠ 0) : ∀ᶠ t in l, Function.Injective (B t).mulVec := by
…

theorem OAI.Nagata.Workers.W11.eventually_injective_of_nonzero_minor line 106

Source documentation

The rectangular version used by the manuscript: an explicit square row minor with nonzero limiting determinant suffices. No finiteness assumption on the row set is needed for this implication.

theorem eventually_injective_of_nonzero_minor {l : Filter α}
    {B : α → Matrix κ ι ℂ} {B₀ : Matrix κ ι ℂ} (row : ι → κ)
    (hB : ∀ i j, Tendsto (fun t => B t i j) l (𝓝 (B₀ i j)))
    (h₀ : (B₀.submatrix row id).det ≠ 0) :
    ∀ᶠ t in l, Function.Injective (B t).mulVec := by
…

theorem OAI.Nagata.Workers.W11.eventually_injective_of_left_inverse line 120

Source documentation

Multiplication by a fixed left inverse reduces the rectangular problem to the square determinant theorem.

theorem eventually_injective_of_left_inverse [Fintype κ]
    {l : Filter α} {B : α → Matrix κ ι ℂ} {B₀ : Matrix κ ι ℂ}
    (C : Matrix ι κ ℂ) (hC : C * B₀ = 1)
    (hB : ∀ i j, Tendsto (fun t => B t i j) l (𝓝 (B₀ i j))) :
    ∀ᶠ t in l, Function.Injective (B t).mulVec := by
…

theorem OAI.Nagata.Workers.W11.eventually_injective_of_injective_limit line 138

Source documentation

Full column rank of the limiting finite complex matrix implies eventual full column rank under entrywise convergence. This closes the finite-matrix implication in prop:matrix-limit without assuming a preselected minor.

theorem eventually_injective_of_injective_limit [Fintype κ] [DecidableEq κ]
    {l : Filter α} {B : α → Matrix κ ι ℂ} {B₀ : Matrix κ ι ℂ}
    (hB : ∀ i j, Tendsto (fun t => B t i j) l (𝓝 (B₀ i j)))
    (h₀ : Function.Injective B₀.mulVec) :
    ∀ᶠ t in l, Function.Injective (B t).mulVec := by
…

theorem OAI.Nagata.Workers.W11.not_eventually_nonzero_kernel_of_injective_limit line 153

Source documentation

Collision supplies nonzero kernel vectors independently for each parameter; their continuity is unnecessary. Together with an injective limiting matrix, even eventual existence of such vectors is impossible.

theorem not_eventually_nonzero_kernel_of_injective_limit
    [Fintype κ] [DecidableEq κ] {l : Filter α} [NeBot l]
    {B : α → Matrix κ ι ℂ} {B₀ : Matrix κ ι ℂ}
    (hB : ∀ i j, Tendsto (fun t => B t i j) l (𝓝 (B₀ i j)))
    (h₀ : Function.Injective B₀.mulVec) :
    ¬ (∀ᶠ t in l, ∃ v : ι → ℂ, v ≠ 0 ∧ (B t).mulVec v = 0) := by
…

theorem OAI.Nagata.Workers.W11.det_mul_eq_zero_of_all_maximal_minors_zero line 180
Source documentation
If every maximal row minor of a rectangular matrix vanishes, multiplying on the left by any matrix to make it square still gives determinant zero.
```
theorem det_mul_eq_zero_of_all_maximal_minors_zero [CommRing K]
    (A : Matrix ρ κ K) (C : Matrix κ ρ K)
    (hA : ∀ s : κ → ρ, Matrix.det (fun i j => A (s i) j) = 0) :
    (C * A).det = 0 := by
…
```
theorem OAI.Nagata.Workers.W11.exists_nonzero_kernel_of_all_maximal_minors_zero line 201
Source documentation
A finite rectangular matrix over a field whose maximal row minors all vanish has a nonzero vector in its kernel. No nonempty-column assumption is necessary: in zero columns the hypothesis itself is false.
```
theorem exists_nonzero_kernel_of_all_maximal_minors_zero [Field K]
    (A : Matrix ρ κ K)
    (hA : ∀ s : κ → ρ, Matrix.det (fun i j => A (s i) j) = 0) :
    ∃ c : κ → K, c ≠ 0 ∧ A.mulVec c = 0 := by
…
```

theorem OAI.Nagata.Workers.W11.exists_nonzero_kernel_coordinates_of_all_maximal_minors_zero line 221

Source documentation

Coordinate form matching the affine-jet incidence interface.

theorem exists_nonzero_kernel_coordinates_of_all_maximal_minors_zero [Field K]
    (A : Matrix ρ κ K)
    (hA : ∀ s : κ → ρ, Matrix.det (fun i j => A (s i) j) = 0) :
    ∃ c : κ → K, c ≠ 0 ∧ ∀ i, ∑ j, A i j * c j = 0 := by
…

theorem OAI.Nagata.Workers.W11.all_maximal_minors_zero_of_card_lt line 230
Source documentation
In an underdetermined finite matrix every maximal row selection repeats a row, so all its maximal minors vanish. This includes the empty-row case.
```
theorem all_maximal_minors_zero_of_card_lt [CommRing K]
    (A : Matrix ρ κ K) (hcard : Fintype.card ρ < Fintype.card κ) :
    ∀ s : κ → ρ, Matrix.det (fun i j => A (s i) j) = 0 := by
…
```
theorem OAI.Nagata.Workers.W11.exists_nonzero_kernel_of_fewer_rows line 241
Source documentation
Fewer equations than unknowns gives a nonzero solution, using exactly the same maximal-minor criterion as the incidence construction.
```
theorem exists_nonzero_kernel_of_fewer_rows [Field K]
    (A : Matrix ρ κ K) (hcard : Fintype.card ρ < Fintype.card κ) :
    ∃ c : κ → K, c ≠ 0 ∧ A.mulVec c = 0 :=
…
```
theorem OAI.Nagata.Workers.W11.not_nonzero_kernel_of_isEmpty_columns line 250
Source documentation
With no unknowns there is no nonzero coefficient vector, as required by the nonzero-curve incidence convention.
```
theorem not_nonzero_kernel_of_isEmpty_columns [CommRing K] [IsEmpty κ]
    (A : Matrix ρ κ K) : ¬ ∃ c : κ → K, c ≠ 0 ∧ A.mulVec c = 0 := by
…
```
theorem OAI.Nagata.Workers.W11.not_all_maximal_minors_zero_of_isEmpty_columns line 258
Source documentation
With no unknowns the unique zero-by-zero maximal minor is one, so the determinantal vanishing condition is false over a nontrivial ring.
```
theorem not_all_maximal_minors_zero_of_isEmpty_columns
    [CommRing K] [Nontrivial K] [IsEmpty κ]
    (A : Matrix ρ κ K) :
    ¬ ∀ s : κ → ρ, Matrix.det (fun i j => A (s i) j) = 0 := by
…
```
theorem OAI.Nagata.Workers.W11.exists_nonzero_maximal_minor_of_injective line 268
Source documentation
The exact nonzero-minor existence statement used in the manuscript's matrix-limit proof, derived from injectivity rather than assumed.
```
theorem exists_nonzero_maximal_minor_of_injective [Field K]
    (A : Matrix ρ κ K) (hA : Function.Injective A.mulVec) :
    ∃ s : κ → ρ, Matrix.det (fun i j => A (s i) j) ≠ 0 := by
…
```