Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedaudited 2026-09-22
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.

Real projective bundle and tautological line

Definition

Let E→B be a numerable real vector bundle of rank n≥1 over an arbitrary topological base, with linear trivializing cover (Ui)i∈I and transition functions gji:Ui∩Uj→GL⁡n(R). Write RPn−1 for the space of lines (one-dimensional linear subspaces) of Rn, and for a linear isomorphism g let [g] denote the induced homeomorphism of RPn−1.

The projective bundle P(E)→B is the quotient P(E)=(∐iUi×RPn−1)/∼,(x,ℓ)∼(x,[gji(x)]ℓ) for x∈Ui∩Uj, with the quotient topology, and p:P(E)→B induced by the first-coordinate maps; here P(E) is to be read as the chosen quotient model, whose identity as a topological space over B is checked in the Verification. Its fiber over b is P(Eb), the projectivization of the fiber Eb, so it is a locally trivial fiber bundle with fiber RPn−1 in the sense of Locally trivial fiber bundle, numerated by the same cover and partition of unity that numerates E.

The tautological line γE is the quotient γE=(∐iUi×γn−1)/∼,(x,ℓ,v)∼(x, [gji(x)]ℓ, gji(x)v), where γn−1={(ℓ,v)∈RPn−1×Rn:v∈ℓ} is the tautological line over RPn−1 and the equivalence is formed on the overlap Ui∩Uj. The coordinates (x,ℓ) give a map γE→P(E) whose fiber over a point (b,L) of P(E) is recognized with the line L⊆Eb itself; it is a rank-one real vector bundle over P(E).

Assuming AC, by Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses, P(E) is again a paracompact Hausdorff CGWH space of CW type whenever B is a paracompact Hausdorff CGWH space of CW type, since it is the total space of a numerable bundle with compact fiber RPn−1; the Verification below records the same numeration statement.

Two degenerate cases are fixed by convention. For n=1 the fiber RP0 is a point, P(E)≅B over B, and γE corresponds to E under this identification. For n=0 the projectivization of a zero-dimensional space carries no line; we set P(E)=∅ and let γE be the empty bundle over the empty space. For the empty base both P(E) and γE are empty.

The projective and tautological quotient constructions and their supplied numerations below require no choice. AC is assumed only for the asserted paracompactness/CW-type consequence.

Facts & Assumptions

Given: A numerable real rank-n bundle E→B over an arbitrary topological base with a linear trivializing cover (Ui) and transition functions gji, and the notation above.

[F1]

Linear charts of E have transition functions gji:Ui∩Uj→GL⁡n(R) satisfying gii=I and gki=gkjgji, and a numeration consists of such charts together with a locally finite partition of unity subordinate to the cover (Real and complex topological vector bundles).

[F2]

The quotient of ∐iUi×Fn by the cocycle relation is a vector bundle with charts Φi, and every rank-n bundle is recovered from the cocycle of any linear atlas (Vector bundles are glued from transition cocycles).

[F3]

A locally trivial fiber bundle is a continuous projection together with fiber homeomorphisms θi:p−1(Ui)→Ui×F over Ui, and its overlap changes are the corresponding homeomorphism-valued cocycles (Locally trivial fiber bundle).

[A1]

For the total-space consequence only, assume the Axiom of Choice (The Axiom of Choice).

[F5]

Under AC, a numerable compact-Hausdorff-fiber bundle over a paracompact Hausdorff base has paracompact Hausdorff total space; if the base is CGWH, so is the total space, and if the base and fiber have CW homotopy type, so does the total space (Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses).

Verification

1.1F1F2F4

The projectivized transitions are well defined and obey the cocycle law. For x∈Ui∩Uj the linear isomorphism gji(x) carries lines to lines and depends continuously on x, so the joint map (x,ℓ)↦[gji(x)]ℓ is continuous. Indeed on a projective coordinate chart choose the representative with a specified coordinate equal to one, apply the continuous matrix, and take its nonzero-vector projective quotient. The identities of [F1] give [gii(x)]=id⁡ and [gki(x)]=[gkj(x)][gji(x)] for x∈Ui∩Uj∩Uk, because projectivization is functorial for composition of linear isomorphisms. Reading the displayed relation on the overlaps, the cocycle law makes ∼ reflexive, symmetric and transitive: it is the same calculation as in [F2] with [gji] in place of gji. Therefore the quotient P(E) exists, and the induced projection p:P(E)→B is continuous by [F4], since its composite with the quotient map is the first-coordinate projection on each summand.

