Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

Zero th de rham cohomology is locally constant functions

Statement

HdR0(M) is the algebra of locally constant real functions. For nonempty connected M it is canonically R.

Facts & Assumptions

Given: A smooth real function f on M; B0=0.

[F1]

De rham cohomology: The real de Rham cohomology is HdRk(M)=Zk(M)/Bk(M), with Zk,Bk as in def-closed-and-exact-differential-forms. This is def-cohomology-object-of-a-cochain-complex in real vector spaces. Only a closed form ω represents a class [ω]. For closed forms ω,ω′, equality [ω]=[ω′] means precisely ω′−ω=dη for some (k−1)-form η. Addition and real scalar multiplication are induced by those of forms. All groups on the empty manifold are zero.

[F2]

The local coordinate formula for the exterior derivative: Let (U,x1,…,xn) be a smooth chart on a smooth manifold and ω a smooth k-form on U, with k≥0. Summing over increasing k-tuples I, and writing dxI=dxi1∧⋯∧dxik, if ω=∑IωI dxI, then dω=∑IdωI∧dxI.

[F3]

Newton–Leibniz needs only continuity on [a,b], differentiability on (a,b), and a Riemann-integrable extension of the interior derivative: Let a<b. Suppose G:[a,b]→R is continuous on [a,b] and differentiable on (a,b). If f:[a,b]→R is Riemann integrable and f(x)=G′(x)(a<x<b), then ∫abf=G(b)−G(a). No derivative of G at either endpoint is assumed, and the two endpoint values assigned to the integrable extension f do not enter the conclusion.

Proof

technique · direct
1.1F2F3given

In a coordinate ball, df=∑i∂if dxi. If df=0, for points x,y in that ball set h(t)=f(x+t(y−x)). The chain rule gives h′(t)=∑i(yi−xi)∂if=0; the fundamental theorem gives f(y)−f(x)=∫010 dt=0. In dimension zero each coordinate ball is a singleton, so the same constancy conclusion holds.

2.1F1F2step 1.1

Conversely, a locally constant function is smooth and has zero coordinate derivatives, hence df=0. Since B0=0, the quotient in degree zero identifies each such function with itself, preserving addition and multiplication.

3.1step 1.1step 2.1given∎

If M is nonempty and connected, fix p∈M. The level set f−1(f(p)) and its complement are open by local constancy; connectedness forces the complement empty. Thus f is the constant f(p), and a↦(p↦a) is the asserted algebra isomorphism. On the empty manifold the function space is zero.

Source locator

Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 17, pp.441–443, Proposition 17.2 and Corollary 17.3; local quotient calculations below.

Depends on

Dependency tree · 2 levels

Sources