Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-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.

Smooth orientation sign is the local integral homology multiplier

Statement

Fix a dimension n1 and one generator en of Hn(Rn,Rn{0};Z). A smooth orientation on a boundaryless n-manifold determines an integral local-homology orientation by requiring each positive chart centred at p to send its local generator μp to en. This is independent of the positive chart and is a continuous generator section of the orientation local system. Use the same en for all manifolds being compared.

If F is smooth near p, F(p)=q, and dFp is invertible, its induced map on local integral homology carries μp to sgn(dFp)μq. In dimension zero put e0=[point]; the smooth sign ε(p) gives μp=ε(p)[p], and the local multiplier is the product of the source and target point signs. All assertions are choice-free. The local map is formed on a sufficiently small neighbourhood on which p is the only preimage of q.

Facts & Assumptions

[F1]

Local homology detects manifold dimension, interior, and boundary computes the local integral group as infinite cyclic in degree n and zero in the other degrees at an interior point.

[F2]

Long exact sequence of a pair gives the boundary isomorphism used in that identification; on a relative cycle it is represented by its boundary.

[F3]

The singular chain homotopy formula gives the prism identity, including degree zero, for homotopies of the pairs below.

[F4]

Functoriality of relative homology gives composition and inverse maps for pair homeomorphisms.

[F5]

Degree of identity constant reflection and antipodal sphere maps gives degree 1 for every coordinate reflection of Sk when k1.

[F6]

For n1, radial normalisation is a deformation retraction of Rn{0} onto Sn1 gives the displayed radial deformation retraction of punctured Euclidean space onto its unit sphere.

[F7]

Every invertible finite square real matrix is a finite product of elementary matrices gives a finite elementary factorization of an invertible real matrix.

[F8]

Elementary matrices obtained by applying one elementary row operation to an identity matrix lists row additions, nonzero row scalings and row swaps, with no elementary matrix in dimension zero.

[F10]

For same-sized finite square matrices over a commutative ring, det(AB)=det(A)det(B) makes the determinant sign of a product the product of its determinant signs.

[F11]

The total (Fréchet) derivative Df(a) as the linear first-order approximation with o(h2) remainder supplies f(x)=Lx+r(x) with r(x)=o(x) after centring source and target.

[F13]

Local orientation sign of a regular preimage identifies the intrinsic positive-dimensional sign with the determinant in positive bases, and computes the zero-dimensional ray sign.

[F14]

Coordinate-ball classes identify local homology stalks supplies the ball-to-point isomorphisms.

[F15]

R-orientation of a topological manifold defines an integral orientation as a locally constant generator in these ball trivializations.

[F16]

Excision for singular homology identifies the local group after shrinking a neighbourhood of its distinguished point.

Proof

Given: A fixed dimension and Euclidean generator as stated. All homology in this proof has integral coefficients.

1.1

A homotopy H:(X×I,A×I)(Y,B) gives the same induced relative homology map at both ends. Indeed every simplex in A has all its prism simplices mapped into B, so the operator of [F3] passes to quotient chains. Its identity g#f#=P+P then says that the two images of any relative cycle differ by a relative boundary. The same reasoning includes degree zero and unnormalized degenerate simplices. Also the boundary map [F2] commutes with maps of pairs, because f#c=f#c on each representative.

F2F3F4given
2.1

Let Ji be reflection of one coordinate of Rn. Since Rn is contractible, its pair sequence [F2] identifies Hn(Rn,Rn0) naturally with H~n1(Rn0). The radial deformation retraction [F6] identifies the latter group with H~n1(Sn1) and commutes with Ji, because radial normalization satisfies r(Jix)=Jir(x). For n2 this action is 1 by [F5]. For n=1, the two components of the punctured line have classes [+] and [], and the augmentation kernel is generated by [+][]; reflection interchanges them and negates their difference. Hence every Ji acts as 1 on the infinite cyclic local group [F1], regardless of which generator was chosen.

F1F2F5F6step 1.1
3.1

