Local multiplicities of complex-valued functions on the upper half-plane #
The upper half-plane is an open subset of ℂ, and its complex-manifold structure has the single
chart given by the inclusion, with inverse UpperHalfPlane.ofComplex
(UpperHalfPlane.chartAt_eq_ofComplex_symm). So the local multiplicity of a function
f : ℍ → ℂ at z is the order of vanishing of f ∘ ofComplex - f z at z
(TauCeti.UpperHalfPlane.localMultiplicity_eq_analyticOrderNatAt_comp_ofComplex_sub). This is the
form in which orders of modular forms and modular functions are computed, and the form in which
they enter the ramification theory of the orbit projection.
TauCeti.UpperHalfPlane.localMultiplicity_eq_toNat_analyticOrderAt_comp_ofComplex_of_sub_eq
reads off the local multiplicity from the order of any function agreeing with f - f z, such as
j - 1728.
The chart of the upper half-plane at every point is the inclusion into ℂ, the inverse of
UpperHalfPlane.ofComplex.
On the upper half-plane, the local multiplicity of f : ℍ → ℂ at z is the order of vanishing
of f ∘ ofComplex - f z at z.
On the upper half-plane, if g agrees with f - f z, then the local multiplicity of f at
z is the order of vanishing of g ∘ ofComplex at z.