PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-14

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.

Serre transgression agrees with the relative connecting construction

Statement

Let $p : E \to B$ and $R$ satisfy the homological Serre theorem, write $E_{a} = p^{- 1} (B^{a})$ , and fix $n \geq 2$ . Let $D_{n} = E_{n, 0}^{n} ↪ E_{n, 0}^{2}$ be the domain of the homological transgression. If $ξ \in D_{n}$ , choose an $E^{n}$ representative $x \in A_{n, n}^{n} = C_{n} (E_{n}; R) \cap \partial^{- 1} C_{n - 1} (E_{0}; R) .$ Then $x$ is a relative cycle for $(E_{n}, E_{0})$ , and if $δ : H_{n} (E_{n}, E_{0}; R) ⟶ H_{n - 1} (E_{0}; R)$ is the positive connecting map and $q_{n} : H_{n - 1} (E_{0}; R) = E_{0, n - 1}^{1} ⟶ E_{0, n - 1}^{n}$ is the composite of the vertical-axis page quotients, then $τ_{n} (ξ) = d_{n} (ξ) = q_{n} δ [x] = q_{n} [\partial x] .$ The result is independent of the representative $x$ and of its relative class. Thus a transgressive base-axis class is lifted through the relevant filtered relative group and its boundary gives the fiber-axis transgression, with no sign beyond the fixed homological differential convention. This is the homological orientation; the dual cohomological transgression starts with a fiber-axis class.

When the CW structure has one zero-cell $b$ , $E_{0} = F_{b}$ , so this is the familiar relative connecting construction for $(E_{n}, F_{b})$ . All assertions are choice-free.

Facts & Assumptions

Given: A transgressive class on the homological base axis and one local representative on its n-page.

[F1]

Serre edge homomorphisms and transgression defines the homological transgression as $d_{n} : E_{n, 0}^{n} \to E_{0, n - 1}^{n}$ and fixes its sign and restricted domain.

[F2]

Serre filtration over the base skeleta identifies $F_{a} C_{*} (E; R)$ with $C_{*} (E_{a}; R)$ . R cycles and r boundaries of an increasingly filtered complex and R page of the spectral sequence of a filtered complex give the representative formulas for $A^{n}$ , $B^{n}$ , and $E^{n}$ , while The filtered differential induces d r on the r page states that the page differential sends a local representative $[x]$ to $[\partial x]$ .

[F3]

Long exact sequence of a pair supplies the pair connector, and Relative connecting homomorphism on cycles fixes its positive formula $δ [x] = [\partial x]$ .

[F4]

Spectral sequence subquotient and local lifting calculus supplies natural quotient descent and the nested-quotient identifications used by the vertical-axis maps.

Proof

technique · compare the two boundary formulas on one filtered representative

1.1

Since $x \in A_{n, n}^{n}$ , [F2] gives $x \in C_{n} (E_{n}; R)$ and $\partial x \in C_{n - 1} (E_{0}; R)$ . Thus $x$ determines $[x] \in H_{n} (E_{n}, E_{0}; R)$ , and [F3] gives $δ [x] = [\partial x]$ with positive sign.

F2F3

2.1

On the vertical axis no differential leaves $(0, n - 1)$ . Its transitions from $E^{1}$ through $E^{n}$ are therefore quotient maps by successive incoming images, and [F4] gives their canonical composite $q_{n}$ . The page-differential theorem in [F2] sends the representative $[x]$ to the class of the same chain boundary $\partial x$ and then takes precisely this target quotient. Therefore $d_{n} (ξ) = q_{n} [\partial x] = q_{n} δ [x]$ , with the sign fixed simultaneously by [F1] and [F3].

F1F2F3F4Step 1.1

3.1

Suppose $x^{'}$ is another $E^{n}$ representative of $ξ$ . Since these are quotient modules, [F2] gives $x^{'} - x = a + \partial y$ with $a \in A_{n - 1, n}^{n - 1}$ and $y \in A_{2 n - 1, n + 1}^{n - 1}$ . Hence $\partial x^{'} - \partial x = \partial a$ . In the target position $(0, n - 1)$ , this lies in the second denominator summand $\partial A_{n - 1, n}^{n - 1} \subseteq B_{0, n - 1}^{n},$ so quotient descent in [F4] gives $q_{n} [\partial x^{'}] = q_{n} [\partial x]$ . If the relative cycle representative is changed by a chain in $E_{0}$ or an ordinary boundary, its pair connector changes by a boundary in $E_{0}$ or by zero. Thus both the page and relative ambiguities disappear in the displayed target quotient.

F2F3F4Step 2.1

4.1

For $n = 2$ , $q_{2}$ is the single passage from $E^{1}$ to $E^{2}$ , and there are no earlier transgression-domain conditions. If $E_{0}$ , the source, the target, or $R$ is zero, every displayed class is zero. A zero base-axis class in $D_{n}$ , one relative representative, a constant or degenerate simplex, and a relative boundary obey the same formula. Both source and target endpoints, both representative ambiguities, and the positive sign are checked in Steps 1.1–3.1. Classes killed by an earlier differential are outside $D_{n}$ , so the formula makes no claim about them. The proof uses one supplied representative and canonical quotient maps, so no AC is used. The proposition has no iff assertion.

F1F2F3F4Step 1.1Step 2.1Step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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

Hatcher, Algebraic Topology, Proposition 5.14 (standard reference, not scraped)