C10 — Linear Algebra: Summary Notes

Table of Contents

• Part I — Vector Spaces, Linear Maps, and Products (S01)
  • Vector Spaces as Modules
    • Distribution property
    • Commutativity property
    • Module over ideals/submodules
    • Module over Ring vs. Semiring
  • Linear Maps
    • Linear maps form a vector space
    • Composition
    • Constructing a linear map from scratch
    • Internal vs. user-facing lemmas
    • lsmul
  • Linear Equivalence
  • Binary Products
    • Projection maps
    • Universal property of the product
    • Parallel combination (prodMap)
    • Inclusion maps
    • Universal property of the sum (coproduct)
  • Vector Families (DirectSum)
    • Direct sum (finite support)
    • Product (infinite support)
    • Projection, inclusion, and single
    • Sum vs. product
• Part II — Submodules, Linear Maps, and Quotient Spaces (S02)
  • Submodules (Subspaces)
    • Closure properties
    • Example: ℝ as a submodule of ℂ
    • Preimage of a submodule under a linear map
    • A submodule is itself a vector space
  • Lattice Operations on Submodules
    • Intersection (⊓)
    • Union / span (⊔)
    • Top (⊤) and bottom (⊥)
    • Complementary submodules (IsCompl)
    • Internal direct sum (DirectSum.IsInternal)
    • Span as the smallest containing submodule
    • Decomposing an element of S ⊔ T
  • Linear Maps Between Vector Spaces
    • Image (map) and preimage (comap) of a submodule
    • Range and kernel, expressed via map/comap
    • Injectivity and surjectivity criteria
    • Membership lemmas
    • Galois connection: map φ E ≤ F ↔ E ≤ comap φ F
  • Quotient Spaces
    • The quotient is a vector space
    • Canonical projection (mkQ)
    • Universal properties: liftQ and mapQ
    • map_comap_eq and comap_map_eq
    • Open exercise: submodules of the quotient
• Part III — Endomorphisms (S03)
  • Endomorphisms
    • Multiplication is composition
  • Polynomial Evaluation on Endomorphisms (aeval)
    • aeval is an algebra homomorphism
  • Toolbox: Subspace Lemmas
  • Theorem 1: Coprime evaluations have trivially intersecting kernels
    • Proof walkthrough
  • Theorem 2: Supremum of kernels is the kernel of the product
    • Proof walkthrough
• Part IV — Bases (S04)
  • Bases and Coordinates
    • Constructing a basis
    • Canonical bases
    • Reconstructing a vector from its coordinates
  • Linear Combinations
    • Linear combination with general vectors
    • Linear combination with a basis
  • Linear Maps Constructed from a Basis
    • Extension by linearity (B.constr)
    • Maps agreeing on a basis are equal (B.ext)
  • Matrices Representing Linear Maps
    • The matrix of a linear map (toMatrix)
    • Change of basis
    • Composition corresponds to matrix multiplication
    • The determinant of an endomorphism is basis-independent
  • Finite Rank of Vector Spaces
    • The archetypical n-dimensional space
    • The scalar field matters
    • Positivity of rank
    • Finite basis ⇔ finite-dimensional
  • Finite Rank of Submodules

Merged notes for Chapter 10 of Mathematics in Lean, generated from the comments in C10-S01.lean–C10-S04.lean. The individual section notes (S10-1.md, S10-2.md, S10-3.md, S10-4.md) remain available alongside this file.

Part I — Vector Spaces, Linear Maps, and Products (S01)

Summary generated from the comments in C10-S01.lean.

Vector Spaces as Modules

A vector space V over a field K is a special case of a module, instantiated as Module K V:

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

Class in Module	Instantiated by (vector space)
AddCommMonoid (the object)	AddCommGroup V
Semiring (the scalars)	Field K

NOTE

Semiring is a Ring without the inverse property for + in AddCommMonoid. Upgrading the scalars from Semiring to Field and the object from AddCommMonoid to AddCommGroup is exactly what turns a module into a vector space.

Distribution property

Scalar multiplication • distributes over + on both sides — the operator • defined in Module describes the interaction between the AddCommMonoid object and the Semiring scalars:

Lemma	Statement
smul_add	a • (u + v) = a • u + a • v
add_smul	(a + b) • u = a • u + b • u

Commutativity property

Since Field is commutative, scalar multiplication is commutative in the scalars:

• smul_comm: a • b • u = b • a • u

Module over ideals/submodules

The following somewhat surprising instance holds:

example {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] :
    Module (Ideal R) (Submodule R M) :=
  inferInstance

Module (Ideal R) (Submodule R M) holds because:

1. Submodule R M is itself a Module, instantiating the AddCommMonoid that Module extends.
2. Ideal R is a CommSemiring, instantiating the scalar Semiring (since CommSemiring extends Semiring).

Module over Ring vs. Semiring

Scalars	Object required	Why
Ring R	AddCommGroup M	the object of a Ring is an AddCommGroup
Semiring R	AddCommMonoid M	the object of a Semiring is an AddCommMonoid

Over a Ring the module automatically has additive inverses; over a Semiring it does not.

Linear Maps

Let W be another vector space over the same field K. A linear map φ : V →ₗ[K] W satisfies two properties:

Property	Lemma	Statement
Homogeneity	map_smul	φ (a • v) = a • φ v
Additivity	map_add	φ (v + w) = φ v + φ w

Linear maps form a vector space

V →ₗ[K] W is itself a vector space, satisfying:

1. 0 ∈ V →ₗ[K] W — the zero map sending everything in V to 0 in W.
2. ∀ x y ∈ V →ₗ[K] W, x + y ∈ V →ₗ[K] W — addition closure.
3. ∀ a ∈ K, x ∈ V →ₗ[K] W, a • x ∈ V →ₗ[K] W — scalar multiplication closure.

For example, linear combinations of linear maps are linear maps:

#check (2 • φ + ψ : V →ₗ[K] W)

Composition

∘ₗ composes linear maps into another linear map. The two spellings are equivalent:

variable (θ : W →ₗ[K] V)
#check (φ.comp θ : W →ₗ[K] W)
#check (φ ∘ₗ θ : W →ₗ[K] W)

Constructing a linear map from scratch

Example: the homothety toFun v := 3 • v as a term of V →ₗ[K] V:

example : V →ₗ[K] V where
  toFun v := 3 • v
  map_add' _ _ := smul_add ..
  map_smul' _ _ := smul_comm ..

The two proof obligations are:

• map_add': toFun (a + b) = toFun a + toFun b, i.e. 3 • (a + b) = 3 • a + 3 • b, proved by smul_add ...
• map_smul': toFun (a • b) = a • toFun b, i.e. 3 • (a • b) = a • (3 • b), proved by smul_comm ...

Internal vs. user-facing lemmas

Lemma	Kind	Statement
φ.map_add'	internal proposition	∀ x y : V, φ.toFun (x + y) = φ.toFun x + φ.toFun y
φ.map_add	derived, user-facing	∀ x y : V, φ (x + y) = φ x + φ y

map_add φ is the same as φ.map_add — dot notation and first-argument application coincide.

lsmul

LinearMap.lsmul K V : K →ₗ[K] V →ₗ[K] V turns scalar multiplication into a bilinear map; partially applied, LinearMap.lsmul K V 3 : V →ₗ[K] V is the homothety v ↦ 3 • v.

#check (LinearMap.lsmul K V : K →ₗ[K] V →ₗ[K] V)
#check (LinearMap.lsmul K V 3 : V →ₗ[K] V)

Linear Equivalence

A linear equivalence f : V ≃ₗ[K] W is a bijective linear map bundled with its (also linear) inverse.

• Composing with the inverse gives the identity:$$f\circ f^{-1}=\mathrm{id}$$

  example (f : V ≃ₗ[K] W) : f ≪≫ₗ f.symm = LinearEquiv.refl K V :=
    f.self_trans_symm

• A bijective linear map upgrades to a linear equivalence:

  noncomputable example (f : V →ₗ[K] W) (h : Function.Bijective f) : V ≃ₗ[K] W :=
    .ofBijective f h

Binary Products

Throughout this section, V, W, U, T are vector spaces over the same field K.

Projection maps

example : V × W →ₗ[K] V := LinearMap.fst K V W   -- first projection
example : V × W →ₗ[K] W := LinearMap.snd K V W   -- second projection

Universal property of the product

Given φ : U →ₗ[K] V and ψ : U →ₗ[K] W, LinearMap.prod φ ψ : U →ₗ[K] V × W is the unique map such that:

$$\mathsf{fst}\circ (\phi \times \psi )=\phi ,\mathsf{snd}\circ (\phi \times \psi )=\psi$$

example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : U →ₗ[K] V × W := LinearMap.prod φ ψ
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.fst K V W ∘ₗ LinearMap.prod φ ψ = φ := rfl
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.snd K V W ∘ₗ LinearMap.prod φ ψ = ψ := rfl

Both equations hold by rfl — the product map does the expected thing on each component, definitionally.

Parallel combination (prodMap)

φ.prodMap ψ : (V × W) →ₗ[K] (U × T) combines φ : V →ₗ[K] U and ψ : W →ₗ[K] T in parallel:

example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) :
    φ.prodMap ψ = (φ ∘ₗ .fst K V W).prod (ψ ∘ₗ .snd K V W) := rfl

Inclusion maps

example : V →ₗ[K] V × W := LinearMap.inl K V W   -- first inclusion
example : W →ₗ[K] V × W := LinearMap.inr K V W   -- second inclusion

Universal property of the sum (coproduct)

Given φ : V →ₗ[K] U and ψ : W →ₗ[K] U, φ.coprod ψ : V × W →ₗ[K] U is the unique map such that:

$$(\phi \bigsqcup \psi )\circ \mathsf{inl}=\phi ,(\phi \bigsqcup \psi )\circ \mathsf{inr}=\psi$$

Lemma	Statement
LinearMap.coprod_inl	φ.coprod ψ ∘ₗ LinearMap.inl K V W = φ
LinearMap.coprod_inr	φ.coprod ψ ∘ₗ LinearMap.inr K V W = ψ

Concretely, the coproduct map adds the two images:

example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) (v : V) (w : W) :
    φ.coprod ψ (v, w) = φ v + ψ w := rfl

TIP

In the category of vector spaces, the binary product and coproduct coincide: the same object V × W is universal in both directions, which is why this section can discuss projections and inclusions side by side.

Vector Families (DirectSum)

V : ι → Type* is a family of vector spaces over K indexed by ι (with DecidableEq ι):

variable {ι : Type*} [DecidableEq ι]
         (V : ι → Type*) [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]

Direct sum (finite support)

Given a family of linear maps φ : Π i, (V i →ₗ[K] W), assemble them into a single map from the direct sum:

example (φ : Π i, (V i →ₗ[K] W)) : (⨁ i, V i) →ₗ[K] W :=
  DirectSum.toModule K ι W φ

This is the universal coproduct of a family of linear maps — the infinitary generalization of coprod.

Product (infinite support)

Given a family of linear maps φ : Π i, (W →ₗ[K] V i), assemble them into a single map into the product:

example (φ : Π i, (W →ₗ[K] V i)) : W →ₗ[K] (Π i, V i) :=
  LinearMap.pi φ

This is the universal product of a family of linear maps — the infinitary generalization of prod.

Projection, inclusion, and single

Map	Type	Role
LinearMap.proj i	(Π j, V j) →ₗ[K] V i	universal projection out of the product
DirectSum.lof K ι V i	V i →ₗ[K] (⨁ i, V i)	universal inclusion into the direct sum
LinearMap.single K V i	V i →ₗ[K] (Π i, V i)	inclusion into the product: x ↦ (fun j => if j = i then x else 0)

