Table of Contents

• C10 S02 — Linear Algebra: Summary Notes
  • 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

C10 S02 — Linear Algebra: Summary Notes

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