Conformal maps

Stream: maths

[Yourong Zang]

Hello, I am trying to formalize conformal maps, but I am not sure in what generality this should be done. @Heather Macbeth mentioned here that conformal maps should be formalized in the context of inner product space. Does this mean the definition should be something that preserves the quotient of an inner product of two vectors over the product of their norms? Or does this mean I should be defining and using Riemannian metrics to define a conformal map? It seems to me that the mathlib version of Riemannian metrics would be written as a (2, 0)-tensor field, and then say it determines an inner product on every tangent space. I can't think of a more general definition of Riemannian metrics (well, as an average undergraduate student) except the reduction of structure groups of the frame bundle (which we do not have in mathlib (?)) to O(n) on an n-dimensional smooth manifold.

The goal of formalizing conformal maps is to utilize the special case of conformal maps on the complex plane, and show that holomorphic functions are conformal. I would be very grateful if someone would give me some related information or suggestion that I can study.

[Heather Macbeth]

Hi @Yourong Zang, I'm glad you're interested in developing this area! I'd suggest defining a conformal map between inner product spaces E, F to be a function f : E → F, such that at each x : E, we have has_fderiv_at f f' x for some continuous ℝ-linear map f' which is a multiple of a docs#linear_isometry_equiv.

[Heather Macbeth]

Together with some regularity condition -- I wouldn't bother optimizing that at this stage, maybe C^4 (use docs#times_cont_diff), which I think is the level needed for the elementary proof of the Liouville theorem.

[Heather Macbeth]

Yourong Zang said:

Does this mean the definition should be something that preserves the quotient of an inner product of two vectors over the product of their norms?

You can prove this as a consequence of the definition above.

[Yourong Zang]

Heather Macbeth said:

Yourong Zang said:

Does this mean the definition should be something that preserves the quotient of an inner product of two vectors over the product of their norms?

You can prove this as a consequence of the definition above.

Thank you for the information! I will try to define and prove some basic things according to the definition you give.

[Heather Macbeth]

Yourong Zang said:

Or does this mean I should be defining and using Riemannian metrics to define a conformal map?

You're right that one could eventually generalize this to define a conformal map between Riemannian manifolds, but that ends up giving a different theory. What I had in mind is specifically the groupoid of conformal maps from Euclidean space to itself, because this lets you define (using docs#has_groupoid) the theory of "spaces conformally modelled on Euclidean space", aka "conformally flat" manifolds.

[Heather Macbeth]

I think chapters 3 and 5 of the book Inversion theory and conformal mapping, by David Blair, would be a good reference if you need one! (But also feel free to ask questions here.)

[Yourong Zang]

Heather Macbeth said:

I think chapters 3 and 5 of the book Inversion theory and conformal mapping, by David Blair, would be a good reference if you need one! (But also feel free to ask questions here.)

Thank you! I suppose that to prove Liouville's theorem at the current stage, we will have to require the maps to be $C^4$, as most theories of surfaces (especially curvatures) are still underdeveloped in Lean?

[Heather Macbeth]

It's true that we're nowhere near having Riemannian geometry, curvature, etc, in mathlib, but that's not the obstruction here -- rather what's missing is tools for PDEs.

[Yourong Zang]

Heather Macbeth said:

It's true that we're nowhere near having Riemannian geometry, curvature, etc, in mathlib, but that's not the obstruction here -- rather what's missing is tools for PDEs.

Oh I see. I thought it's a geometry issue. Thank you for the valuable information!