Sum vs. product

There is always a linear map (Π j, V j) →ₗ[K] (⨁ i, V i), since (Π j, V j) →ₗ[K] V i →ₗ[K] (⨁ i, V i).

IMPORTANT

Elements of ⨁ i, V i are finitely supported tuples, while elements of Π i, V i may have infinite support — so in general only one direction exists. When ι is a Fintype, every tuple is finitely supported, and the two coincide:

example [Fintype ι] : (⨁ i, V i) ≃ₗ[K] (Π i, V i) :=
  linearEquivFunOnFintype K ι V

$$\underset{i:\iota }{⨁}{V}_i\cong \prod _{i:\iota }{V}_i(\iota \text{ finite})$$

---

Part II — Submodules, Linear Maps, and Quotient Spaces (S02)

Summary generated from the comments in C10-S02.lean.

Throughout, V is a vector space over a field K:

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

Submodules (Subspaces)

Closure properties

A submodule U : Submodule K V is closed under the two vector-space operations:

Closure	Lemma	Statement
addition	U.add_mem	x ∈ U → y ∈ U → x + y ∈ U
scalar multiplication	U.smul_mem	a ∈ K → x ∈ U → a • x ∈ U

Example: ℝ as a submodule of ℂ

Submodule ℝ ℂ instantiates the scalar Semiring with ℝ (a field) and the Module object with ℂ (a vector space over ℝ). It is built from four fields:

noncomputable example : Submodule ℝ ℂ where
  carrier := Set.range ((↑) : ℝ → ℂ)
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m
    simp
  zero_mem' := by
    use 0
    simp
  smul_mem' := by
    rintro c - ⟨a, rfl⟩
    use c*a
    simp

Field	Role	Proof idea
carrier	the underlying set, here Set.range ((↑) : ℝ → ℂ) — the image of the coercion ℝ → ℂ	since the ambient module is ℂ, the carrier must be a subset of ℂ, hence the coercion
add_mem'	closure under +	destruct x, y ∈ carrier as ⟨n, rfl⟩, ⟨m, rfl⟩ (i.e. x = ↑n, y = ↑m), witness x + y = ↑(n + m), close with simp since (↑) preserves addition
zero_mem'	0 ∈ carrier	witness 0 = ↑0, since (↑) preserves zero
smul_mem'	closure under •	destruct x ∈ carrier as ⟨a, rfl⟩, witness c • ↑a = ↑(c * a), since (↑) preserves scalar multiplication

NOTE

The coercion (↑) : ℝ → ℂ behaves like a linear map ℝ →ₗ[ℝ] ℂ here — it preserves +, 0, and • — which is exactly why simp can close each obligation.

Preimage of a submodule under a linear map

Given φ : V →ₗ[K] W and H : Submodule K W, the preimage φ ⁻¹' H is a submodule of V:

Full definition (click to expand)

def preimage {W : Type*} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W) (H : Submodule K W) :
    Submodule K V where
  carrier := φ ⁻¹' H
  zero_mem' := by
    rw [Set.mem_preimage, LinearMap.map_zero]
    exact Submodule.zero_mem H
  add_mem' := by
    rintro a b ha hb
    rw [Set.mem_preimage, LinearMap.map_add] at *
    exact Submodule.add_mem H ha hb
  smul_mem' := by
    rintro c x hx
    rw [Set.mem_preimage, LinearMap.map_smul] at *
    exact Submodule.smul_mem H c hx

