funlean.
Step 36 / 64

University

Vectors and subspaces

Vectors can be added and scaled; a subspace stays closed under those operations.

Start with a concrete example

Horizontal arrows can be added or stretched and still remain horizontal. They form a smaller space inside the plane of all arrows. Rotating by 90° takes them out of that horizontal space.

A small check: try the idea

Think with the concrete example above. You can try again.

Does a 90° turn preserve the collection of all horizontal arrows?

Read the answer and reasoning

No; nonzero horizontal arrows become vertical. Staying in a subspace means the resulting arrow remains in that collection. Sharing a starting point is not enough.

Build the idea in three steps

  1. An ordinary arrow has two coordinates. Arrows can be added and multiplied by numbers.
  2. A vector space generalizes those two operations. In this proof the scalars can be residues modulo a prime, rather than real numbers.
  3. A subspace contains zero and stays closed under addition and scaling. A stable subspace also stays closed under the symmetries.

A small example

All horizontal arrows form a subspace of the plane. A quarter-turn sends them vertically, so it does not preserve that subspace.

Lean definition · original excerpt

Mathlib · db584cd · Defs.lean

structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v    extends AddSubmonoid M, SubMulAction R M

How to read this Lean

A Submodule is the module version of a linear subspace. Its fields encode closure under the relevant operations. The ambient Module supplies addition and scalar multiplication.

Original source ↗ · L41–42Open the complete saved source

Where this idea is used

6. The scissors incident9. Two doors to the concert10. A three-note audition11. Borrow a better passport12. The workshops agree13. Pip’s impossible quilt14. The shrinking reservation
I’m lost · Help

Mika’s help desk

Vectors and subspaces

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Vectors can be added and scaled; a subspace stays closed under those operations.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

All horizontal arrows form a subspace of the plane. A quarter-turn sends them vertically, so it does not preserve that subspace.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →