Isotropic cotangent transport and discrete critical values

Suppose a function has derivative constrained to an isotropic cotangent set. Why should its selected values be locally finite? There are two issues: selected points may escape to infinity, and selected values may accumulate near a point that stays in a compact set. Properness controls the first issue. An analytic curve and the canonical one-form settle the second.

We first prove this directly on the source manifold. We then establish the two cotangent transports, including their singular-set form calculus and the variable-rank linear-image argument. This also recovers the critical-value conclusion through the cotangent bundle of the line. Manifolds are finite dimensional, real analytic, Hausdorff and countable at infinity. Conic means invariant under every strictly positive fibre scale. No coefficient ring or sheaf finiteness condition enters these geometric results.

Kashiwara–Schapira’s Microlocal Study of Sheaves, Astérisque 128 (1985) uses canonical forms to establish proper cotangent transport. We give its compactness and singular-form steps below, alongside a direct critical-set proof using analytic curve selection.

Programme exposition: CC0. AI contributors: GPT-6.1 Sol and GPT-6 Astra (OpenAI), Ultra, October 2026.

Exact geometric inputs

We use the following foundational results as prerequisites:

  1. Subanalytic sets are closed under finite Boolean operations, closure and analytic inverse image. Their regular loci are subanalytic and dense. A regular point has an ambient neighborhood in which the set is a closed analytic submanifold.
  2. If a point lies in the closure of a subanalytic set, an analytic curve through that point enters the set at every sufficiently small positive parameter. Squaring the parameter gives a two-sided version if needed. This applies to the auxiliary subanalytic sets used below.
  3. An analytic map proper on the closure of a subanalytic subset has subanalytic image of that subset. The subset itself need not be closed.
  4. Every closed subanalytic set admits a proper surjective analytic parametrization by a manifold. For the analytic map in (C9), we use the analytic critical-value theorem, (A1)–(A8). Its analytic Taylor, implicit-function and constant-rank inputs remain explicitly stated calculus prerequisites.

Subanalytic sets and limiting tangent directions states the geometric prerequisites in their wider normal-cone setting. Its local curve-selection reduction identifies the required analytic preparation and cell/Puiseux inputs. Here items 1–2 suffice for the direct critical-value proof, together with elementary compactness and one-variable calculus. Items 3–4 enter the general image theorems later.

Testing a one-form along approaches to a singular set

For an analytic one-form θ\theta and subanalytic E⊂ME\subset M, write θ|E=0\theta|_E=0 when the form kills every tangent vector at every regular point of EE. It does not mean that the ambient covector is zero. In a coordinate chart define the point cone by

Cx(E)={v:zj∈E,zj→x,cj>0,cj→∞,cj(zj−x)→v}.(C1) C_x(E)=\{v:\ z_j\in E,\ z_j\to x,\ c_j>0,\ c_j\to\infty, \ c_j(z_j-x)\to v\}. \qquad\text{(C1)}

The definition also makes sense at x∉Ex\notin E. Coordinate changes carry the limiting vector by their derivative, by first-order Taylor expansion.

Form test. The condition θ|E=0\theta|_E=0 is equivalent to θx(v)=0\theta_x(v)=0 for every ambient xx and v∈Cx(E)v\in C_x(E).

Proof. First, replacing EE by its regular locus does not change (C1). Given a representing sequence, density provides regular wjw_j with ∥wj−zj∥<1/(jcj)\|w_j-z_j\|<1/(j c_j). The scaled error tends to zero. The same argument shows Cx(E)=Cx(E¯)C_x(E)=C_x(\overline E).

Suppose v≠0v\ne0 is in (C1). In a chart around xx, the subanalytic set

{(z,r,w):z∈Ereg,r>0,z−x=rw}(C2) \{(z,r,w):z\in E_{\mathrm{reg}},\ r>0,\ z-x=rw\} \qquad\text{(C2)}

has (x,0,v)(x,0,v) in its closure: take rj=1/cjr_j=1/c_j and wj=cj(zj−x)w_j=c_j(z_j-x) after the regular approximation. Curve selection gives analytic z(t),r(t),w(t)z(t),r(t),w(t), with that endpoint, lying in (C2) for positive tt. There is a finite k≥1k\ge1 and b>0b>0 with r(t)=btk+O(tk+1)r(t)=bt^k+O(t^{k+1}), since rr is analytic, positive for positive tt, and zero at zero. Consequently

z(t)=x+btkv+O(tk+1),0=θz(t)(z′(t))=bktk−1θx(v)+O(tk).(C3) z(t)=x+bt^k v+O(t^{k+1}),\qquad 0=\theta_{z(t)}(z'(t))=bk t^{k-1}\theta_x(v)+O(t^k). \qquad\text{(C3)}

At each positive parameter the curve lies locally in the regular manifold, so the first equality to zero follows from the hypothesis. Divide by tk−1t^{k-1} and take the limit. The zero vector needs no argument. Conversely any tangent vector at a regular point is obtained in (C1) from a smooth curve with that derivative. This proves the equivalence. ▫\square

Analytic pullback, closure and union. If h:M′→Mh:M'\to M is analytic, E′,EE',E are subanalytic, and h(E′)⊂Eh(E')\subset E, then

θ|E=0⟹(h*θ)|E′=0.(C4) \theta|_E=0\quad\Longrightarrow\quad(h^*\theta)|_{E'}=0. \qquad\text{(C4)}

Indeed, a sequence for v∈Cx′(E′)v\in C_{x'}(E') gives cj(h(zj)−h(x′))→dhx′vc_j(h(z_j)-h(x'))\to dh_{x'}v: the first-order remainder multiplied by cjc_j tends to zero because cj∥zj−x′∥c_j\|z_j-x'\| is bounded. Apply the form test. Equality of the cones of EE and E¯\overline E proves that vanishing passes to the closure and back. For a locally finite union, every convergent sequence lies locally in finitely many members; a subsequence lies in one member. Thus its point cone is the union of their cones, and vanishing on the members implies vanishing on their union. In particular, (C4) applies to a subset wholly contained in the singular locus; regularity of its image points is not assumed.

For T*XT^*X, let αX\alpha_X be the canonical one-form, α(x,ξ)(v)=ξ(dπ(v))\alpha_{(x,\xi)}(v)=\xi(d\pi(v)). A conic subanalytic Λ\Lambda is isotropic here when αX|Λ=0\alpha_X|_\Lambda=0. This agrees with symplectic isotropy on its regular locus: in coordinates α=∑ξidxi\alpha=\sum\xi_i dx_i, dα=∑dξi∧dxid\alpha=\sum d\xi_i\wedge dx_i; the radial vector R=∑ξi∂ξiR=\sum\xi_i\partial_{\xi_i} is tangent to the regular locus and satisfies ιRdα=α\iota_Rd\alpha=\alpha. Hence vanishing of the two-form implies vanishing of the one-form, while differentiating the pulled-back one-form proves the converse.

Critical values directly from analytic curves

Let φ:X→ℝ\varphi:X\to\mathbb R be analytic and Λ⊂T*X\Lambda\subset T^*X closed, conic, subanalytic and isotropic. Assume that φ|π(Λ)\varphi|_{\pi(\Lambda)} is proper. The selected values are

Sφ={φ(x):dφx∈Λ}.(9) S_\varphi =\{\varphi(x):d\varphi_x\in\Lambda\}. \qquad\text{(9)}

Microlocal Bertini–Sard theorem. The set SφS_\varphi is closed and locally finite in the ambient line. Equivalently, every compact interval meets it in a finite set.

Proof. Introduce the analytic derivative section s(x)=(x,dφx)s(x)=(x,d\varphi_x). Its selected source set is

E=s−1(Λ),s*αX=dφ,dφ|E=0.(C5) E=s^{-1}(\Lambda),\qquad s^*\alpha_X=d\varphi, \qquad d\varphi|_E=0. \qquad\text{(C5)}

The set EE is closed and subanalytic, and the final assertion follows from (C4). If x0∈Ex_0\in E, then φ\varphi is constant on EE in some neighborhood of x0x_0. Otherwise the subanalytic set E\φ−1(φ(x0))E\setminus\varphi^{-1}(\varphi(x_0)) would have x0x_0 in its closure. Select an analytic curve γ\gamma through x0x_0 entering this set. Apply (C4) to γ:(0,ϵ)→E\gamma:(0,\epsilon)\to E. Then

(φ∘γ)′(t)=0(0<t<ϵ),φ(γ(t))=φ(x0).(C6) (\varphi\circ\gamma)'(t)=0\quad(0<t<\epsilon), \qquad \varphi(\gamma(t))=\varphi(x_0). \qquad\text{(C6)}

The second equality follows from the first by the mean value theorem and continuity at zero. It contradicts the chosen set. This argument needs no connected-component enumeration, uniformization or Sard theorem.

For compact J⊂ℝJ\subset\mathbb R, the set π(Λ)∩φ−1(J)\pi(\Lambda)\cap\varphi^{-1}(J) is compact by the stated properness. The closed subset E∩φ−1(J)E\cap\varphi^{-1}(J) is compact too. The neighborhoods on which φ|E\varphi|_E is constant cover it, so finitely many suffice. Its image Sφ∩JS_\varphi\cap J is therefore finite. A subset of the line finite on every compact interval is locally finite and closed: a convergent sequence of distinct points would lie in a single compact interval. ▫\square

The support includes zero covectors. Positive conicity and closedness imply

π(Λ)={x:(x,0)∈Λ}.(C7) \pi(\Lambda)=\{x:(x,0)\in\Lambda\}. \qquad\text{(C7)}

Indeed, scaling any member of a nonempty fibre to zero stays in the closed set; the reverse inclusion is immediate. Thus the support is itself closed and subanalytic. Properness is required only there, not on all of XX.

The same proof applies to the negative test −dφx∈Λ-d\varphi_x\in\Lambda, using s−(x)=(x,−dφx)s_-(x)=(x,-d\varphi_x) and s−*α=−dφs_-^*\alpha=-d\varphi. Each signed value set is closed and locally finite; so is their union. The hypotheses impose positive conicity, not invariance under the antipodal map.

Detecting vanishing after a surjective analytic map

The transport theorems need the converse of (C4). Suppose h(E′)=Eh(E')=E, with both subsets subanalytic. Then

(h*θ)|E′=0⟹θ|E=0.(C8) (h^*\theta)|_{E'}=0\quad\Longrightarrow\quad\theta|_E=0. \qquad\text{(C8)}

To prove it, pass to T=E′¯T=\overline{E'} using the closure argument above and choose a proper analytic uniformization q:W→Tq:W\to T. Pullback gives (hq)*θ=0(hq)^*\theta=0 on the manifold WW. Around a regular point of EE, choose VV such that E∩V=NE\cap V=N is a closed analytic submanifold of VV. Then E¯∩V=N\overline E\cap V=N. Continuity and surjectivity give E⊂h(T)⊂E¯E\subset h(T)\subset\overline E, so

hq:(hq)−1(V)⟶Nis surjective.(C9) hq:(hq)^{-1}(V)\longrightarrow N \quad\text{is surjective.} \qquad\text{(C9)}

The domain (hq)−1(V)(hq)^{-1}(V) is an open analytic manifold and the map (C9) is analytic into the embedded analytic manifold NN. Both have countable atlases. For positive-dimensional NN, the analytic critical-value theorem makes regular values dense in each target chart: critical values have measure zero, and surjectivity ensures a lift at every value. This invokes only that theorem’s standalone calculus proof, not the later conormal or isotropic results in its host lesson. At a regular value, an onto differential lifts every tangent vector of NN; the zero pullback therefore kills every such vector. Continuity of θ|N\theta|_N extends this to all points of NN. When dim⁡N=0\dim N=0, tangent spaces vanish. This proves (C8) at every regular point. Properness was used for the available uniformization; it was not imposed on hh, and we did not infer that an arbitrary analytic image is subanalytic.

The two cotangent maps

For an analytic f:Y→Xf:Y\to X, set

Cf=Y×XT*X,fπ:Cf→T*X,fd:Cf→T*Y.(1) C_f=Y\times_XT^*X, \qquad f_\pi:C_f\to T^*X, \qquad f_d:C_f\to T^*Y. \qquad\text{(1)}

Their action is

fπ(y;ξ)=(f(y);ξ),fd(y;ξ)=(y;dfytξ).(2) f_\pi(y;\xi)=(f(y);\xi),\qquad f_d(y;\xi)=(y;df_y^t\xi). \qquad\text{(2)}

They commute with positive fibre scaling, and the second is linear over YY, with no constant-rank hypothesis. In local coordinates both pulled-back canonical forms are ∑iξidfi(y)\sum_i\xi_i\,d f_i(y). Thus

fd*αY=fπ*αXon Cf.(3) f_d^*\alpha_Y=f_\pi^*\alpha_X \quad\text{on }C_f. \qquad\text{(3)}

These conventions use the transpose differential with its displayed positive sign. No antipodal map enters this identity.

Proper direct transport

Given conic subanalytic isotropic ΛY⊂T*Y\Lambda_Y\subset T^*Y, define

A=fd−1(ΛY)⊂Cf,Df(ΛY)=fπ(A).(5) A=f_d^{-1}(\Lambda_Y)\subset C_f, \qquad D_f(\Lambda_Y)=f_\pi(A). \qquad\text{(5)}

Direct-transport theorem. If the actual restriction fπ|A:A→T*Xf_\pi|_A:A\to T^*X has compact inverse images of compact sets, then Df(ΛY)D_f(\Lambda_Y) is closed, conic, subanalytic and isotropic. Closedness of ΛY\Lambda_Y is not an additional hypothesis.

Proof. The set AA is subanalytic and conic. Its stated properness forces it to be closed in the correspondence manifold: if aj∈Aa_j\in A converges to aa, the images and their limit form a compact target set KK. The compact inverse image of KK in AA is also compact, hence closed, in the Hausdorff ambient manifold. It contains aa. First countability turns this sequential argument into closedness. Now the map is proper on A¯=A\overline A=A; foundational input 3 makes its image subanalytic.

A converging sequence in the image has preimages in the compact inverse image of the sequence together with its limit. Compactness gives a convergent subsequence with the required limiting image, so the image is closed. Conicity follows from fibre scaling. Finally (C4) and (3) give (fπ*αX)|A=(fd*αY)|A=0(f_\pi^*\alpha_X)|_A=(f_d^*\alpha_Y)|_A=0. Apply (C8) to the surjection from AA onto its now-known subanalytic image. ▫\square

There is also a distinct weaker image assertion. If only fπ|A¯f_\pi|_{\overline A} is proper, input 3 and the same form argument still give a conic subanalytic isotropic image of AA. They do not make that image closed. Neither version assumes global properness of the base map.

Variable-rank linear images and inverse transport

We supply the conic-image calculation used for the other direction. Work locally over a relatively compact base chart, using analytic bundle coordinates. Let L:E→FL:E\to F be an analytic linear bundle map over the identity and H⊂EH\subset E a positive-conic subanalytic set. Let DD be the closed unit disk bundle and set

H0=H∩D,B=L(H0),L(H)=ℝ>0B.(C10) H_0=H\cap D,\qquad B=L(H_0),\qquad L(H)=\mathbb R_{>0}B. \qquad\text{(C10)}

Over every compact base set, DD is compact. Thus LL is proper on H0¯\overline{H_0}, giving subanalytic BB. Also L(D)L(D) is closed and proper over the base: for a convergent image sequence, its base points lie in a compact set and its disk preimages have a convergent subsequence. Compactness over a compact base follows directly from continuity. Therefore B¯⊂L(D)\overline B\subset L(D) is proper over the base.

For any subanalytic B⊂FB\subset F whose closure is proper over the base, its strictly positive saturation is subanalytic. To see this put μ(t,e)=te\mu(t,e)=te, p(t,e)=ep(t,e)=e, and

Q={(t,e):0<t≤1,te∈B},ℝ>0B=μ((0,1]×B)∪p(Q).(C11) Q=\{(t,e):0<t\le1,\ te\in B\},\qquad \mathbb R_{>0}B=\mu((0,1]\times B)\cup p(Q). \qquad\text{(C11)}

The first image covers scales at most one, the second scales at least one. On the closure of the first domain, μ\mu is proper: a compact target set bounds the base, while B¯\overline B over that base and [0,1][0,1] are compact. For the second image, Q¯⊂[0,1]×F\overline Q\subset[0,1]\times F, and its intersection with [0,1]×K[0,1]\times K is compact for every compact K⊂FK\subset F; hence pp is proper on Q¯\overline Q. Input 3 proves both images subanalytic. We image the original domains, so this calculation does not add zero vectors absent from BB. In (C10), every nonzero member of HH can be positively scaled into the unit disk; any zero member is already there. This proves (C10), including kernel outputs, at variable rank.

Inverse-transport theorem. For conic subanalytic isotropic ΛX⊂T*X\Lambda_X\subset T^*X, the set

If(ΛX)=fd(fπ−1(ΛX))(4) I_f(\Lambda_X)=f_d\bigl(f_\pi^{-1}(\Lambda_X)\bigr) \qquad\text{(4)}

is conic, subanalytic and isotropic, without a noncharacteristic or rank assumption. Indeed, B=fπ−1(ΛX)B=f_\pi^{-1}(\Lambda_X) is a conic subanalytic subset of the bundle Cf→YC_f\to Y. The linear-image calculation applies to fdf_d. Equations (C4) and (3) make fd*αYf_d^*\alpha_Y vanish on BB, and (C8) detects vanishing on its image. This is the ordinary transpose-differential image; it makes no claim to equal a limiting characteristic inverse.

A second proof using the cotangent line

For conic subanalytic isotropic Γ⊂T*ℝ\Gamma\subset T^*\mathbb R, consider

i:ℝ→T*ℝ,i(t)=(t;1),S=i−1(Γ).(6) i:\mathbb R\to T^*\mathbb R, \qquad i(t)=(t;1),\qquad S=i^{-1}(\Gamma). \qquad\text{(6)}

The section pulls adta\,dt back to dtdt, so (C4) gives

dt|S=0.(7) dt|_S=0. \qquad\text{(7)}

If distinct tj∈St_j\in S converged to any ambient t0t_0, pass to points on one side and set cj=1/|tj−t0|c_j=1/|t_j-t_0|. Then

cj(tj−t0)=1or−1.(8) c_j(t_j-t_0)=1\quad\text{or}\quad-1. \qquad\text{(8)}

The resulting nonzero cone vector contradicts the form test for dtdt. This works even at a point outside SS and does not assume Γ\Gamma closed. Thus SS is closed and locally finite.

Apply this observation to the function theorem. Its cotangent correspondence is Cφ=X×ℝaC_\varphi=X\times\mathbb R_a, with

φd(x,a)=(x;adφx),φπ(x,a)=(φ(x);a).(10) \varphi_d(x,a)=(x;a\,d\varphi_x),\qquad \varphi_\pi(x,a)=(\varphi(x);a). \qquad\text{(10)}

The incidence A=φd−1(Λ)A=\varphi_d^{-1}(\Lambda) is closed. For compact K⊂T*ℝK\subset T^*\mathbb R, denote its projections to the base and covector coordinates by JJ and BB. The inverse image of KK in AA is a closed subset of

(π(Λ)∩φ−1(J))×B,(11) \bigl(\pi(\Lambda)\cap\varphi^{-1}(J)\bigr)\times B, \qquad\text{(11)}

which is compact by the support-properness assumption. This includes a=0a=0: membership in the incidence still requires a base point in π(Λ)\pi(\Lambda). Proper direct transport therefore gives a closed conic subanalytic isotropic Γ=φπ(A)\Gamma=\varphi_\pi(A), and

Sφ={t:(t;1)∈Γ}=i−1(Γ).(12) S_\varphi=\{t:(t;1)\in\Gamma\}=i^{-1}(\Gamma). \qquad\text{(12)}

The cotangent-line calculation proves the same critical-value conclusion. Unlike the earlier direct proof, this route also uses proper subanalytic images and surjective form detection. Keeping the routes separate makes their actual prerequisite requirements visible.

Exercises with solutions

Escape of source points allows accumulation of selected values

Difficulty: Advanced. Let Λ⊂T*ℝ\Lambda\subset T^*\mathbb R be the zero section together with every full fibre above a positive integer, and set φ(x)=1/(1+x2)\varphi(x)=1/(1+x^2). Determine the selected values and test the theorem’s properness hypothesis.

Solution. The integer fibres are locally finite in the cotangent ambient. Each is closed and analytic, and its canonical form vanishes since its base coordinate is fixed. The zero section also has zero canonical form. The local finite-union rule proves isotropy, while locality proves closedness and subanalyticity. All fibres scale positively. The support is the whole line. On the zero section the test requires φ′(x)=−2x/(1+x2)2=0\varphi'(x)=-2x/(1+x^2)^2=0, hence x=0x=0; each positive integer is selected because its whole fibre is present. Therefore

Sφ={1}∪{1/(1+m2):m≥1}.(14) S_\varphi=\{1\}\cup\{1/(1+m^2):m\ge1\}. \qquad\text{(14)}

Zero is an accumulation value but is not a value of φ\varphi. The selected points escape to infinity; φ−1([0,1])=ℝ\varphi^{-1}([0,1])=\mathbb R is not compact. Thus properness on the support fails. Individual isolation of every existing selected value does not imply closed local finiteness in the ambient line.

Ordinary critical values on a closed analytic submanifold

Difficulty: Intermediate. Let N⊂XN\subset X be a closed analytic submanifold with φ|N\varphi|_N proper. Identify its critical values through the theorem, and compute the case N={(u,v):v=u2}N=\{(u,v):v=u^2\}, φ(u,v)=v\varphi(u,v)=v.

Solution. Take Λ=TN*X\Lambda=T_N^*X. This is closed and conic. In submanifold coordinates it is an analytic bundle; a tangent vector to its total space projects to TxNT_xN, which its covector kills, proving canonical-form isotropy. Its support is exactly NN. The condition dφx∈TN*Xd\varphi_x\in T_N^*X is d(φ|N)x=0d(\varphi|_N)_x=0, so the selected values are precisely the ordinary critical values. Their closed local finiteness follows under the given properness. On the parabola the restriction is u↦u2u\mapsto u^2, a proper function with derivative 2u2u. Its unique critical point is (0,0)(0,0) and its unique critical value is zero; equivalently dv(1,2u)=2udv(1,2u)=2u.

A quadratic function and two source strata

Difficulty: Intermediate. Take φ(x)=x2\varphi(x)=x^2 and Λ\Lambda equal to the zero section of T*ℝT^*\mathbb R together with its full fibre over zero. Compute the transported set and both signed selections.

Solution. The two conormals form a closed conic subanalytic isotropic union. The support is all of ℝ\mathbb R, on which x2x^2 is proper. In (10), membership of (x,2ax)(x,2ax) requires a=0a=0 when x≠0x\ne0, while every aa is admitted when x=0x=0. Consequently

Γ={(t;0):t≥0}∪T{0}*ℝt.(13) \Gamma=\{(t;0):t\ge0\}\cup T^*_{\{0\}}\mathbb R_t. \qquad\text{(13)}

Both slices a=1a=1 and a=−1a=-1 select only t=0t=0. Directly, ±2xdx\pm2x\,dx lies in the zero section only when x=0x=0, and the full fibre adds that same point. Hence both signed value sets are {0}\{0\}.

Proper incidence for a nonproper base map

Difficulty: Intermediate. For f(u,v)=uf(u,v)=u, compute direct transport of the point conormal T{(0,0)}*ℝ2T^*_{\{(0,0)\}}\mathbb R^2. Compare the properness condition with that for the source zero section.

Solution. In correspondence coordinates, fd(u,v;ξ)=(u,v;ξ,0)f_d(u,v;\xi)=(u,v;\xi,0). Point-conormal membership forces u=v=0u=v=0; the incidence maps isomorphically to the closed target fibre T{0}*ℝT^*_{\{0\}}\mathbb R. This map is proper, although the base projection has noncompact fibres. For the source zero section, incidence only forces ξ=0\xi=0, and the inverse image of the single output (0;0)(0;0) contains the entire line (0,v;0)(0,v;0). The hypothesis fails. The resulting image nevertheless happens to be the target zero section, showing that the sufficient properness condition is not necessary for isotropy in each particular example.

A critical differential can collapse an ordinary inverse image

Difficulty: Introductory. For f(y)=y3f(y)=y^3 and ΛX=T{0}*ℝ\Lambda_X=T^*_{\{0\}}\mathbb R, compare (4) with the conormal of the inverse-image point.

Solution. The base equation is y3=0y^3=0, so y=0y=0. Every input covector is allowed, but dfytξ=3y2ξ=0df_y^t\xi=3y^2\xi=0. The ordinary inverse transport is the single zero covector (0;0)(0;0), a zero-dimensional conic analytic isotropic set. The conormal of f−1(0)={0}f^{-1}(0)=\{0\} is the full fibre. The difference reflects the actual zero derivative; no noncharacteristic condition was available to identify these sets, and a limiting inverse construction is a different operation.

Sources and scope

Kashiwara and Schapira, Microlocal Study of Sheaves, Astérisque 128 (1985), develops the isotropic-set setting and canonical-form transport for locally closed subanalytic sets. The transport statements here allow arbitrary subanalytic subsets: the form test (C1)–(C4), uniformization and the proper-closure image theorem supply the required arguments for that broader convention.

The form test, pullback/closure/union rules, local constancy on the selected source set, compactness proof of finite values, surjective detection, conic linear-image calculation and cotangent-line comparison are proved above from the listed prerequisites. The subanalytic foundations and elementary analytic-calculus inputs remain prerequisites. The analytic critical-value theorem used in (C9) has its full argument in the linked section, independent of that lesson’s later conormal results. The constructibility criterion for sheaves additionally requires microsupport and stratification results; it is not a conclusion of this geometric lesson.