Each obligation follows the same pattern: rewrite membership in the preimage via Set.mem_preimage (x ∈ φ⁻¹' H ↔ φ x ∈ H), push φ through +/0/• because φ is linear, then close using the corresponding closure lemma for H.

A submodule is itself a vector space

A submodule U of V is a vector space over the same field K, in two equivalent phrasings:

example (U : Submodule K V) : Module K U := inferInstance
example (U : Submodule K V) : Module K {x : V // x ∈ U} := inferInstance

U (as a Submodule K V) and the subtype {x : V // x ∈ U} carry the same Module K instance.

Lattice Operations on Submodules

Intersection (⊓)

The intersection of two submodules is literally the intersection of their underlying sets:

example (H H' : Submodule K V) :
    ((H ⊓ H' : Submodule K V) : Set V) = (H : Set V) ∩ (H' : Set V) := rfl

Union / span (⊔)

WARNING

Unlike ⊓, the set-theoretic union of two submodules is not generally closed under +/•.

So ⊔ is instead defined as the span of the set union:

example (H H' : Submodule K V) :
    ((H ⊔ H' : Submodule K V) : Set V) = Submodule.span K ((H : Set V) ∪ (H' : Set V)) := by
  simp [Submodule.span_union]

Top (⊤) and bottom (⊥)

• ⊤ : Submodule K V is the whole space: x ∈ (⊤ : Submodule K V) holds trivially for every x.
• ⊥ : Submodule K V is the zero subspace: x ∈ (⊥ : Submodule K V) ↔ x = 0 (Submodule.mem_bot).

Complementary submodules (IsCompl)

If U and V' are complementary (IsCompl U V'), they decompose the ambient space: they span it, and they only meet at 0.

$$U\bigsqcup V^{\prime }=\mathrm{\top }\text{and}U\sqcap V^{\prime }=\mathrm{\perp }$$

example (U V' : Submodule K V) (h : IsCompl U V') : U ⊔ V' = ⊤ := h.sup_eq_top
example (U V' : Submodule K V) (h : IsCompl U V') : U ⊓ V' = ⊥ := h.inf_eq_bot

Internal direct sum (DirectSum.IsInternal)

DirectSum.IsInternal U (for a family U : ι → Submodule K V, with DecidableEq ι) says V decomposes as the internal direct sum of the U i, i.e. (⨁ i, U i) ≃ₗ[K] V. Concretely this means:

1. ⊔ i, U i = ⊤ — the subspaces together span the whole space, and
2. U i ⊓ U j = ⊥ for i ≠ j — the subspaces pairwise intersect only at zero.

example (U : ι → Submodule K V) (h : DirectSum.IsInternal U) :
    ⨆ i, U i = ⊤ := h.submodule_iSup_eq_top

example (U : ι → Submodule K V) (h : DirectSum.IsInternal U) {i j : ι} (hij : i ≠ j) :
    U i ⊓ U j = ⊥ :=
  (h.submodule_iSupIndep.pairwiseDisjoint hij).eq_bot

noncomputable example (U : ι → Submodule K V) (h : DirectSum.IsInternal U) :
    (⨁ i, U i) ≃ₗ[K] V :=
  LinearEquiv.ofBijective (coeLinearMap U) h

DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top packages both conditions above as an iff characterization of IsInternal.

Span as the smallest containing submodule

example {s : Set V} (E : Submodule K V) : Submodule.span K s ≤ E ↔ s ⊆ E :=
  Submodule.span_le

example : GaloisInsertion (Submodule.span K) ((↑) : Submodule K V → Set V) :=
  Submodule.gi K V

Submodule.span_le says span K s is the smallest submodule containing s. Submodule.gi packages span and the coercion Submodule K V → Set V as a Galois insertion.

Decomposing an element of S ⊔ T

Every element of S ⊔ T splits as a sum of an element of S and an element of T:

$$x\in S\bigsqcup T⟹\mathrm{\exists }s\in S,t\in T,x=s+t$$

The key idea: rewrite the problem of S ⊔ T as the problem of Submodule.span K (↑S ∪ ↑T) (via Submodule.span_eq and Submodule.span_union), then induct with Submodule.span_induction.

Proof walkthrough (click to expand)

example {S T : Submodule K V} {x : V} (h : x ∈ S ⊔ T) :
    ∃ s ∈ S, ∃ t ∈ T, x = s + t := by
  rw [← S.span_eq, ← T.span_eq, ← Submodule.span_union] at h
  induction h using Submodule.span_induction with
  | mem y h =>
      rcases h with (y_in_S | y_in_T)
      · use y, y_in_S, 0, T.zero_mem; simp
      · use 0, S.zero_mem, y, y_in_T; simp
  | zero =>
      use 0, S.zero_mem, 0, T.zero_mem; simp
  | add x y hx hy hx' hy' =>
      rcases hx' with ⟨sx, sx_in_S, tx, tx_in_T, rfl⟩
      rcases hy' with ⟨sy, sy_in_S, ty, ty_in_T, rfl⟩
      use sx + sy, S.add_mem sx_in_S sy_in_S, tx + ty, T.add_mem tx_in_T ty_in_T
      module
  | smul a x hx hx' =>
      rcases hx' with ⟨sx, sx_in_S, tx, tx_in_T, rfl⟩
      use a • sx, S.smul_mem a sx_in_S, a • tx, T.smul_mem a tx_in_T
      simp

1. Rewrite. ← S.span_eq and ← T.span_eq turn S, T into spans of their carrier sets, and ← Submodule.span_union merges them: h : x ∈ Submodule.span K (↑S ∪ ↑T). Note span_eq explicitly uses the coercion (↑) : Submodule K V → Set V.
2. Induct over the span with Submodule.span_induction, which has four cases:
   • mem: y ∈ ↑S ∪ ↑T directly — pick (y, 0) or (0, y) depending on the side.
   • zero: pick (0, 0).
   • add: from decompositions of x and y, build the decomposition of x + y; the module tactic discharges the algebra.
   • smul: from a decomposition of x, build one for a • x.

Linear Maps Between Vector Spaces

Let φ : V →ₗ[K] W be a linear map between vector spaces V, W over K.

Image (map) and preimage (comap) of a submodule

variable (E : Submodule K V) in
#check (Submodule.map φ E : Submodule K W)

variable (F : Submodule K W) in
#check (Submodule.comap φ F : Submodule K V)

• Submodule.map φ E — the image of a subspace E ≤ V under φ.
• Submodule.comap φ F — the preimage of a subspace F ≤ W under φ.

Range and kernel, expressed via map/comap

Conceptually, range/kernel and image/preimage are the same idea, but in Lean they are defined differently:

example : LinearMap.range φ = .map φ ⊤ := LinearMap.range_eq_map φ
example : LinearMap.ker φ = .comap φ ⊥ := Submodule.comap_bot φ -- or `rfl`

• range = image of the top subspace ⊤ under φ.
• kernel = preimage of the bottom subspace ⊥ under φ.

Injectivity and surjectivity criteria

$$\phi \text{ injective}⟺\ker \phi =\mathrm{\perp },\phi \text{ surjective}⟺\mathrm{range}\phi =\mathrm{\top }$$

example : Injective φ ↔ ker φ = ⊥ := ker_eq_bot.symm
example : Surjective φ ↔ range φ = ⊤ := range_eq_top.symm

Membership lemmas

Lemma	Statement
Submodule.mem_map_of_mem	if x ∈ E ≤ V then φ x ∈ Submodule.map φ E
Submodule.mem_map	y ∈ Submodule.map φ E ↔ ∃ x ∈ E, φ x = y
Submodule.mem_comap	x ∈ Submodule.comap φ F ↔ φ x ∈ F

Galois connection: map φ E ≤ F ↔ E ≤ comap φ F

The image of E lands inside F exactly when E lands inside the preimage of F:

$$\phi (E)\le F⟺E\le {\phi }^{-1}(F)$$

Proof walkthrough (click to expand)

example (E : Submodule K V) (F : Submodule K W) :
    Submodule.map φ E ≤ F ↔ E ≤ Submodule.comap φ F := by
  constructor
  · rintro h x x_in_E
    specialize h ⟨x, x_in_E, rfl⟩
    exact h
  · rintro h _ ⟨x, x_in_E, rfl⟩
    rcases h x_in_E with h1
    exact h1

• (→) any x ∈ E gives φ x ∈ Submodule.map φ E, so h forces φ x ∈ F, i.e. x ∈ comap φ F.
• (←) any y ∈ Submodule.map φ E is φ x for some x ∈ E, and h : E ≤ comap φ F gives φ x ∈ F.

Quotient Spaces

Let E : Submodule K V be a subspace of V.

The quotient is a vector space

example : Module K (V ⧸ E) := inferInstance

Canonical projection (mkQ)

Submodule.mkQ is the canonical linear projection onto the quotient, mkQ : V →ₗ[K] V ⧸ E:

Fact	Lemma	Statement
the projection itself	Submodule.mkQ	V →ₗ[K] V ⧸ E
its kernel	E.ker_mkQ	ker E.mkQ = E
its range	E.range_mkQ	range E.mkQ = ⊤

Universal properties: liftQ and mapQ

• Submodule.liftQ (lifting): if hφ : E ≤ ker φ, there's a unique V ⧸ E →ₗ[K] W factoring φ through mkQ, i.e. φ = liftQ φ hφ ∘ mkQ.

  example (hφ : E ≤ ker φ) : V ⧸ E →ₗ[K] W := E.liftQ φ hφ

• Submodule.mapQ (mapping quotients): if hφ : E ≤ .comap φ F, there's a unique V ⧸ E →ₗ[K] W ⧸ F making the square commute:

  V     →     W
  ↓mkQ  φ     ↓mkQ
  V ⧸ E →     W ⧸ F
       mapQ

  example (F : Submodule K W) (hφ : E ≤ .comap φ F) : V ⧸ E →ₗ[K] W ⧸ F := E.mapQ F φ hφ

• First isomorphism theorem: the quotient by the kernel is linearly isomorphic to the range:

  $$V/\ker \phi \cong \mathrm{range}\phi$$

  noncomputable example : (V ⧸ LinearMap.ker φ) ≃ₗ[K] range φ := φ.quotKerEquivRange

map_comap_eq and comap_map_eq

Lemma	Statement	Intuition
Submodule.map_comap_eq	Submodule.map φ (Submodule.comap φ F) = F ⊓ range φ	some elements of F may have no preimage under φ, so mapping the preimage back only recovers F ⊓ range φ, not all of F
Submodule.comap_map_eq	Submodule.comap φ (Submodule.map φ E) = E ⊔ ker φ	everything in ker φ maps into φ E (since 0 ∈ φ E), so the preimage of the image picks up all of ker φ in addition to E

Open exercise: submodules of the quotient

NOTE

The correspondence theorem — submodules of V ⧸ E correspond to submodules of V containing E — is stated but left unproved (sorry) in the source:

example : Submodule K (V ⧸ E) ≃ { F : Submodule K V // E ≤ F } where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

---

Part III — Endomorphisms (S03)

Summary generated from the comments in C10-S03.lean.

Throughout, V is a vector space over a field K:

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]
open Polynomial Module LinearMap End

Endomorphisms

An endomorphism is a linear map from a vector space to itself. In Mathlib this has its own notation:

End K V   -- abbreviation for `V →ₗ[K] V`

Unlike general linear maps, endomorphisms can be multiplied, which makes End K V a (non-commutative) ring — and even a K-algebra.

Multiplication is composition

Multiplication of endomorphisms is composition of linear maps, i.e. * ↔ ∘ₗ:

example (φ ψ : End K V) : φ * ψ = φ ∘ₗ ψ :=
  End.mul_eq_comp φ ψ -- `rfl` would also work

NOTE

The multiplication φ * ψ applies ψ first: (φ * ψ) x = φ (ψ x), as witnessed by End.mul_apply.

Polynomial Evaluation on Endomorphisms (aeval)

Evaluating a polynomial P : K[X] at an endomorphism φ yields another endomorphism. This is a special kind of evaluation, called algebra evaluation (aeval):

example (P : K[X]) (φ : End K V) : V →ₗ[K] V :=
  aeval φ P

Evaluating the simplest polynomial X gives the endomorphism back:

example (φ : End K V) : aeval φ (X : K[X]) = φ :=
  aeval_X φ

aeval is an algebra homomorphism

aeval φ : K[X] →ₐ[K] End K V is an AlgHom — it maps polynomials to endomorphisms and preserves the whole algebra structure. This is what justifies rewriting with:

Rewrite	Meaning
map_add	aeval φ (P + Q) = aeval φ P + aeval φ Q
map_mul	aeval φ (P * Q) = aeval φ P * aeval φ Q
map_one	aeval φ 1 = 1 (the identity endomorphism)

IMPORTANT

Even though both K[X] and End K V are vector spaces, aeval φ is not treated as a bare linear map in Lean — it is an algebra homomorphism, so multiplicative lemmas like map_mul apply directly.

Toolbox: Subspace Lemmas

The two theorems below rely on the following characterizations:

Lemma	Statement
Submodule.eq_bot_iff	S = ⊥ ↔ ∀ x ∈ S, x = 0 — a subspace is trivial iff it only contains 0
Submodule.mem_inf	x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T — intersection membership
LinearMap.mem_ker	x ∈ ker φ ↔ φ x = 0 — kernel membership
Submodule.add_mem_sup	x ∈ S → y ∈ T → x + y ∈ S ⊔ T — sums land in the supremum
LinearMap.ker_le_ker_comp	ker f ≤ ker (g ∘ f) — kernels grow under pre-composition
End.mul_apply	(φ * ψ) x = φ (ψ x) — multiplication is composition, pointwise
map_mul	aeval φ (P * Q) = aeval φ P * aeval φ Q — aeval preserves *

Theorem 1: Coprime evaluations have trivially intersecting kernels

Statement. If P and Q are coprime polynomials, then the kernels of their evaluations on an endomorphism φ intersect trivially:

$$gcd(P,Q)=1⟹\ker P(\phi )\cap \ker Q(\phi )=\{0\}$$

example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) :
    ker (aeval φ P) ⊓ ker (aeval φ Q) = ⊥ := by
  rw [Submodule.eq_bot_iff]
  rintro x h1
  rw [Submodule.mem_inf, LinearMap.mem_ker, LinearMap.mem_ker] at h1
  rcases h1 with ⟨h2, h3⟩
  rcases h with ⟨a, b, bezout_identy⟩
  have := congr((aeval φ) $bezout_identy.symm x)
  rwa [map_add, map_mul, map_mul, map_one, LinearMap.add_apply, End.mul_apply, End.mul_apply,
       h2, h3, LinearMap.map_zero, LinearMap.map_zero, add_zero, End.one_apply] at this

Proof walkthrough

1. Unfold the goal. Submodule.eq_bot_iff turns S = ⊥ into ∀ x ∈ S, x = 0. After rintro x h1 and unfolding ⊓/ker membership, h1 becomes the pair
   • h2 : aeval φ P x = 0, and
   • h3 : aeval φ Q x = 0.
2. Invoke Bézout. IsCoprime P Q destructs into polynomials a, b with the Bézout identity a * P + b * Q = 1.
3. Apply aeval φ to both sides, then evaluate at x (via congr((aeval φ) $ bezout_identy.symm x)). This is legitimate because aeval φ is an AlgHom.
4. Rewrite to x = 0. The long rwa [...] chain pushes aeval φ through the algebra operations:
   • map_add, map_mul, map_mul, map_one split the evaluation into (aeval φ a * aeval φ P + aeval φ b * aeval φ Q) x = (1 : End K V) x;
   • LinearMap.add_apply and End.mul_apply (twice) turn this into aeval φ a (aeval φ P x) + aeval φ b (aeval φ Q x) = x;
   • h2, h3 kill both terms; map_zero, add_zero, and End.one_apply finish with x = 0.

Theorem 2: Supremum of kernels is the kernel of the product

Statement. For coprime P and Q, the sum of the kernels of the evaluations equals the kernel of the evaluation of the product:

$$gcd(P,Q)=1⟹\ker P(\phi )+\ker Q(\phi )=\ker ((PQ)(\phi ))$$

example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) :
    ker (aeval φ P) ⊔ ker (aeval φ Q) = ker (aeval φ (P*Q)) := by
  apply le_antisymm
  · apply sup_le
    · rw [mul_comm, map_mul]
      apply LinearMap.ker_le_ker_comp
    · rw [map_mul]
      apply LinearMap.ker_le_ker_comp
  · rintro x h1
    rcases h with ⟨U, W, h2⟩
    have key : x = aeval φ (U*P) x + aeval φ (W*Q) x := by simpa using congr((aeval φ) $h2.symm x)
    rw [key, add_comm]
    apply Submodule.add_mem_sup <;> rw [mem_ker] at *
    · rw [← End.mul_apply, ← map_mul, show P*(W*Q) = W*(P*Q) by ring, map_mul, End.mul_apply, h1,
          map_zero]
    · rw [← End.mul_apply, ← map_mul, show Q*(U*P) = U*(P*Q) by ring, map_mul, mul_apply, h1,
          map_zero]

Proof walkthrough

The equality is proved by mutual inclusion via le_antisymm (a = b ↔ a ≤ b ∧ b ≤ a).

Direction ≤: each kernel sits inside the kernel of the product.

• sup_le reduces S ⊔ T ≤ C to the two goals S ≤ C and T ≤ C.
• For ker (aeval φ P) ≤ ker (aeval φ (P*Q)): rewrite P*Q = Q*P (mul_comm) and split the evaluation (map_mul), so the goal becomes ker (aeval φ P) ≤ ker (aeval φ Q * aeval φ P) — which is exactly LinearMap.ker_le_ker_comp, since the right-hand kernel contains everything killed by the first applied factor.
• The Q case is symmetric, without needing mul_comm.

Direction ≥: anything killed by the product splits across the two kernels.

1. Take x with h1 : aeval φ (P*Q) x = 0 and destruct the Bézout identity as U*P + W*Q = 1.
2. Key decomposition (key): applying aeval φ to Bézout and evaluating at x gives x = aeval φ (U*P) x + aeval φ (W*Q) x (proved by simpa off the same congr trick as Theorem 1).
3. After rw [key, add_comm], Submodule.add_mem_sup reduces the goal to showing each summand lies in the appropriate kernel; rw [mem_ker] at * unfolds all kernel memberships.
4. For the first summand, aeval φ P (aeval φ (W*Q) x) = 0:
   • ← End.mul_apply merges the two applications into one multiplication (aeval φ P * aeval φ (W*Q)) x;
   • ← map_mul folds it into a single evaluation aeval φ (P * (W * Q)) x;
   • show P*(W*Q) = W*(P*Q) by ring re-associates inside the polynomial ring (which is commutative);
   • map_mul, End.mul_apply split again to expose the factor aeval φ (P*Q) x, which h1 rewrites to 0, and map_zero closes the goal.
5. The second summand is identical with the roles of P/Q and U/W swapped.

TIP

The recurring pattern in both proofs: End.mul_apply (pointwise multiplication ⇔ composition) and map_mul (aeval ⇔ polynomial multiplication) let you move freely between evaluating a product and composing evaluations — with ring handling commutativity at the polynomial level.

---

Part IV — Bases (S04)

Summary generated from the comments in C10-S04.lean.

Throughout, V is a vector space over a field K:

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]
open Module

Bases and Coordinates

Fix a basis B : Basis ι K V indexed by a type ι, a vector v : V, and an index i : ι:

variable {ι : Type*} (B : Basis ι K V) (v : V) (i : ι)

Expression	Type	Meaning
B i	V	the basis vector with index i
B.repr	V ≃ₗ[K] ι →₀ K	the linear isomorphism between V and finitely supported functions ι →₀ K
B.repr v	ι →₀ K	the coordinate of v with respect to B
B.repr v i	K	the i-th entry of the coordinate of v

NOTE

ι →₀ K (Finsupp) is the type of functions ι → K that are nonzero on only finitely many inputs. Every vector in V has a unique coordinate representation of this form via the basis B.

Constructing a basis

Given a linearly independent family of vectors b that spans V, we can assemble it into a basis:

noncomputable example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) : Basis ι K V :=
  Basis.mk b_indep (fun v _ ↦ b_spans v)

A basis is exactly the conjunction of two conditions:

1. the family b is linearly independent, and
2. the family b spans the whole vector space.

The constructed basis retrieves the original family pointwise:

example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) (i : ι) :
    Basis.mk b_indep (fun v _ ↦ b_spans v) i = b i :=
  Basis.mk_apply b_indep (fun v _ ↦ b_spans v) i

