Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02
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.

The coordinate axes form a reduced crossing

Example

In C2 with coordinates (x,y), the zero set

X=Z(xy)={x=0}∪{y=0}

is a reduced plane curve germ at the origin whose two irreducible components are the coordinate axes. Both axes are smooth, they meet only at the crossing 0, and 0 is the only singular point of X near 0. No holomorphic map of a connected disc whose image lies in X can have image germ all of X; in particular no single injective branch parametrisation covers both components, so the one-disc parametrisation results for irreducible germs do not extend to reducible ones. Each branch separately is parametrised by t↦(t,0) and t↦(0,t).

Facts & Assumptions

Given: The equation germ f=xy∈OC2,0 and its zero germ X=(Z(xy),0).

[F1]

A hypersurface germ at p is a nonempty proper set germ X=(Z(g),p) for a nonzero nonunit g; its reduced defining germ is the square-free reduction gred, which satisfies Z(gred)=Z(g) and is determined up to a unit, and the vanishing ideal of a reduced germ h is Ip(Z(h))=(h) (Complex-analytic hypersurface germ and its reduced equation, Square-free reduction of a holomorphic equation, The vanishing ideal of a reduced hypersurface germ is principal).

[F2]

A nonzero nonunit germ is reduced when no irreducible germ divides it twice; a germ is irreducible when it is not a product of two nonunits; an irreducible germ is reduced, since a relation q=r⋅(rh) would exhibit q as a product of two nonunits (Reduced holomorphic germ for a hypersurface, Irreducible and prime elements of an integral domain).

[F3]

Units are exactly the germs not vanishing at the base point, and a product of nonunits lies in the maximal ideal; the maximal ideal m0 consists of the germs with zero value at 0, and a germ with nonzero linear part lies outside m02 (A germ is a unit exactly when its value at 0 is nonzero, so Om,0 is local, The ring of holomorphic germs at 0 and its maximal ideal).

[F4]

If a reduced germ factors as u q1⋯qr with u a unit and the qi pairwise nonassociate irreducibles, then Z(f)=⋃iZ(qi) and the germs Z(qi) are exactly the irreducible components of Z(f): they are pairwise distinct and pairwise incomparable, and every irreducible hypersurface subgerm of Z(f) is one of them (Finite unique irreducible components of a hypersurface germ, Irreducible hypersurface germs and their components).

[F5]

A point q of a reduced hypersurface germ Z(h) is regular exactly when the differential of the local reduced equation does not vanish at q, equivalently exactly when Z(h) is a holomorphic hypersurface graph near q (Regular and singular points of an analytic hypersurface).

[F6]

If U⊆Cm is a nonempty connected open set and h is holomorphic on U with h≡0 on a nonempty open subset of U, then h≡0 on U; for m=1 this applies to a disc (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically). Consequently, if u,v are holomorphic on such a U and uv≡0, then u≡0 or v≡0: if both were nonzero, then Z(u) and Z(v) would be closed subsets of U with empty interior, and the nonempty open set U∖Z(u) would be contained in Z(v), forcing v≡0 by the identity theorem.

Proof technique: direct — identify the two prime factors, use the graph criterion for regularity, and rule out a disc map onto both branches with the identity theorem.

Verification

1.1givenF1F2F3algebra

The germs x and y are irreducible. Neither lies in m02, because both have nonzero linear part; if x=ab with a,b nonunits, then a,b∈m0 by [F3] and hence x=ab∈m02, a contradiction. So x is not a product of two nonunits, and the same argument applies to y. The two germs are not associates: x=uy with u a unit would give x(t,0)=u(t,0)⋅0=0 for every small t, contradicting x(t,0)=t≠0 for t≠0. Hence f=xy is a product of two pairwise nonassociate irreducibles, each occurring once, so f is reduced and its reduced defining germ is f itself, with I0(X)=(f) by [F1].

1.2givenF6

Let Δ⊆C be a connected open set containing the origin and let γ=(u,v):Δ→C2 be holomorphic with γ(Δ)⊆X, that is, u(t)v(t)=0 for every t∈Δ. By [F6] applied to the connected domain Δ, one of the two coordinate functions vanishes identically, so the image of γ is contained in a single axis: either γ(Δ)⊆Z(x) or γ(Δ)⊆Z(y).

2.1step 1.1F4

By [F4] applied to the factorisation f=x⋅y of step 1.1, X=Z(x)∪Z(y), and the two branches Z(x)={x=0} and Z(y)={y=0} are exactly the irreducible components of X; they are distinct as set germs and neither contains the other.

3.1step 2.1F5construct

Every point of Z(x) is regular: Z(x) is the graph {(x,y):x=0} of the zero function over the y-coordinate near each of its points, hence a holomorphic hypersurface graph near every such point, so [F5] gives regularity. The same argument exhibits Z(y)={(x,y):y=0} as the graph of the zero function over the x-coordinate, so every point of Z(y) is regular as well.

4.1step 1.1step 3.1F5algebra

The origin is a singular point: by step 1.1 the reduced defining germ of X is xy, and d(xy)=y dx+x dy vanishes at 0. So 0 is not regular by [F5]. Since Z(x)∩Z(y)={0}, every point of X other than the origin lies on exactly one of the two branches and is regular by step 3.1; hence the origin is the only singular point of X in a neighbourhood of 0, and it is exactly the crossing of the two branches.

5.1step 1.2step 2.1step 4.1∎

Suppose first that γ(Δ)⊆Z(x). The set germ of the image of γ at the origin is then contained in Z(x), which is a proper subgerm of X: for every small ε≠0 the point (ε,0) belongs to X but not to Z(x). Hence the image of γ cannot contain a full representative of X, so its image germ is not X; the case γ(Δ)⊆Z(y) is the same with the roles of x and y exchanged. Therefore no holomorphic map of a connected disc has image germ X, injective or not, and in particular no single injective branch parametrisation covers both components. The individual branches are parametrised by the injective holomorphic maps t↦(t,0) and t↦(0,t), whose images are full representatives of Z(y) and Z(x) respectively.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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