2.1F1F3F4step 1.1

The quotient is a numerable fiber bundle with fiber RPn−1. Let Q:∐iUi×RPn−1→P(E) be the quotient map. It is open: if O is open in the disjoint union, then on the j-th summand the saturation Q−1Q(O) is the union, over i, of the images of O∩((Ui∩Uj)×RPn−1) under the overlap homeomorphisms (x,ℓ)↦(x,[gji(x)]ℓ), and is therefore open. Thus Q(O) is open by the definition of the quotient topology. It follows that the restrictions of Q to the i-th summands are open onto p−1(Ui). The maps Φi:p−1(Ui)⟶Ui×RPn−1,Φi[x,ℓ,k]=(x,[gik(x)]ℓ) are well defined, continuous by [F4], and inverse over Ui to the maps (x,ℓ)↦[x,ℓ,i]; the latter maps are open by the preceding calculation. Hence they are homeomorphisms over Ui, so P(E) is a locally trivial fiber bundle with fiber RPn−1 in the sense of [F3]. The given numerating cover and partition of unity of E serve unchanged, since the chart domains are the same Ui and their supports are already subordinate; hence P(E) is numerable.

3.1F1F3F4step 1.1step 2.1

The tautological quotient has the local bundle descriptions Ui×γn−1: the same open-saturation argument as in step 2.1 applies to the overlap homeomorphisms (x,ℓ,v)↦(x,[gji(x)]ℓ,gji(x)v). Inside each such description refine the base by Di,a={(x,ℓ):va≠0 for 0≠v∈ℓ}, for 1≤a≤n. The unique vector wa(ℓ)∈ℓ with coordinate a equal to one is a continuous nonzero section. The map (x,ℓ,t)↦(x,ℓ,twa(ℓ)) and its inverse, which reads the a-th coordinate of the vector, are continuous linear bundle charts. Thus the tautological quotient is a rank-one real bundle with the asserted fiber, not generally trivial over all of p−1(Ui).

3.2A1F5step 2.1

If B is paracompact Hausdorff CGWH of CW type and AC is assumed, [F5] applies to the numerable projective bundle of step 2.1: the fiber is the compact Hausdorff finite CW space RPn−1. It follows directly that P(E) is paracompact Hausdorff, CGWH, and of CW type, which is the asserted total-space consequence.

4.1F1step 2.1step 3.1

An explicit refined numeration needs no choice. In chart i put si,a(ℓ)=va2/∑bvb2, independent of the nonzero representative, and di,a=max⁡(si,a−1/(2n),0). Since some si,a≥1/n, the sum Di=∑adi,a is positive. Put θi,a=di,a/Di, and define ψi,a=(ρi∘p)θi,a on p−1(Ui), extended by zero elsewhere. This extension is continuous since points outside Ui have a neighborhood disjoint from the closed support of ρi. The family is locally finite, because the base family is locally finite and there are only n coordinates for each i. Its sum is one. Its closed support lies in p−1(supp⁡ρi) and in the locus si,a≥1/(2n), hence inside Di,a. It is therefore support-subordinate to the actual line charts of step 3.1, proving numerability of γE.

5.1A1F1F5step 1.1step 2.1step 3.1step 3.2step 4.1∎

For n=1, the projective fiber is a point, so the displayed charts identify P(E) with B and γE with E. Rank zero uses only the declared empty-space convention, not the formulas involving 1/(2n). An empty base gives empty quotients. Steps 1.1, 2.1, 3.1 and 4.1 use the supplied charts and partition and finite coordinate operations only; AC enters solely in step 3.2 through [F5].

Depends on

Dependency tree · 2 levels

Sources