Orbit augmentation subspace

Definition

legacyOrbitAugmentation

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

coinvariantsgroupactionslinearalgebra

Let a group G act on a set X and let k be a field. The orbit augmentation subspace of the finitely supported functions X → k is the k-linear span of all differences e_(g·x) − e_x, for g in G and x in X.

Definition code

import Mathlib

set_option autoImplicit false

/-- The subspace generated by differences of basis vectors in a group orbit.
The orbit set is not required to be finite in this definition. -/
noncomputable def legacyOrbitAugmentation
    (k G X : Type*) [Field k] [Group G] [MulAction G X] :
    Submodule k (X →₀ k) :=
  Submodule.span k
    (Set.range fun gx : G × X =>
      Finsupp.single (gx.1 • gx.2) (1 : k) - Finsupp.single gx.2 1)

Source

Unpublished research note metabelian_pure_fiber_no_go.md, §3 (Orbit-rank theorem); SHA-256 3ba5b183826a2e93741d33827b5a1d701c3df2f6d31beeb3857cc2141849e3c8.

Read-back

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

For every field $k$ , every group $G$ , and every type $X$ equipped with a left action of $G$ , this defines a $k$ -linear subspace of the vector space $k^{(X)}$ of finitely supported functions $X\to k$ : it is the span of all vectors $\delta_{g\cdot x}-\delta_x$ with $g\in G$ and $x\in X$ , where $\delta_x$ takes the value $1$ at $x$ and $0$ elsewhere. Equivalently, its elements are finite $k$ -linear combinations of those differences. Neither $G$ nor $X$ is required to be finite, and no restriction is imposed on the characteristic of $k$ ; an empty $X$ is allowed and gives the zero subspace, as does a trivial action.

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