/-- The basis of the path algebra together with zero: either a path `p` from some vertex `a` tosome vertex `b` (recorded with its endpoints), or `none`, standing for `0`. -/abbrev PathOrZero (V : Type u) [Quiver.{v + 1} V] := Option (Σ a b : V, Quiver.Path a b)
/-- The product of basis paths in `kQ`, with the convention used in the lesson: `p · q` means"first `p`, then `q`", defined when `p` ends where `q` starts, and `0` otherwise. (Many booksuse the opposite order; the two conventions give opposite algebras.) -/def pmul : PathOrZero V → PathOrZero V → PathOrZero V | some ⟨a, b, p⟩, some ⟨c, d, q⟩ => if h : b = c then some ⟨a, d, p.comp (h ▸ q)⟩ else none | _, _ => none
pmul_assoctheoremProved here from basic factspropext
pmul_assocLean 4Proved here from basic factsFormally verified
/-- **The multiplication of paths is associative**, including the cases where some product is`0`. Human proof: `(p · q) · r` and `p · (q · r)` are both defined exactly when `p` ends where `q`starts and `q` ends where `r` starts, and then both equal the concatenation `pqr`, byassociativity of concatenation (`Quiver.Path.comp_assoc`). Extended bilinearly, this makes `kQ`an associative algebra. -/theorem pmul_assoc (x y z : PathOrZero V) : pmul (pmul x y) z = pmul x (pmul y z) := by rcases x with _ | ⟨a, b, p⟩ · rfl rcases y with _ | ⟨c, d, q⟩ · simp [pmul] rcases z with _ | ⟨e, f, r⟩ · by_cases h : b = c · subst h; simp [pmul] · simp [pmul, h] by_cases h1 : b = c · subst h1 by_cases h2 : d = e · subst h2 simp [pmul, Quiver.Path.comp_assoc] · simp [pmul, h2] · by_cases h2 : d = e · subst h2 simp [pmul, h1] · simp [pmul, h1, h2]
idempotentstheoremProved here from basic factspropext
idempotentsLean 4Proved here from basic factsFormally verified
/-- **The trivial paths `eₐ` are orthogonal idempotents**: `eₐ · eₐ = eₐ` and `eₐ · e_b = 0` for`a ≠ b`. (For a finite quiver their sum is the identity of `kQ`.) -/theorem idempotents (a b : V) : pmul (some ⟨a, a, Quiver.Path.nil⟩) (some ⟨b, b, Quiver.Path.nil⟩) = if a = b then some ⟨a, a, Quiver.Path.nil⟩ else none := by by_cases h : a = b · subst h; simp [pmul] · simp [pmul, h]
concat_assoctheoremApplies a library theoremNo axioms
concat_assocLean 4Applies a library theoremFormally verified
/-- Concatenation of paths is associative: Mathlib's `Quiver.Path.comp_assoc`. (Mathlib's`p.comp q` is "first `p`, then `q`".) -/theorem concat_assoc {V : Type u} [Quiver.{v + 1} V] {a b c d : V} (p : Quiver.Path a b) (q : Quiver.Path b c) (r : Quiver.Path c d) : (p.comp q).comp r = p.comp (q.comp r) := Quiver.Path.comp_assoc p q r
path_length_letheoremProved here from basic factspropext, Quot.sound
path_length_leLean 4Proved here from basic factsFormally verified
/-- **Acyclic quivers have bounded paths.** If every arrow strictly increases a height function`h : V → ℕ`, then every path from `a` to `b` has length at most `h b - h a`. Such a function existsfor every finite quiver without oriented cycles (number the vertices compatibly with the arrows),so then paths have length less than the number of vertices, and with finitely many arrows thereare only finitely many paths: `kQ` is finite-dimensional. Proof: induction on the path. -/theorem path_length_le {V : Type u} [Quiver.{v + 1} V] (h : V → ℕ) (hh : ∀ {a b : V}, (a ⟶ b) → h a < h b) {a b : V} (p : Quiver.Path a b) : h a + p.length ≤ h b := by induction p with | nil => simp | cons p e ih => rw [Quiver.Path.length_cons] have := hh e omega
/-- The powers `cⁿ = c c ⋯ c` of a cycle `c` at a vertex `a`. -/def cyclePow {V : Type u} [Quiver.{v + 1} V] {a : V} (c : Quiver.Path a a) : ℕ → Quiver.Path a a | 0 => Quiver.Path.nil | n + 1 => (cyclePow c n).comp c
cycle_infinitetheoremProved here from basic factspropext, Classical.choice, Quot.sound
cycle_infiniteLean 4Proved here from basic factsFormally verified
/-- **A cycle makes `kQ` infinite-dimensional.** If `c` is an oriented cycle of positive length,its powers `cⁿ` have lengths `n · length c`, all different, so there are infinitely many pathsfrom `a` to `a`. With the previous theorem: a finite quiver has finite-dimensional path algebraexactly when it has no oriented cycles. -/theorem cycle_infinite {V : Type u} [Quiver.{v + 1} V] {a : V} (c : Quiver.Path a a) (hc : 0 < c.length) : Infinite (Quiver.Path a a) := by have hlen : ∀ n : ℕ, (cyclePow c n).length = n * c.length := by intro n induction n with | zero => simp [cyclePow] | succ n ih => rw [cyclePow, Quiver.Path.length_comp, ih, Nat.succ_mul] refine Infinite.of_injective (cyclePow c) fun m n hmn => ?_ have := congrArg Quiver.Path.length hmn rw [hlen, hlen] at this exact Nat.eq_of_mul_eq_mul_right hc this
/-- The arrows of `Aₙ`: there is an arrow from `i` to `j` exactly when `j = i + 1`. -/instance linAQuiver (n : ℕ) : Quiver (LinA n) where Hom i j := PLift ((j : Fin n).val = (i : Fin n).val + 1)
lin_a_lengththeoremProved here from basic factspropext, Quot.sound
lin_a_lengthLean 4Proved here from basic factsFormally verified
/-- **Paths in `Aₙ`.** Every path from `i` to `j` in the linearly oriented quiver has lengthexactly `j - i`; in particular paths `i → j` exist only for `i ≤ j`. (There is in fact exactlyone for each `i ≤ j`, so `kAₙ` has dimension `n(n+1)/2` and is isomorphic to the algebra of uppertriangular `n × n` matrices.) Proof: induction on the path, each arrow adding `1`. -/theorem lin_a_length {n : ℕ} {i j : LinA n} (p : Quiver.Path i j) : (i : Fin n).val + p.length = (j : Fin n).val := by induction p with | nil => simp | cons p e ih => rw [Quiver.Path.length_cons] have := e.down omega
rep_extendstheoremApplies a library theorempropext, Quot.sound
rep_extendsLean 4Applies a library theoremFormally verified
/-- **Representations of `Q` are functors out of the path category.** A representation — aprefunctor `ρ : Q ⥤q ModuleCat k` — extends to a functor `F` on the free category `Paths Q`(paths act by composites of the arrow maps), and `F` is the unique functor that restricts to `ρ`on arrows. Mathlib: `Paths.lift`, `Paths.lift_spec`, `Paths.lift_unique`. Linearising, a functor`Paths Q ⥤ ModuleCat k` is the same as a `kQ`-module — the equivalence proved in the lesson. -/theorem rep_extends {Q : Type u} [Quiver.{w} Q] {k : Type v} [Field k] (ρ : Q ⥤q ModuleCat.{v} k) : ∃ F : Paths Q ⥤ ModuleCat.{v} k, Paths.of Q ⋙q F.toPrefunctor = ρ ∧ ∀ G : Paths Q ⥤ ModuleCat.{v} k, Paths.of Q ⋙q G.toPrefunctor = ρ → G = F := ⟨Paths.lift ρ, Paths.lift_spec ρ, fun G hG => Paths.lift_unique ρ G hG⟩
/-- If every arrow increases a height function, paths are short.Hint: `induction p with | nil => simp | cons p e ih => ?_`; in the second case rewrite with`Quiver.Path.length_cons`, record `hh e`, and finish with `omega`. -/theorem path_length_le {V : Type*} [Quiver V] (h : V → ℕ) (hh : ∀ {a b : V}, (a ⟶ b) → h a < h b) {a b : V} (p : Quiver.Path a b) : h a + p.length ≤ h b := by sorry
Show the compiled solution
path_length_leLean 4Proved here from basic factsFormally verified
/-- **Acyclic quivers have bounded paths.** If every arrow strictly increases a height function`h : V → ℕ`, then every path from `a` to `b` has length at most `h b - h a`. Such a function existsfor every finite quiver without oriented cycles (number the vertices compatibly with the arrows),so then paths have length less than the number of vertices, and with finitely many arrows thereare only finitely many paths: `kQ` is finite-dimensional. Proof: induction on the path. -/theorem path_length_le {V : Type u} [Quiver.{v + 1} V] (h : V → ℕ) (hh : ∀ {a b : V}, (a ⟶ b) → h a < h b) {a b : V} (p : Quiver.Path a b) : h a + p.length ≤ h b := by induction p with | nil => simp | cons p e ih => rw [Quiver.Path.length_cons] have := hh e omega
/-- Every path from `i` to `j` in the linear quiver `Aₙ` has length `j - i`.Hint: the same induction; an arrow `e : b ⟶ c` carries the proof `e.down : c.val = b.val + 1`. -/theorem lin_a_length {n : ℕ} {i j : LinA n} (p : Quiver.Path i j) : (i : Fin n).val + p.length = (j : Fin n).val := by sorry
Show the compiled solution
lin_a_lengthLean 4Proved here from basic factsFormally verified
/-- **Paths in `Aₙ`.** Every path from `i` to `j` in the linearly oriented quiver has lengthexactly `j - i`; in particular paths `i → j` exist only for `i ≤ j`. (There is in fact exactlyone for each `i ≤ j`, so `kAₙ` has dimension `n(n+1)/2` and is isomorphic to the algebra of uppertriangular `n × n` matrices.) Proof: induction on the path, each arrow adding `1`. -/theorem lin_a_length {n : ℕ} {i j : LinA n} (p : Quiver.Path i j) : (i : Fin n).val + p.length = (j : Fin n).val := by induction p with | nil => simp | cons p e ih => rw [Quiver.Path.length_cons] have := e.down omega