LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Untwisted Hall structure constants and products are finite

Statement

For a finitary abelian category, each untwisted Hall coefficient $g_{M, N}^{L}$ is finite and depends only on the isomorphism classes of $M, N, L$ . For fixed $M, N$ , only finitely many isomorphism classes $[L]$ have $g_{M, N}^{L} \neq 0$ . Hence the basis formula in The untwisted Hall algebra of a finitary abelian category is a finite sum in its direct-sum module.

Facts & Assumptions

Given: A finitary abelian category $A$ , objects $M, N, L$ , and the coefficient $g_{M, N}^{L}$ from the untwisted Hall product.

[F1]

For every pair $X, Y$ , the sets $Hom (X, Y)$ and ${YExt}^{1} (X, Y)$ are finite; the latter consists of Yoneda classes of short exact sequences with the displayed endpoints (Small finitary abelian categories for Hall multiplication).

[F2]

$g_{M, N}^{L}$ counts equivalence classes of monomorphisms $N \to L$ under precomposition by isomorphisms of $N$ , retaining those whose cokernel is isomorphic to $M$ (The untwisted Hall algebra of a finitary abelian category).

[F3]

A morphism between short exact sequences that is the identity on both endpoints is an isomorphism on the middle object, by the short five lemma (Short five lemma in an abelian category).

Proof

technique · direct

1.1F2algebra

An isomorphism of middle objects transports subobjects and induces an isomorphism of their cokernel quotients; replacing either endpoint by an isomorphic object preserves the two type conditions. Thus the count in [F2] depends only on $[M], [N], [L]$ .

1.2F1F2

For fixed $L$ , the equivalence classes counted by [F2] are a quotient of the finite set $Hom (N, L)$ from [F1]. The subset whose cokernel is isomorphic to $M$ is therefore finite.

1.3F1F2F3choose

Every elementary map in the generating relation for [F1] preserves the middle-object isomorphism class by [F3], and so does its reflexive, symmetric and transitive closure. Thus taking the middle-object class defines a map from the finite set ${YExt}^{1} (M, N)$ . If $g_{M, N}^{L} \neq 0$ , a counted subobject and quotient give a short exact sequence $0 \to N \to L \to M \to 0$ after transporting its endpoints by isomorphisms, so $[L]$ lies in the image. That image is finite, proving finite support without simultaneous choices of extension representatives.

2.1F2step 1.2step 1.3algebra∎

Each coefficient is a natural number and the support is finite by steps 1.2–1.3. Mapping an integer $n$ to $n 1_{R}$ therefore gives a well-defined element of the direct sum in [F2], with no automorphism denominator or additional finiteness condition.

Depends on

Used by

Cited to discharge well-definedness by The untwisted Hall algebra of a finitary abelian category.

Dependency tree · two levels

22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Olivier Schiffmann, Lectures on Hall Algebras, arXiv:math/0611617v2, §§1.1 and 1.3 (standard reference, not scraped)
Matthew B. Young, Degenerate versions of Green’s theorem for Hall modules, arXiv:1810.08238v2, §2.1 (standard reference, not scraped)