Compute the action of the elementary matrices in [F8] on the pair (Rn,Rn0). A shear I+cEij, ij, is homotopic to the identity through I+tcEij, whose inverse is ItcEij; thus its action is +1 by step 1.1. A positive coordinate scaling c>0 is homotopic to the identity by replacing c with (1t)+tc>0, so also acts as +1. A negative scaling is a positive scaling followed by Ji, hence acts as 1 by [F4] and step 2.1. A swap of coordinates i,j is conjugate to a coordinate reflection: use the basis with vectors ei+ej and eiej in that plane and the other standard basis vectors elsewhere; the swap has eigenvalues +1,1 on those two specified vectors. Conjugation does not change its local multiplier, since every invertible change of basis induces an automorphism of the same cyclic group by [F4], and conjugating multiplication by 1 leaves it 1. These multipliers equal the determinant signs in [F9].

F4F8F9step 1.1step 2.1
4.1

Factor any LGLn(R) into finitely many elementary matrices by [F7]. Functoriality [F4] and step 3.1 multiply their local multipliers, while [F10] multiplies their determinant signs. Thus Len=sgndet(L)en. The empty factorization gives the identity multiplier +1. This proof requires no connectedness theorem for the general linear or orthogonal group and selects only a finite factorization of the one matrix.

F4F7F10step 3.1
5.1

Let f be a centred smooth coordinate representative with f(0)=0 and invertible L=Df(0). By [F12], choose C>0 with L1vCv, hence LxC1x. By [F11] choose a small ball about zero contained in the coordinate domain and on which r(x)(2C)1x, where r(x)=f(x)Lx. Then H(x,t)=Lx+tr(x),H(x,t)(2C)1x(x0, 0t1). Thus this is a homotopy of pairs from the linear map to f, into (Rn,Rn0), and f has no other zero in the ball. By [F16], inclusion of this small ball identifies its local group with the whole Euclidean local group; shrinking again does not change the map by [F4]. Steps 1.1 and 4.1 prove that the germ multiplier is sgndetDf(0). No local inverse theorem is needed for this homology calculation.

F4F11F12F16step 1.1step 4.1
6.1

At p in an oriented smooth manifold choose a positive chart centred at p and use [F16] to pull en back to μp. Two such charts are related by a smooth transition fixing zero with positive derivative determinant, by [F13]. Step 5.1 says the transition induces multiplication by +1 on the local group, so the two values μp agree. This defines one generator at every point by a unique chart-independent value; it does not select a chart at every point.

F13F16step 5.1
7.1

Verify local continuity in the precise sense of [F15]. Inside one positive chart choose concentric balls K=B(0,r)B(0,s). By [F14], choose the unique class over K whose restriction at zero is the generator from step 6.1. Let ρ satisfy r<ρ<s. Excision [F16] identifies the supported pair with (B(0,s),B(0,s)K); since the ball is contractible, the boundary map [F2] identifies its degree-n relative group with reduced degree-(n1) homology of the annulus. Radial deformation onto Sρ shows that the boundary class is represented by a sphere class there. For xintK, restriction to the local pair at x and translation of the target by x sends this sphere map to uux. The homotopy uutx avoids zero because x<r<ρ, so step 1.1 and naturality of [F2] identify its class with uu. This is exactly the generator defined using the chart centred at x in step 6.1. The calculation works for n=1 on reduced H0 as well. Hence the restrictions of the one ball class are all the μx, proving that this is a continuous generator section by [F15].

F2F14F15F16step 1.1step 6.1
8.1

For the given germ F choose positive centred charts on source and target. The local map in these charts is exactly the one in step 5.1, so Fμp=sgndet(Df(0))μq=sgn(dFp)μq by [F13]. The local map is independent of shrinking and charts by [F4], [F16] and step 6.1. Changing the common reference en to en negates all source and target generators and leaves this multiplier unchanged.

F4F13F16step 5.1step 6.1step 7.1
9.1

When n=0, each singleton chart is open and its local group is Z[p] by [F1]. The section ε(p)[p] is continuous on the discrete manifold. The unique local point map sends [p] to [q], so its multiplier in these signed generators is ε(p)ε(q), as in [F13]. Empty manifolds impose an empty section condition, and no germ at an absent point. Singular derivatives are excluded; the remainder estimate in step 5.1 explicitly excludes zero along the entire homotopy except at its fixed origin. All homotopy endpoints and the identity/empty-factorization case are included. One reference generator for the fixed dimension and finitely many witnesses for one germ suffice; no family of generators over dimensions, charts, or points is chosen, and no AC occurs.

F1F4F13step 1.1step 4.1step 5.1step 6.1step 7.1step 8.1

Depends on

Used by

Dependency tree · two levels

67 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