ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck pass

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.

Two projective lines have one mod 2 intersection

Example

Model the real projective plane as ${R P}^{2} = S^{2} / (x \sim - x)$ with its quotient smooth structure (Real projective space from affine charts, Real projective space cover as a discrete fiber fibration). Two distinct projective lines are the images of two distinct great circles of $S^{2}$ (Great circles as round-sphere geodesics); they are embedded circles meeting transversely in exactly one point of ${R P}^{2}$ , because two distinct great circles meet in exactly two antipodal points of $S^{2}$ , which the quotient identifies. Since ${R P}^{2}$ is nonorientable (Positive-dimensional real projective space is orientable exactly in odd dimension), no oriented intersection number of the two lines is available, but the mod 2 intersection number is defined and equals $I_{2} = 1$ ; hence, under ${A C}_{ω}$ for homotopy invariance, the lines cannot be separated by deformation of either or both inclusion maps. This is the paradigm case showing why the parity theory exists.

Facts & Assumptions

Given: Two distinct great circles $C_{1}, C_{2} \subseteq S^{2}$ and the antipodal quotient $q : S^{2} \to {R P}^{2}$ .

[F1]

$S^{2} = F^{- 1} (1)$ for $F (x) = ⟨ x, x ⟩$ on $R^{3}$ with its standard smooth structure is a regular level set ( $d F_{x} (v) = 2 ⟨ x, v ⟩ \neq 0$ for $x \in S^{2}$ ), hence a smooth $2$ -manifold with its standard structure, and $C_{i}$ is the image of a maximal round geodesic, an embedded circle (Euclidean spaces and Euclidean open subsets as smooth manifolds, A regular level set is an embedded submanifold, Great circles as round-sphere geodesics).

[F2]

${R P}^{2} = S^{2} / (x \sim - x)$ has the quotient smooth structure, and $q$ is a two-sheeted covering. On an affine patch $x_{i} \neq 0$ , the ratios $x_{j} / x_{i}$ give its smooth coordinates; on each hemisphere $x_{i} > 0$ or $x_{i} < 0$ the inverse sends an affine coordinate vector to the corresponding normalized vector with the prescribed sign of $x_{i}$ . Thus the local inverse is smooth and $q$ is a local diffeomorphism (Real projective space from affine charts, Real projective space cover as a discrete fiber fibration).

[F3]

For $n \geq 1$ , ${R P}^{n}$ is orientable exactly when $n$ is odd, so ${R P}^{2}$ is nonorientable and admits no integral orientation (Positive-dimensional real projective space is orientable exactly in odd dimension).

[F4]

The mod 2 intersection number of transverse compact complementary-dimensional submanifolds is the cardinality of the intersection modulo two, requires no orientability, and under ${A C}_{ω}$ is invariant under homotopies of either or both inclusion maps, by the two-map diagonal formulation (The mod 2 intersection number, Transverse complementary-dimensional intersection sets, The mod 2 intersection number is homotopy invariant, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Verification

1.1F1givenalgebra

Distinct great circles $C_{1}, C_{2}$ are planes through the origin meeting the sphere, and distinct planes through the origin in $R^{3}$ meet in a line through the origin, which cuts $S^{2}$ in exactly two antipodal points; at such a point $p$ the tangent line $T_{p} C_{i} = p^{⊥} \cap P_{i}$ lies in $T_{p} S^{2} = p^{⊥}$ and determines the plane $P_{i}$ as $span {p, T_{p} C_{i}}$ , so the two tangent lines are distinct one-dimensional subspaces of the two-dimensional $T_{p} S^{2}$ and therefore span it, which is transversality.

2.1F1F2step 1.1algebra

Each great circle is antipodally invariant. Its antipodal quotient is a circle, and the induced map $C_{i} / (\pm 1) \to {R P}^{2}$ is injective. Since its source is compact and its target Hausdorff, it is a homeomorphism onto its image; in the local diffeomorphism charts of [F2] it is the embedded arc $C_{i}$ , hence is a smooth embedding. Saturation of the two $C_{i}$ under the antipodal involution gives $q (C_{1}) \cap q (C_{2}) = q (C_{1} \cap C_{2})$ , a single point. The invertible differential of $q$ carries the two distinct tangent lines of 1.1 to distinct tangent lines in the quotient, preserving transversality.

3.1F3F4step 2.1∎

By [F3] the projective plane is nonorientable, so no oriented intersection number of the two lines is defined. By [F4] the mod 2 intersection number is defined and equals the parity of the intersection, namely $1$ ; under the stated ${A C}_{ω}$ , every homotopic pair of transverse representatives of the two projective lines meets an odd number of times, so the lines can never be deformed to disjoint positions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

68 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

Victor Guillemin and Alan Pollack, Differential Topology (Prentice-Hall, 1974; complete 236-page PDF) (standard reference, not scraped)
John Milnor, Topology from the Differentiable Viewpoint (Princeton University Press; complete 76-page PDF, including the appendix Classifying 1-manifolds) (standard reference, not scraped)