Alphabeta Math
PropositionStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

The orientation system is a local system

Statement

Let M be a boundaryless n-manifold. The published orientation system OM is a functor Π1(M)Z-Mod. For a commutative unital ring R, the stalkwise extension OMR=OMZR is a rank-one R-module local system. At a chosen basepoint of a component, a loop acts on a chosen generator by its orientation character wM:π1(M){±1}.

Facts & Assumptions

Given: A boundaryless n-manifold M and a commutative unital ring R.

[F1]

Orientation local system and orientation cover constructs the stalks Ox=Hn(M,M{x};Z) and transport Tγ depending only on the endpoint-fixed homotopy class of γ; it proves identity, reversal, and concatenation laws.

[F2]

Local systems and pullback defines a local system as a covariant fundamental-groupoid functor.

[F3]

The tensor product MRN from the additive group underlying the free Z-module on M×N, elementary tensors, and finite tensor sums constructs the tensor product as an abelian group generated by elementary tensors, modulo additivity and balancing relations. Its arbitrary-ring definition supplies no further module structure or functoriality.

Proof

technique · direct
1.1

Assign xOx and [γ:xy]Tγ. Homotopy invariance in [F1] makes the arrow map well defined. The constant-path and concatenation identities say respectively that identities and composition in Π1(M) are preserved, while reversal says every transport is an isomorphism. This is precisely the functor required by [F2].

F1F2
1.2

Put (OMR)x=OxZR. On elementary tensors define q(or):=o(qr). The additive and balancing relations in [F3] are preserved by this formula; distributivity, associativity, and the unit law in R therefore make the tensor product a left R-module. For a path γ:xy, the formula orTγ(o)r also preserves every relation in [F3], because Tγ is an additive, hence Z-linear, map. It descends to an R-linear map denoted Tγ1R. Identity and composition agree on elementary tensors, which generate the tensor product, and Tγˉ1R is the inverse. Thus these maps define an R-module local system. Finally, if ox generates Ox, the maps R(OMR)x,roxr,(mox)rmr are well defined inverse R-linear maps by the same relations. Hence every stalk is free of rank one, including the zero ring under the usual rank-one convention RR.

F1F2F3step 1.1
2.1

Fix x and a generator ox. A loop transport is an automorphism of the infinite cyclic group Ox, so Tγ(ox)=wM(γ)ox for a unique sign. Composition in step 1.1 makes wM a homomorphism. It is +1 exactly when the lifted path in the orientation cover returns to the chosen generator sheet, and 1 exactly when it returns to the other sheet, so it is the orientation character. Scalar extension gives the same multiplication by wM(γ) on OxR. Changing ox to ox does not change this sign.

F1step 1.1step 1.2
3.1

For an orientable component, a continuous choice of generator identifies the system with the constant rank-one system; conversely such a trivialization selects one sheet of the orientation cover and orients the component. The empty manifold gives the empty functor, dimension zero gives constant stalks on a discrete space, and disconnected manifolds are handled componentwise. No global generator or path family is selected in the construction, so no AC is used.

F1step 1.2step 2.1

Depends on

Used by

Dependency tree · two levels

17 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