Canonical bases

variable [DecidableEq ι]
-- The basis of `ι →₀ K` given by the single vectors
example : Finsupp.basisSingleOne.repr = LinearEquiv.refl K (ι →₀ K) := rfl
example (i : ι) : Finsupp.basisSingleOne i = Finsupp.single i 1 := rfl
-- Coordinates of a function `ι → K` with respect to the Pi basis
example [Finite ι] (x : ι → K) (i : ι) : (Pi.basisFun K ι).repr x i = x i := by simp

• Finsupp.basisSingleOne — the basis of ι →₀ K whose i-th vector is Finsupp.single i 1; its repr is definitionally the identity. DecidableEq ι is needed to decide equality of indices.
• Pi.basisFun K ι — the basis of ι → K (for finite ι) that recovers each function entry as its own coordinate.

Reconstructing a vector from its coordinates

The vector v is the linear combination of the basis vectors B i with coefficients B.repr v i:

example [Fintype ι] : ∑ i : ι, B.repr v i • (B i) = v :=
  B.sum_repr v

Linear Combinations

Linear combination with general vectors

For a coefficient function c : ι →₀ K and any family of vectors f : ι → V, the linear combination over the support of c can be computed as a sum over any finset s containing that support — the extra terms contribute zero coefficients:

example (c : ι →₀ K) (f : ι → V) (s : Finset ι) (h : c.support ⊆ s) :
    Finsupp.linearCombination K f c = ∑ i ∈ s, c i • f i :=
  Finsupp.linearCombination_apply_of_mem_supported K h

Taking linear combinations is itself linear in the coefficients:

variable (f : ι → V) in
#check (Finsupp.linearCombination K f : (ι →₀ K) →ₗ[K] V)

Linear combination with a basis

Combining the basis vectors with their coordinates gives back the vector:

example : Finsupp.linearCombination K B (B.repr v) = v :=
  B.linearCombination_repr v

Linear Maps Constructed from a Basis

Let W be another vector space over K, φ : V →ₗ[K] W, and u : ι → W a family of vectors in W.

Extension by linearity (B.constr)

A linear map out of V is completely determined by its values on a basis. This is packaged as a linear equivalence:

#check (B.constr K : (ι → W) ≃ₗ[K] (V →ₗ[K] W))
#check (B.constr K u : V →ₗ[K] W)

In other words, given a basis B of V:

• (a) once we specify the images u of the basis vectors, the linear map is completely determined;
• (b) conversely, once the linear map is specified on the basis vectors, the images u are determined.

The constructed map does what it should on basis vectors:

example (i : ι) : B.constr K u (B i) = u i :=
  B.constr_basis K u i

Maps agreeing on a basis are equal (B.ext)

Two linear maps that agree on all basis vectors are equal:

example (φ ψ : V →ₗ[K] W) (h : ∀ i, φ (B i) = ψ (B i)) : φ = ψ :=
  B.ext h

