Basis-flip criterion for vanishing coinvariants

Proved

LegacyAlgebra.basisFlipCoinvariants

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

coinvariantslinearalgebrarepresentationtheory

Let ρ be a linear representation of a group G on a vector space V over a field k in which 2 is nonzero. Suppose V has a basis b such that, for every basis vector b_i, some element of G sends b_i to −b_i. Then the span of all differences ρ(g)v − v is V, so the coinvariant space is zero. The basis and group may be infinite.

Preamble

import Mathlib

set_option autoImplicit false

Formal statement

theorem LegacyAlgebra.basisFlipCoinvariants
    (k G V ι : Type*) [Field k] [Group G]
    [AddCommGroup V] [Module k V]
    (ρ : Representation k G V) (b : Module.Basis ι k V)
    (hTwo : (2 : k) ≠ 0)
    (hFlip : ∀ i : ι, ∃ g : G, ρ g (b i) = -(b i)) :
    Representation.Coinvariants.ker ρ = ⊤ := by
  sorry

Source

Unpublished research note class2_pure_braid_filter_assessment.md, section “Odd-primary no-go for the stationary-source family”; SHA-256 3138168576f237898231c34e54fc76869bbb5f4c2b820c00f73b62ebe2f9d907.

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$ , every additive commutative group $V$ equipped with a $k$ -module structure, every type $\iota$ , every representation $\rho:G\to\operatorname{End}_k(V)$ , and every $k$ -basis $(b_i)_{i\in\iota}$ of $V$ , assume that $2\ne0$ in $k$ and that for each $i\in\iota$ there exists a group element $g\in G$ such that $\rho(g)(b_i)=-b_i$ . Then the $k$ -linear span of all vectors $\rho(g)(v)-v$ , for $g\in G$ and $v\in V$ , equals the whole space $V$ . The group element that negates a basis vector may depend on its index. No finiteness is required of $G$ , $\iota$ , or the dimension of $V$ ; an empty basis is allowed, in which case the basis condition forces $V$ to be the zero space and the negation hypothesis is vacuous.

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