Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13
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.

Covariant and contravariant Hom⁡ are left exact

Statement

Let X be a left R-module.

  1. If 0→A→uB→vC is exact, then 0→Hom⁡R(X,A)→u∗Hom⁡R(X,B)→v∗Hom⁡R(X,C) is exact.
  2. If A→uB→pC→0 is exact, then 0→Hom⁡R(C,X)→p∗Hom⁡R(B,X)→u∗Hom⁡R(A,X) is exact.

Thus covariant and contravariant Hom⁡ are left exact.

Facts & Assumptions

Given: The two exact sequences in the statement and a left R-module X.

[F1]

Postcomposition and precomposition define the displayed homomorphisms on Hom groups (The abelian group Hom⁡R(M,N) and maps induced by pre- and postcomposition).

[F2]

Exactness means equality of the incoming image and outgoing kernel; the zero endpoints make u injective in the first sequence and p surjective in the second (Exact sequences and short exact sequences of modules).

[L1]

If a homomorphism h:M→P vanishes on a submodule N, it factors uniquely through M/N (A module homomorphism vanishing on N factors uniquely through M/N).

Proof

technique · direct
1.1

If u∗f=0, then u(f(x))=0 for every x, and injectivity of u gives f=0; hence u∗ is injective.

F1F2
1.2

Composability gives v∗u∗=0, so im⁡u∗≤ker⁡v∗.

F1F2
1.3

If g:X→B satisfies v∗g=0, then g(x)∈ker⁡v=im⁡u for every x. Injectivity of u gives a unique f(x)∈A with u(f(x))=g(x); uniqueness makes f linear, so g=u∗f.

F1F2
1.4

If p∗h=0, surjectivity of p gives h=0, so p∗ is injective; and u∗p∗=0 because p∘u=0.

F1F2
1.5

If g:B→X satisfies u∗g=g∘u=0, then g vanishes on im⁡u=ker⁡p. By [L1] it factors uniquely through B/ker⁡p, and since p is surjective the rule gˉ(p(b))=g(b) gives the corresponding homomorphism gˉ:C→X with g=gˉ∘p=p∗(gˉ).

F1F2L1
2.1

Steps 1.1 to 1.3 prove the covariant sequence exact, and steps 1.4 and 1.5 prove the contravariant sequence exact.

step 1.1step 1.2step 1.3step 1.4step 1.5∎

Depends on

Used by

Dependency tree · two levels

8 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