Matrices Representing Linear Maps

The matrix representing a linear map is determined by three things:

1. the choice of basis B for the source V — once B is fixed, V is coordinatized;
2. the choice of basis B' for the target W;
3. the action of the linear map on the basis vectors of V.

IMPORTANT

The basis vectors B i need not be mapped to basis vectors of W — they can land anywhere in W, and different actions give different matrices. Moreover, even when B is mapped onto B', the map on indices need not be bijective, since the index types ι and ι' may have different sizes.

The matrix of a linear map (toMatrix)

With bases B of V (indexed by ι) and B' of W (indexed by ι'), both finite with decidable equality:

variable {ι' : Type*} (B' : Basis ι' K W)
         [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι']
open LinearMap Matrix  -- `*ᵥ` is matrix–vector multiplication

#check (toMatrix B B' : (V →ₗ[K] W) ≃ₗ[K] Matrix ι' ι K)

This is a two-way correspondence:

• (a) given the linear map, the matrix Matrix ι' ι K with respect to these bases is determined;
• (b) given the matrix, the linear map is determined.

The matrix acts on coordinate vectors as expected — the coordinate of v multiplied by the matrix of φ gives the coordinate of φ v:

$$M_{B^{\prime }}^B(\phi )\cdot [v{]}_B=[\phi (v){]}_{B^{\prime }}$$

example (φ : V →ₗ[K] W) (v : V) : (toMatrix B B' φ) *ᵥ (B.repr v) = B'.repr (φ v) :=
  toMatrix_mulVec_repr B B' φ v

Change of basis

Let B'' be another basis of W (indexed by ι''). The matrix of φ with respect to B, B'' is obtained by multiplying the matrix of the identity map from B' to B'' with the matrix of φ from B to B':

$$M_{B^{″}}^B(\phi )=M_{B^{″}}^{B^{\prime }}(\mathrm{id})\cdot M_{B^{\prime }}^B(\phi )$$

example (φ : V →ₗ[K] W) : (toMatrix B B'' φ) = (toMatrix B' B'' .id) * (toMatrix B B' φ) := by
  simp

Composition corresponds to matrix multiplication

Lemma	Statement
toMatrix_comp	toMatrix v₁ v₃ (f.comp g) = toMatrix v₂ v₃ f * toMatrix v₁ v₂ g
id_comp	LinearMap.id ∘ₗ f = f
comp_id	f ∘ₗ LinearMap.id = f
toMatrix_id	the identity map is represented by the identity matrix
Matrix.det_mul	det (A * B) = det A * det B
Matrix.det_one	det 1 = 1

The determinant of an endomorphism is basis-independent

If B and B' are both bases of the same space V and φ : End K V, then the determinant of the representing matrix does not depend on the chosen basis:

$$det{M}_B^B(\phi )=det{M}_{B^{\prime }}^{B^{\prime }}(\phi )$$

Two aspects are at play:

1. the matrix of an endomorphism is unchanged when the target basis varies together with the source basis;
2. once source and target bases are fixed, the matrix is uniquely determined by the map itself.

That is, toMatrix B B φ is determined by φ, not by the particular choice between B and B'.

Proof walkthrough (click to expand)

example [Fintype ι] (B' : Basis ι K V) (φ : End K V) :
    (toMatrix B B φ).det = (toMatrix B' B' φ).det := by
  set M := toMatrix B B φ
  set M' := toMatrix B' B' φ
  set P := (toMatrix B B') LinearMap.id
  set P' := (toMatrix B' B) LinearMap.id
  have F : M = P' * M' * P := by
    rw [← toMatrix_comp, ← toMatrix_comp, id_comp, comp_id]
  have F' : P' * P = 1 := by
    rw [← toMatrix_comp, id_comp, toMatrix_id]
  rw [F, Matrix.det_mul, Matrix.det_mul,
      show P'.det * M'.det * P.det = P'.det * P.det * M'.det by ring, ← Matrix.det_mul, F',
      Matrix.det_one, one_mul]

1. Name the players. M, M' are the matrices of φ in the two bases; P and P' are the change-of-basis matrices (the identity map read in the two pairs of bases).
2. Similarity (F). M = P' * M' * P: fold matrix products back into compositions with ← toMatrix_comp (twice), then simplify id ∘ₗ φ ∘ₗ id to φ via id_comp/comp_id.
3. Inverse change of basis (F'). P' * P = 1, since the two identity readings compose to the identity map, whose matrix is 1 (toMatrix_id).
4. Determinant computation. Expand det M via Matrix.det_mul twice, commute the scalar determinants with ring, refold P'.det * P.det into det (P' * P) = det 1 = 1 (← Matrix.det_mul, F', Matrix.det_one), and finish with one_mul.

Finite Rank of Vector Spaces

The finite rank (dimension) of V over K is a natural number:

#check (Module.finrank K V : ℕ)

The archetypical n-dimensional space

Fin n → K is the canonical space of dimension n over K:

example (n : ℕ) : Module.finrank K (Fin n → K) = n :=
  Module.finrank_fin_fun K

The scalar field matters

Different scalar fields give different dimensions, even when the underlying additive group is the same. When computing a dimension, always keep the scalar field in mind:

• ℂ as a vector space over itself has dimension one: Module.finrank ℂ ℂ = 1 (Module.finrank_self).
• ℂ as a vector space over ℝ has dimension two: Module.finrank ℝ ℂ = 2 (Complex.finrank_real_complex).

Positivity of rank

For a finite-dimensional space, the rank is positive iff the space is nontrivial:

example [FiniteDimensional K V] : 0 < Module.finrank K V ↔ Nontrivial V :=
  Module.finrank_pos_iff

The forward direction alone is often useful on its own:

example [FiniteDimensional K V] (h : 0 < Module.finrank K V) : Nontrivial V := by
  apply (Module.finrank_pos_iff (R := K)).1
  exact h

Finite basis ⇔ finite-dimensional

A basis B : Basis ι K V relates finiteness of the index type ι to finite-dimensionality of V:

variable {ι : Type*} (B : Module.Basis ι K V)
example [Finite ι] : FiniteDimensional K V := Module.Basis.finiteDimensional_of_finite B
example [FiniteDimensional K V] : Finite ι := (FiniteDimensional.fintypeBasisIndex B).finite

Finite Rank of Submodules

Let E F : Submodule K V with V finite-dimensional.

Dimension formula. The rank of the supremum plus the rank of the infimum equals the sum of the ranks:

$$\dim (E+F)+\dim (E\cap F)=\dim E+\dim F$$

example : finrank K (E ⊔ F : Submodule K V) + finrank K (E ⊓ F : Submodule K V) =
    finrank K E + finrank K F :=
  Submodule.finrank_sup_add_finrank_inf_eq E F

Monotonicity. The rank of a submodule is at most the rank of the whole space:

example : finrank K E ≤ finrank K V := Submodule.finrank_le E

Pigeonhole for subspaces. If the ranks of E and F add up to more than the rank of V, their intersection is nontrivial:

example (h : finrank K V < finrank K E + finrank K F) :
    Nontrivial (E ⊓ F : Submodule K V) := by
  rw [← Module.finrank_pos_iff (R := K)]
  rw [← Submodule.finrank_sup_add_finrank_inf_eq E F] at h
  have : finrank K (E ⊔ F : Submodule K V) ≤ finrank K V := Submodule.finrank_le (E ⊔ F : Submodule K V)
  linarith

The proof rewrites the goal into positivity of finrank K (E ⊓ F) (← Module.finrank_pos_iff), rewrites the hypothesis with the dimension formula, notes that finrank K (E ⊔ F) ≤ finrank K V by monotonicity, and lets linarith close the arithmetic.