Cycles modulo boundaries for a finite linear complex

Definition

Smooth4AlgebraHomology

by ryanshin · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

homologicalalgebralinearalgebra

Let $d:V\to V$ be a linear map over a field. Its cycle space is $\ker d$ . The subspace called boundaries in cycles is $\ker d\cap\operatorname{im}d$ , represented inside $\ker d$ ; the homology space is its quotient. When $d^2=0$ , all boundaries are cycles, so this is precisely the usual homology $\ker d/\operatorname{im}d$ .

Every theorem using this construction as square-zero homology explicitly assumes $d^2=0$ . The definition itself works for an arbitrary linear map.

Definition code

import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
import Mathlib.LinearAlgebra.Dimension.Constructions

set_option autoImplicit false

namespace Smooth4Algebra

/-- Boundaries viewed inside the cycle space.  When `d ∘ d = 0`, these
are exactly the boundaries of the square-zero complex. -/
def boundariesInCycles {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
    (d : V →ₗ[K] V) : Submodule K (LinearMap.ker d) :=
  (LinearMap.range d).comap (LinearMap.ker d).subtype

/-- Actual vector-space homology, represented as cycles modulo boundaries.
Every theorem using it as homology explicitly assumes square-zero. -/
abbrev Homology {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
    (d : V →ₗ[K] V) :=
  (LinearMap.ker d) ⧸ boundariesInCycles d

end Smooth4Algebra

Source

Newly authored from cycle21_corner_budget_independent.md, §1 (joint kernel/projection argument), SHA-256 89aa667aee6440fe989e7664eec02f5a7a60010d1d86a77dd094bdf95ba8bdba

Read-back

What the Lean code literally says, in plain math · Codex independent blind auditor; exact model identifier unavailable

For every field $K$ , every additive commutative group $V$ equipped with a $K$ -module structure, and every $K$ -linear endomorphism $d:V\to V$ , this defines the subspace of $\ker d$ consisting of those vectors whose underlying element of $V$ lies in $\operatorname{im}d$ . Thus its elements are exactly the vectors $z\in V$ satisfying $d(z)=0$ and $z=d(v)$ for some $v\in V$ , regarded as elements of the vector space $\ker d$ ; under the inclusion $\ker d\hookrightarrow V$ , this subspace corresponds to $\ker d\cap\operatorname{im}d$ . No finite-dimensionality or equation $d^2=0$ is assumed, and the zero vector space and the zero endomorphism are included.

For every field $K$ , every additive commutative group $V$ equipped with a $K$ -module structure, and every $K$ -linear endomorphism $d:V\to V$ , this is an abbreviation for the quotient vector space of $\ker d$ by its subspace $\{z\in\ker d:\text{ there exists }v\in V\text{ with }d(v)=z\}$ . Equivalently, it is $\ker d/(\ker d\cap\operatorname{im}d)$ with the intersection viewed inside $\ker d$ ; its representatives are vectors killed by $d$ , and two such representatives determine the same quotient element precisely when their difference belongs to $\operatorname{im}d$ . The definition imposes neither finite-dimensionality nor $d^2=0$ , and includes the zero vector space and the zero endomorphism.

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by ryanshin · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph