FullMatrixCyclicity.lean

1 import KomorebiVerification.MathlibImports
2 
3 /-!
4 # Cyclicity for the full matrix algebra
5 
6 Every nonzero vector in a finite-dimensional coordinate space is cyclic for
7 the natural action of the full matrix algebra.  Concretely, if `x ≠ 0`, then
8 for every target vector `y` there is a matrix `A` with `A *ᵥ x = y`.
9 -/
10 
11 set_option autoImplicit false
12 
13 namespace Komorebi.FullMatrixCyclicity
14 
15 universe u v
16 
17 variable {K : Type u} [Field K]
18 variable {ι : Type v} [Fintype ι] [DecidableEq ι]
19 
20 /-- A vector is cyclic for the natural action of the full matrix algebra. -/
21 def IsCyclic (x : ι → K) : Prop :=
22   ∀ y : ι → K, ∃ A : Matrix ι ι K, Matrix.mulVec A x = y
23 
24 /-- Every nonzero vector is cyclic under the full matrix algebra. -/
25 theorem isCyclic_of_ne_zero {x : ι → K} (hx : x ≠ 0) : IsCyclic x := by
26   obtain ⟨j, hj⟩ : ∃ j, x j ≠ 0 := by
27     by_contra h
28     apply hx
29     funext i
30     by_contra hi
31     exact h ⟨i, hi⟩
32   intro y
33   let A : Matrix ι ι K := fun i k ↦ if k = j then y i / x j else 0
34   refine ⟨A, ?_⟩
35   funext i
36   simp [A, Matrix.mulVec, dotProduct, hj]
37 
38 end Komorebi.FullMatrixCyclicity
39 
40 #print axioms Komorebi.FullMatrixCyclicity.isCyclic_of_ne_zero

Back to source controls