The sheaf of holomorphic functions on ℂ, and its étalé space #
Analytic continuation transports germs. Conformal/Continuation/Basic.lean carries them
concretely — as families of functions compared by =ᶠ[𝓝 _] — and records, without proof, that
reading a germ as a point of the étalé space of holomorphic germs turns a continuation along a
path into a continuous lift of that path. Neither Mathlib nor this repository had the space that
sentence names. This file builds it, and proves the two facts that make it the right object: the
projection to the base is a local homeomorphism, and it is a separated map.
What is built #
The sheaf itself comes from Mathlib's local-predicate machinery
(Mathlib/Topology/Sheaves/LocalPredicate.lean): TauCeti.IsHolomorphicSection says that a
function on an open U ⊆ ℂ is the restriction of a function analytic on a neighbourhood of every
point of U, this is stable under restriction and local, and TauCeti.holomorphicPresheaf /
TauCeti.holomorphicSheaf are the presheaf and the sheaf of such sections, the latter being
Mathlib's TopCat.subsheafToTypes at that local predicate. Locality is where the extension by
zero of a section enters: a function given only on U has no values elsewhere to be analytic at,
so the witness glued from local ones is Function.extend Subtype.val, which agrees with the
section on U and is analytic there because analyticity is a local property of an open set. The
same extension names the function underlying a section,
TauCeti.HolomorphicPresheaf.sectionFun, and every statement below is phrased against it rather
than against the subtype.
The étalé space is Mathlib's TopCat.Presheaf.EtaleSpace — pairs of a base point and a germ over
it — with the chart API of TauCeti/Topology/Sheaves/EtaleSpace.lean. On top of it this file adds
the dictionary between germs as stalk elements and germs as eventual equality of functions:
TauCeti.HolomorphicPresheaf.germ_eq_iff— two sections have the same germ atxexactly when their functions agree nearx;TauCeti.HolomorphicPresheaf.germAt— the stalk element carried by a function analytic at a point, andTauCeti.HolomorphicPresheaf.germPointthe corresponding point of the étalé space;TauCeti.HolomorphicPresheaf.germAt_eq_iff— that dictionary again, now between two functions rather than two sections;TauCeti.HolomorphicPresheaf.repFun— a holomorphic representative of the germ carried by a point of the étalé space, inverse togermPointbyTauCeti.HolomorphicPresheaf.germPoint_repFun.
germAt is total: a function that is not analytic at the point in question is sent to the germ of
0. The junk value is never inspected — every lemma about germAt either supplies analyticity or
is insensitive to it (TauCeti.HolomorphicPresheaf.germAt_congr holds for arbitrary functions,
both sides being junk when the common germ is not analytic) — and totality is what lets the germ
map of a family be written as a plain function of the parameter, with no proof argument to
transport.
The two theorems #
TauCeti.TopCat.Presheaf.EtaleSpace.isLocalHomeomorph_base is the chart statement of
TauCeti/Topology/Sheaves/EtaleSpace.lean: over an open set on which a section is defined, the
germs of that section form an open set carried homeomorphically onto the base.
TauCeti.HolomorphicPresheaf.isSeparatedMap_base is the analytic content, and it is the
identity theorem in disguise. Two distinct germs at one point x are represented by sections
over two open sets; restrict both to one disc about x. The two open sets of germs they sweep out
are disjoint, for a point of both would be a point y of the disc at which the two
representatives have the same germ, and the identity theorem on the disc — connected, and where
both representatives are analytic — would propagate that agreement from y back to x, making
the two germs equal. Separatedness is exactly the hypothesis Mathlib's abstract monodromy theorem
IsLocalHomeomorph.monodromy_theorem asks for, and its docstring names analytic continuation as
the intended application; Conformal/Continuation/Etale.lean supplies the continuation/lift
correspondence needed to apply it.
Main results #
TauCeti.holomorphicSheaf— the sheaf of holomorphic functions onℂ.TauCeti.HolomorphicPresheaf.germ_eq_iff— germs agree exactly when the functions agree nearby.TauCeti.HolomorphicPresheaf.continuousOn_germPoint— the germ map of a holomorphic function is a continuous section of the étalé projection.TauCeti.HolomorphicPresheaf.isSeparatedMap_base— the étalé projection is separated.
Generality #
The target is an arbitrary complex Banach space E, the generality at which
Conformal/Continuation/Basic.lean states analytic continuation; the scalar case E = ℂ is the
one the conformal-mapping consumers instantiate. Both restrictions on E are inherited rather
than chosen. It is confined to Type rather than Type* by Mathlib's étalé space, which is built
for a C-valued presheaf on X : TopCat.{v} with [Category.{v} C]: the base TopCat.of ℂ
lives in TopCat.{0}, so the values of the presheaf are forced into Type. Completeness is asked
for exactly where Mathlib asks for it, from TauCeti.HolomorphicPresheaf.germAt on, because
AnalyticAt.exists_ball_analyticOnNhd — which names a disc on which a germ has a representative —
is stated for a Banach target. The sheaf, the germ dictionary
TauCeti.HolomorphicPresheaf.germ_eq_iff and both theorems about the projection are free of it,
the identity theorem AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq needing no
completeness.
The source is ℂ rather than a Riemann surface, in accordance with the generality bar of
ConformalMapping/README.md, which fixes the scalar domain for the conformal layers L0–L6, and
because the consumer Conformal/Continuation/Basic.lean continues germs along paths in ℂ. A
Riemann surface source would need a holomorphic atlas to even state the predicate, which the
pinned Mathlib has for complex manifolds but which this area does not use anywhere else.
Relation to Mathlib #
Mathlib has the étalé space of a presheaf (Mathlib/Topology/Sheaves/EtaleSpace.lean) and the
local-predicate construction of a sheaf of functions
(Mathlib/Topology/Sheaves/LocalPredicate.lean), both consumed here; it has no sheaf of
holomorphic functions and no étalé space of holomorphic germs. The in-progress human-curated
Riemann-mapping effort mathlib4#33505
contains no continuation or monodromy material, so nothing here is a shim for it. Mathlib's sheaf
of smooth functions on a manifold (Mathlib/Geometry/Manifold/Sheaf/Smooth.lean) reaches the same
LocalPredicate interface through the structure-groupoid machinery, but is fixed at smoothness
∞; running that route at analytic smoothness would put the charted-space structure of ℂ and a
translation between ContMDiff and AnalyticOnNhd between this file and the identity theorem it
needs, so the predicate is written out directly instead.
References #
- L. Ahlfors, Complex Analysis, Ch. 8 §1.
- J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. IX §§1--3.
- O. Forster, Lectures on Riemann Surfaces (GTM 81), §6.
The sheaf #
A function on an open subset U of ℂ is a holomorphic section when it is the
restriction of a function analytic on a neighbourhood of every point of U.
Equations
- TauCeti.IsHolomorphicSection f = ∃ (g : ℂ → E), AnalyticOnNhd ℂ g ↑U ∧ ∀ (x : ↥U), f x = g ↑x
Instances For
Being a holomorphic section is being the restriction of a function analytic on a
neighbourhood of every point. TauCeti.IsHolomorphicSection does not expose its body, so this
is how a consumer of the sheaf introduces or eliminates it.
Being holomorphic is stable under restriction to a smaller open set.
The presheaf of holomorphic functions on ℂ with values in E.
Equations
- TauCeti.holomorphicPresheaf E = TopCat.subpresheafToTypes { pred := fun {x : TopologicalSpace.Opens ↑(TopCat.of ℂ)} (f : ↥x → E) => TauCeti.IsHolomorphicSection f, res := ⋯ }
Instances For
The sheaf of holomorphic functions on ℂ with values in E.
Equations
Instances For
The presheaf underlying the sheaf of holomorphic functions.
Sections as functions #
The function on ℂ underlying a section of TauCeti.holomorphicPresheaf, extended by zero
outside its domain.
Equations
- TauCeti.HolomorphicPresheaf.sectionFun s = Function.extend Subtype.val ↑s fun (x : ℂ) => 0
Instances For
On its own domain, the function underlying a section is the section.
The function underlying a holomorphic section is analytic on a neighbourhood of every point of its domain.
A function analytic on a neighbourhood of every point of U, read as a section over U.
Equations
- TauCeti.HolomorphicPresheaf.toSection U g hg = ⟨fun (y : ↥(Opposite.unop (Opposite.op U))) => g ↑y, ⋯⟩
Instances For
On U, the function underlying the section determined by g is g.
Germs #
Two holomorphic sections have the same germ at a point exactly when their functions agree near it. The forward direction is the definition of the stalk as a filtered colimit; the reverse one restricts both sections to a common open set on which they are equal.
The germ at z of a function analytic there, as an element of the stalk of the sheaf of
holomorphic functions. A function that is not analytic at z is sent to the germ of 0, a junk
value that TauCeti.HolomorphicPresheaf.germAt_eq_germ_of_eventuallyEq never sees.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The germ of a function is the germ of any section representing it. This is the only way
TauCeti.HolomorphicPresheaf.germAt is used: it identifies the abstract germ with the concrete
one carried by a section, and the choice of ball made in the definition drops out.
The germ of the function underlying a section is the germ of that section.
The germ at z depends only on the values near z. Functions agreeing near z have the
same germ there, analytic or not: when they are not analytic both sides are the same junk value.
Two functions analytic at z have the same germ there exactly when they agree near z.
The reverse implication is TauCeti.HolomorphicPresheaf.germAt_congr; the forward one is the
description of the stalk as a colimit, read through
TauCeti.HolomorphicPresheaf.germ_eq_iff.
The germ of a function analytic at z, as a point of the étalé space of holomorphic germs.
Equations
- TauCeti.HolomorphicPresheaf.germPoint g z = { base := z, germ := TauCeti.HolomorphicPresheaf.germAt g z }
Instances For
The germ point of g at z sits over z.
The germ point of g at z carries the germ of g.
Functions agreeing near z give the same point of the étalé space over z.
Over an open set on which g is analytic, the germ map of g is the germ section swept out
by g. This is the comparison between the two descriptions of a point of the étalé space — a
base point paired with TauCeti.HolomorphicPresheaf.germAt, and the germ of a section at a point
of its domain — and it is what carries continuity from one to the other.
The germ map of a holomorphic function is a continuous section of the étalé projection.
Over its domain it is exactly the section of the étalé space swept out by g
(TauCeti.HolomorphicPresheaf.germPoint_eq_germSection), so continuity is
TauCeti.TopCat.Presheaf.EtaleSpace.continuous_germSection.
Representatives of a point of the étalé space #
Every point of the étalé space carries the germ of a function analytic at its base point.
A holomorphic representative of the germ carried by a point of the étalé space.
Equations
Instances For
A representative of a point of the étalé space is analytic at its base point.
A representative of a point of the étalé space carries the germ that point carries.
Taking a representative and then its germ point recovers the point of the étalé space.
The projection is a separated local homeomorphism #
The étalé projection of the sheaf of holomorphic functions is a separated map: two
distinct germs at the same point of ℂ have disjoint neighbourhoods in the étalé space.
This is the identity theorem for holomorphic functions, read in the étalé space. Two sections representing the two germs are restricted to one disc about the common base point; the two open sets swept out by their germs over that disc are disjoint, because a point of both would be a point where the two representatives have the same germ, and the identity theorem on the disc — which is connected — would then propagate that agreement back to the base point.