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.
Connections can change a representative without changing its class
Statement
On the trivial complex line over with coordinates , use the standard Hermitian metric and compare with . Their curvature forms are and . For a line bundle, , so the Chern forms are They are unequal, but so they define the same de Rham class. Both connections are Hermitian for the standard metric.
Facts & Assumptions
Given: The product line , its standard Hermitian metric , and the two displayed connection operators.
For a line bundle, the degree-one determinant coefficient is (Chern, Pontryagin, and Euler characteristic forms).
In a local frame, curvature satisfies (Curvature two-form structure equation).
A connection is Hermitian-compatible when it satisfies the metric derivative identity (Complex-linear and metric-compatible bundle connections).
For degree one, the transgression is the invariant polynomial applied to , and its exterior derivative is the difference of the endpoint curvature evaluations (Explicit Chern–Simons transgression between two connections).
Two closed two-forms define the same real de Rham class precisely when their difference is exact (De rham cohomology).
The product bundle with fibre , regarded as a real vector space, is a smooth trivial real rank-two bundle (Smooth vector bundles, rank, fibres, and trivial bundles).
Chern forms obtained by curvature evaluation are closed (Chern, Pontryagin, and Euler characteristic forms).
Proof
By [F6], is the product line; give its fibres the standard complex structure and . In the global frame, write , where and . Each operator is complex-linear and satisfies , so it is a connection. For either , . Here and , so this equals ; both connections are Hermitian for the stated metric, with the compatibility convention of [F3].
The structure equation [F2] gives . For , and , so .
Expanding the degree-one term of the determinant in the Chern-form definition [F1] gives for this rank-one bundle. Consequently and . The latter is nonzero, since its value on is ; hence the representative forms are not equal.
Put . Direct differentiation gives . This is also the degree-one transgression in [F4]: its polynomial is and , so . Thus the endpoint forms are unequal while [F5] identifies their de Rham classes; [F7] ensures these closed forms represent classes. The example uses only the displayed product bundle and connections; it requires no choice axiom. [F1, F4, F5, F7, step 1.2, step 2.1, given, algebra]
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
28 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
- Stefan Haller, The Atiyah–Singer Index Theorem, Vienna lecture notes (2013) (standard reference, not scraped)