Compact-support duality for finite-atlas manifolds without choice

If $U,V$ are open and duality holds on $U,V,U\cap V$ in every degree, the signed exact ladder [F3] and the five lemma make it hold on $U\cup V$. On an open subset $O$ of a supplied chart, enumerate all rational open boxes whose closures lie in its coordinate image. They cover that image by density of the rationals and openness. A box and each nonempty finite intersection of boxes is a coordinate ball, so [F2] applies. Induction proves duality on every finite union of these boxes: for the last box $B$ and preceding union $A$, $A\cap B$ is a union of fewer boxes, namely their intersections with $B$; the induction hypothesis and the finite gluing implication apply. Empty intersections and unions have zero groups.

Let $O_j$ be the union of admissible boxes among the first $j$ tuples in the fixed enumeration of finite rational tuples. Every compact subset of $O$ lies in some $O_j$, since a finite subcover by boxes has a maximum index. For a support class, [F4] moves its representative to that stage; equality of support classes is witnessed at one larger compact support and hence at a common later stage. Thus $H_c^p(O;\mathcal{L})$ is the colimit of the compact-support groups of these finite unions. A homology cycle uses finitely many compact simplex images, as does a chain bounding it; the same finite-cover argument identifies $H_{n-p}(O;\mathcal{L})$ with the colimit of the stage homology groups. Cap commutes with these maps by [F1]. Surjectivity and injectivity at a common stage, using step 1.1, show that $D_O$ is an isomorphism. No countable family of charts was selected: the only enumeration is the fixed rational enumeration in one supplied chart.

Order the finitely many supplied chart domains $U_1,\dots ,U_m$. Step 2.1 proves duality on $U_1$ and on every intersection $(U_1\cup \cdots \cup U_{j-1})\cap U_j$, which is an open subset of the single chart $U_j$. Induction with the gluing implication of step 1.1 proves it on the entire finite union $N$. All constructions commute with commuting scalar actions because transport, cap, inclusion and restriction do; their inverse isomorphisms therefore do as well. Empty manifolds and all integer degrees are covered by the same exact windows and the coordinate-ball calculation. Each representative comparison uses only finitely many supports and chains. The supplied finite atlas, rational enumeration and individual finite operations introduce no choice axiom.