ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

Coordinate circles give the alternating intersection matrix of a torus

Example

Assume AC. Let $T^{2} = Q \times Q$ with $Q = R / Z$ carry the product smooth structure and orientation, and let $A = Q \times {[0]}$ , $B = {[0]} \times Q$ be the coordinate circles. Then $A, B$ are closed oriented embedded circles and the geometric pairing of The geometric intersection pairing on a closed oriented manifold takes the values $⟨ A, A ⟩ = 0, ⟨ B, B ⟩ = 0, ⟨ A, B ⟩ = 1, ⟨ B, A ⟩ = - 1,$ so the pairing $⟨ x, y ⟩ = ⟨ P D [x] ⌣ P D [y], [T^{2}] ⟩$ has, on the classes $[A], [B]$ , the alternating matrix $(\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array})$ of determinant $1$ ; in particular it is alternating on these classes and the factor order matters. The self-intersections vanish because each coordinate circle projects to a point in the other factor, so it can be pushed off itself by translating in the other factor along a nowhere-zero normal field.

Facts & Assumptions

Given: AC, the torus $T^{2} = Q \times Q$ with $Q = R / Z$ , its product smooth structure and orientation, and the coordinate circles $A = Q \times {[0]}$ , $B = {[0]} \times Q$ .

[F1]

$Q = R / Z$ is the quotient circle; the interval charts constructed in step 1.1 give its smooth structure and increasing orientation. Its product then has the product smooth structure and orientation (The two-dimensional torus $T^{2} = (R / Z)^{2}$ , The circle as $S^{1} = R / Z$ with basepoint $[0]$ , Products of smooth manifolds have a canonical product smooth structure, Product orientations).

[F2]

A regular level set of a smooth function is an embedded submanifold, and the coordinate circles are regular level sets of the coordinate projections (A regular level set is an embedded submanifold, Canonical tangent and cotangent splittings for products).

[F3]

The geometric pairing is $⟨ A, B ⟩_{M} = I (A, B) = I (i_{A}, B)$ evaluated on transverse representatives, first factor first, and swapping the factors gives $I (B, A) = (- 1)^{a b} I (A, B)$ (The geometric intersection pairing on a closed oriented manifold, Intersection number under factor interchange).

[F4]

The self-intersection is $A \cdot A = ⟨ e (ν_{A}), [A] ⟩$ , and a nowhere-zero normal field forces it to vanish (The self-intersection number of a complementary-dimensional oriented submanifold, The self-intersection number is the Euler number of the normal bundle).

[F5]

The geometric pairing equals the Poincare-dual cup pairing, $I (A, B) = ⟨ P D [A] ⌣ P D [B], [M] ⟩$ , with the cap-duality map $D_{M} (a) = a \cap [M]$ (The geometric intersection number is the Poincare-dual cup pairing, The cap-duality map of an oriented manifold).

Verification

technique · compute one transverse signed intersection and use the nowhere-zero normal fields for the self-intersections; the cup-pairing identification is the cited theorem

1.1F1F2F3algebra

Give $Q$ quotient charts by intervals of length less than one: the quotient projection is injective on each interval and open, since the saturation of an open interval is the union of its integer translates. Its restriction is therefore a homeomorphism onto an open set of $Q$ . Chart changes on overlap components are integer translations, hence smooth and increasing. The quotient is Hausdorff: distinct classes have lifts whose difference is not an integer, and sufficiently small intervals about them have disjoint integer saturations. Images of rational-endpoint intervals give a countable base because the quotient projection is open. These charts cover $Q$ , define the smooth structure and orientation, and identify its tangent frame with $\partial_{x}$ . The image of $[0, 1]$ is all of $Q$ , so it is compact and boundaryless. In the product charts, $A$ and $B$ are embedded circles cut out by the coordinate projections [F1], [F2], and they meet transversely in the single point $([0], [0])$ with $T_{([0], [0])} A = R \partial_{x}$ , $T_{([0], [0])} B = R \partial_{y}$ and $(\partial_{x}, \partial_{y})$ the positive product frame. Hence $⟨ A, B ⟩ = 1$ and, by [F3] with $a b = 1$ , $⟨ B, A ⟩ = - 1$ .

1.2F4F1algebra

For the self-intersections: the constant field $\partial_{y}$ restricted to $A$ is a nowhere-zero section of the normal bundle of $A$ (the normal bundle is identified with the $y$ -factor along $A$ ), and likewise $\partial_{x}$ for $B$ ; by [F4], together with A nowhere-zero section forces the Euler data to vanish, the corresponding push-offs are disjoint, so $⟨ A, A ⟩ = 0$ and $⟨ B, B ⟩ = 0$ .

2.1F5step 1.1step 1.2∎

By [F5] the same numbers are $⟨ P D [x] ⌣ P D [y], [T^{2}] ⟩$ evaluated on the two classes, giving the displayed matrix: the factor order contributes the minus sign in degree one, and the determinant of the matrix on the classes displayed is $1$ . For $x = m [A] + n [B]$ and $y = p [A] + q [B]$ , bilinearity gives $⟨ x, y ⟩ = m q - n p$ , which vanishes when $x = y$ . This is the usual alternating (symplectic) block; its displayed signs specify the convention completely. No nondegeneracy claim for the whole pairing on $H_{1} (T^{2}; Z)$ is made here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

106 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)
Ralph L. Cohen, Bundles, Manifolds, and Homotopy (author draft bookR4) (standard reference, not scraped)
Eleny-Nicoleta Ionel (notes by Andrew Lin), Stanford Math 215B Differential Topology, Winter 2023 (complete 63-page lecture notes) (standard reference, not scraped)