| ← Ch. 10: Modules | Table of contents | Ch. 12: Working Efficiently → |
This chapter combines everything covered so far: inductive types (Chapter 1), structures (Chapter 2), and rings (Chapters 7–8), used to build a genuinely interesting example: the path algebra of a quiver.
Learning objectives. By the end of this chapter, encode a quiver as a
structure of vertices/arrows/source/target, define Path as an
inductive type indexed by its own endpoints, compose paths via
Path.append and predict when the composability side-conditions block a
nonsensical composition, and explain in what sense a path algebra $kQ$
extends the Ring/Module machinery of Chapters 8 and 10.
Sections
- What is a quiver?
- Paths
- Defining a quiver in Lean
- Paths as an inductive type indexed by source and target
- Path composition
- Exercises
- Checkpoint project: path length, and composition respects it
| ← Ch. 10: Modules | Table of contents | Ch. 12: Working Efficiently → |