Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-09-07
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.

Tangent and cotangent bundles extend over a boundary

Statement

For a smooth n-manifold with boundary, derivations of smooth boundary germs form an n-dimensional tangent space at every point, and the usual tangent and cotangent bundles have smooth boundary-chart transition maps.

Facts & Assumptions

Given: A smooth n-manifold M with boundary and a point p∈M.

[L1]

Smooth Euclidean extensions that agree on a half-space have the same derivatives there (Half-space extensions agreeing on a relatively open set have the same derivatives there).

[L2]

Derivations annihilate constant germs, and smooth Euclidean functions admit first-order Hadamard factorization (A derivation annihilates constant germs; First-order Hadamard factorization near a point).

[L3]

The cotangent space is the algebraic dual of the tangent space (Cotangent space and cotangent bundle as a disjoint union).

[L4]

Boundary-chart transitions are smooth half-space diffeomorphisms, and their derivatives obey the chain rule (Smooth charts, atlases, and structures with boundary; Chain rule for smooth half-space maps).

Proof

technique · direct
1.1givenL1L2constructalgebra

If n=0, every smooth germ is constant, so [L2] makes every derivation zero and the empty coordinate family is a basis. Assume n≥1. For a boundary germ, define ∂i∣p by differentiating any smooth Euclidean extension in the ith coordinate. By [L1] this is well defined; linearity and the Euclidean product rule make it a derivation.

2.1givenL1L2step 1.1algebra

Let v be any derivation and let F extend a representative of a boundary germ f near the coordinate point a. By [L2], write F(x)−F(a)=∑i(xi−ai)gi(x) with gi(a)=∂iF(a). Restricting to the half-space and applying v, using [L2] and the Leibniz rule, gives v(f)=∑iv(xi)∂i∣p(f). Thus the coordinate derivations span. Applying a linear relation among them to each coordinate germ proves independence, so dim⁡TpM=n.

3.1givenL1L3L4step 1.1step 2.1algebra∎

By [L4], differentiating a boundary-chart transition and its inverse gives mutually inverse matrices; [L1] makes these derivatives extension independent, and their entries vary smoothly. They are the tangent transition maps. By [L3], the dual inverse matrices are the cotangent transition maps. Hence the usual tangent and cotangent bundles extend smoothly over all of M, including the n=0 case with empty matrices.

Depends on

Used by

Dependency tree · two levels

15 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