Add some TODOs

MIL/C09_Linear_Algebra/S02_Subspaces.lean

@@ -396,10 +396,10 @@ attribute [gcongr] comap_mono
 
 example : Submodule K (V ⧸ E) ≃ { F : Submodule K V // E ≤ F } where
 /- EXAMPLES:
-  toFun := _
-  invFun := _
-  left_inv := _
-  right_inv := _
+  toFun := sorry
+  invFun := sorry
+  left_inv := sorry
+  right_inv := sorry
 SOLUTIONS: -/
   toFun F := ⟨comap E.mkQ F, by
     conv_lhs => rw [← E.ker_mkQ, ← comap_bot]

MIL/C09_Linear_Algebra/S03_Endomorphisms.lean

@@ -27,11 +27,10 @@ variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]
 variable {W : Type*} [AddCommGroup W] [Module K W]
 
 
-section endomorphisms
 open Polynomial Module LinearMap
 
 example (φ ψ : End K V) : φ * ψ = φ ∘ₗ ψ :=
-  LinearMap.mul_eq_comp φ ψ -- rfl would also work
+  LinearMap.mul_eq_comp φ ψ -- `rfl` would also work
 
 -- evaluating `P` on `φ`
 example (P : K[X]) (φ : End K V) : V →ₗ[K] V :=
@@ -58,7 +57,7 @@ EXAMPLES: -/
 
 example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) : ker (aeval φ P) ⊓ ker (aeval φ Q) = ⊥ := by
 /- EXAMPLES:
-    sorry
+  sorry
 SOLUTIONS: -/
   rw [Submodule.eq_bot_iff]
   rintro x hx
@@ -76,7 +75,7 @@ SOLUTIONS: -/
 example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) :
     ker (aeval φ P) ⊔ ker (aeval φ Q) = ker (aeval φ (P*Q)) := by
 /- EXAMPLES:
-    sorry
+  sorry
 SOLUTIONS: -/
   apply le_antisymm
   · apply sup_le
@@ -117,7 +116,8 @@ However an eigenvector is, by definition, a non-zero element of an eigenspace. T
 predicate is ``End.HasEigenvector``.
 EXAMPLES: -/
 -- QUOTE:
-example (φ : End K V) (a : K) : φ.eigenspace a = LinearMap.ker (φ - algebraMap K (End K V) a) :=
+example (φ : End K V) (a : K) :
+    φ.eigenspace a = LinearMap.ker (φ - algebraMap K (End K V) a) :=
   rfl
 
 
@@ -140,13 +140,16 @@ example (φ : End K V) : φ.Eigenvalues = {a // φ.HasEigenvalue a} :=
 example (φ : End K V) (a : K) : φ.HasEigenvalue a → (minpoly K φ).IsRoot a :=
   φ.isRoot_of_hasEigenvalue
 
--- In finite dimension, the converse is also true
-example [FiniteDimensional K V] (φ : End K V) (a : K) : φ.HasEigenvalue a ↔ (minpoly K φ).IsRoot a :=
+-- In finite dimension, the converse is also true (we will discuss dimension below)
+example [FiniteDimensional K V] (φ : End K V) (a : K) :
+    φ.HasEigenvalue a ↔ (minpoly K φ).IsRoot a :=
   φ.hasEigenvalue_iff_isRoot
 
 -- Cayley-Hamilton
 example [FiniteDimensional K V] (φ : End K V) : aeval φ φ.charpoly = 0 :=
   φ.aeval_self_charpoly
 
-end endomorphisms
 -- QUOTE.
+
+-- TODO: Add an exercise here. Maybe say that an endormorphism whose minimal polynomial
+-- splits with simple roots is diagonalizable? Needs the full kernels lemma.

MIL/C09_Linear_Algebra/S04_Bases.lean

@@ -19,6 +19,8 @@ Matrices
 
 .. index:: matrices
 
+TODO: make text for this section
+
 Beware the matrix notation list rows but the vector notation
 is neither a row vector nor a column vector. Multiplication of a matrix with a vector
 from the left (resp. right) interprets the vector as a row (resp. column) vector.
@@ -74,21 +76,6 @@ example : !![(1 : ℝ), 2; 3, 4].trace = 5 := by
   simp [trace]
   norm_num
 
--- variable {R : Type*} [AddCommMonoid R]
--- @[simp]
--- theorem trace_fin_one_of (a : R) : trace !![a] = a :=
---   trace_fin_one _
---
--- @[simp]
--- theorem trace_fin_two_of (a b c d : R) : trace !![a, b; c, d] = a + d :=
---   trace_fin_two _
---
--- @[simp]
--- theorem trace_fin_three_of (a b c d e f g h i : R) :
---     trace !![a, b, c; d, e, f; g, h, i] = a + e + i :=
---   trace_fin_three _
-
--- L’exemple ci-dessous est très décevant sans les lemmes ci-dessus (qui sont proposés dans Mathlib)
 #norm_num !![(1 : ℝ), 2; 3, 4].trace
 
 variable (a b c d : ℝ) in
@@ -330,6 +317,9 @@ example (φ : V →ₗ[K] W) (v : V) : (toMatrix B B' φ) *ᵥ (B.repr v) = B'.r
   toMatrix_mulVec_repr B B' φ v
 end
 -- QUOTE.
+
+-- TODO: Need some exercises for this section
+
 /- TEXT:
 
 Dimension
@@ -513,6 +503,8 @@ example [FiniteDimensional K V] :
     (FiniteDimensional.finrank K V : Cardinal) = Module.rank K V :=
   finrank_eq_rank K V
 -- QUOTE.
+
+-- TODO: Decide what to do about the topics below.
 /-