An edge operator moves data between named packets. An exact coordinate change describes the same data in another complete chart. A connection supplies an additional choice of transport. The three can use similar arrows while making different mathematical assertions.
Reading the drawing
The three panels show a supported matrix entry, one ambient vector in three frames, and an independently chosen loop transport. Similar arrows carry different mathematical data.
Drawing labels and data 20 labels
Read the original labels as selectable text. Tables preserve grid relationships; other short labels are grouped compactly.
EDGE
ACTION
EXACT
COORDINATES
CHOSEN
CONNECTION
| Row / column | Column 1 | Column 2 | Column 3 |
|---|---|---|---|
| Row 1 | \(0\) | \(0\) | \(0\) |
| Row 2 | \(2\) | \(0\) | \(0\) |
| Row 3 | \(0\) | \(0\) | \(0\) |
- \(e_0\longmapsto2e_1\)
- \((3,2)\)
- \((1,2)\)
- \((3/2,1/2)\)
- one unchanged ambient vector
- \((1,1)\)
Evidence note from the source edition
Three actual models used below: a single supported matrix entry, one ambient vector in three coordinate systems, and a shear obtained as chosen loop transport. The coordinates in the middle are not three different ambient vectors.
One paper, three tests
For an edge word, ask whether the target of each step matches the source of the next. For exact coordinates, ask whether analysis and synthesis are inverses. For a connection, ask whether its transports through two steps agree with its declared direct transports. None of these tests can replace another.
This guide follows explicit integer and rational matrices through these tests. Each example has an inspectable input, calculation, and conclusion. Vector drawings display those calculations rather than replace them. A graph with two paths can have zero net transfer. A loop with trace two and determinant one can still differ from the identity.
The edition used here
The worked models originate in the finite algebraic v1.0.1 release. The final traditional paper also develops rooted tree expansions, nonlinear defects, obstruction objects, filtered lifting, and analytic transport under their stated hypotheses. Those ordinary mathematical developments have a wider scope than the finite Lean contract. The present models explain the finite mechanisms and provide a route into the broader paper.
Read this as
Follow the object, not the arrow shape. A typed transfer can vanish, a complete coordinate loop must telescope, and an independently chosen connection can have genuine algebraic holonomy.