Maxwell Thum (Formalizing Discrete Differential Geometry?)

Stream: new members

[Maxwell Thum]

Hi everyone,
My name is Maxwell and I'm in my senior year of undergrad for math. I'm thinking of formalizing some discrete differential geometry (https://www.cs.cmu.edu/~kmcrane/Projects/DDG/) in Lean as part of my senior thesis. For instance, I'm imagining defining things like combinatorial surfaces, abstract simplicial complexes (it looks like @Floris Cnossen has already formalized simplicial sets), and discrete differential forms.

As far as I can tell, nobody has done any DDG in Matlib or Lean. I have not learned any Lean yet, so I'm not sure exactly what I would be getting into. Does this sound at all feasible? Would this contribution be welcome?

[Yaël Dillies]

Do you consider Sperner's lemma to fit in DDG? If so, we gave it a try :sweat_smile:

[Kevin Buzzard]

I have no idea what discrete differential geometry is; I always think of combinatorial surfaces and simplicial complexes as algebraic topology and I don't know what a discrete differential form is but maybe I can guess. All of this sounds very doable in lean though.

[Eric Wieser]

I've been keeping an eye on Crane's work there for a while; it's cool to see a desire to formalize it!

[Tomas Skrivan]

I'm developing Lean 4 library for numerical methods and I would be very much interested in getting some parts of DDG in there. My focus is more on computation then on proofs, I'm thinking about attempting to solve all the course homeworks in Lean. What is our main interest?

The main job would be to get a simplicial set/complex and the corresponding chain complex with boundary operator. Discrete differential forms and differential are just the dual notions, so they should fall out immediately by considering the cochain complex i.e. transposing all the boundary maps.

Do you want to formalize the notion of the dual mesh? And use it to define Hodge dual? Maybe a nice goal would be to prove the cotan formula for Laplacian.

[Maxwell Thum]

Yaël Dillies said:

Do you consider Sperner's lemma to fit in DDG? If so, we gave it a try :sweat_smile:

Maybe, but it doesn't seem like something I would do in this project. (I'm also fairly new to DDG, so I think I'll also be learning the subject by formalizing it; pardon my ignorance)

[Maxwell Thum]

Tomas Skrivan said:

I'm developing Lean 4 library for numerical methods and I would be very much interested in getting some parts of DDG in there. My focus is more on computation then on proofs, I'm thinking about attempting to solve all the course homeworks in Lean. What is our main interest?

The main job would be to get a simplicial set/complex and the corresponding chain complex with boundary operator. Discrete differential forms and differential are just the dual notions, so they should fall out immediately by considering the cochain complex i.e. transposing all the boundary maps.

Do you want to formalize the notion of the dual mesh? And use it to define Hodge dual? Maybe a nice goal would be to prove the cotan formula for Laplacian.

Sure, that all sounds great! What would be a good place for us to talk about this more extensively?

[Tomas Skrivan]

I think a good start would be for you to decide what are you really interested in.

Do you want to properly prove stuff and make a contribution to mathlib? Or are you ok doing more computational stuff that might not be fully formalized and probably make a contribution to my library?

Whare to start? I think the main question is on top of what to build the (co)chain complex. Use simplicial complex, simplicial set or some combinatorial surface?

[Tomas Skrivan]

My library has an experimental structure PrismaticSet that might be of an interest. It is generalization of simplicial set that is not limited to simplices but in 2d it has triangles and squares, in 3d it has tets, cubes, prisms and pyramids and so on.

[Tomas Skrivan]

But I think that is unnecessarily complicated. As you have mentioned that you are fairly new to Lean and DDG, I think the best thing would be to write down some simple structure representing closed(no boundary) triangular surfaces and work with that.

[Maxwell Thum]

I think I'm more interested in properly proving stuff and formalizing the theory than computational stuff. I was also imagining trying to solve every written exercise in the textbook in Lean, if not doing the coding exercises as well.

[Tomas Skrivan]

I would check what is already in mathlib. I'm not very familiar with it so input from someone more familiar with it, in particular algebraic topology, what would be nice.

What you need is the corresponding chain complex for a given simplicial complex or semi-simplicial set, and it should be a complex of real vector spaces.

To define discrete differential forms you just take the dual complex and you get "Stokes theorem" immediately from the definition of coboundary.

To get Laplacian, you need to define the dual cochain complex and the map(Hodge star) between the original(called primal) cochain complex and the dual cochain complex. There are few things necessary:

1. Usually you do this only for closed triangular surfaces, such a subset of simplicial complexes needs to be defined.
2. You need distance information on your original simplicial complex, either vertex embeddings or edge lengths.
3. If I remember correctly, the Hodge star is just a diagonal matrix with ratios of primal and dual cells sizes. For example you will need to know all the neighbouring triangles of a vertex.

[Tomas Skrivan]

One neat thing would be to show that the discrete differential/coboundary is not doing any approximation.

First establish the connection 'differential form -> discrete differential form'.

Take a manifold and draw triangulation on it(probably quite hard to formalize). Discrete differential form is just a cochain i.e. map from a chain to a number. So for a differential form w the corresponding discrete differential form is the map taking a chain and integrating w over it.
The fact that the two paths:

1. differential form -> apply differential -> map to discrete differential form
2. differential form -> map to discrete differential form -> apply discrete differential

give the same answer falls "almost" immediately out of the definition. You need to use normal Stokes theorem, that is why "almost".

[Tomas Skrivan]

The discrete Hodge star is just an approximation to the smooth counter part and honestly I have very little idea how to make the connection precise. Maybe through finite element method, Whitney forms, ... definitely beyond an undergrad project.

[Maxwell Thum]

Okay, thank you very much!

[Maxwell Thum]

This isn't discrete differential geometry, but I think I might try and prove the polyhedron formula and that there are five platonic solids. Does anyone have any advice on this?

[Kevin Buzzard]

Take a look at how it was done in one of the HOL systems (I forget which one but there are links on Freek's page)

[Alex J. Best]

I know @Johan Commelin added https://leanprover-community.github.io/mathlib_docs/number_theory/ADE_inequality.html at some point, not sure what he had in mind but this is a key part of the "topological proof" of the platonic solid classification on wikipedia (https://en.wikipedia.org/wiki/Platonic_solid#Topological_proof), which I guess is the one you would do with the polyhedron formula!

[Maxwell Thum]

Ooh, thanks! I know he's a big part of this project anyway, but I noticed that @Johan Commelin authored 3 of the 7 posts I found when searching "streams:public platonic solids", so I suppose it's possible he had this in mind.

[Yaël Dillies]

This looks very hard, if you ask me. We're quite far from proving Euler's formula.

[Yaël Dillies]

Euler's formula in full generality pertains to algebraic topology. For polyhedra, there are simplifications (because your paths are nicely behaved), but that's still far from what I would deem "a nice first project".

[Yaël Dillies]

In fact I am interested in Euler's formula myself because it is a big part of the Cambridge Graph Theory course, which I'm formalising over at http://github.com/YaelDillies/LeanCamCombi.

[Maxwell Thum]

Yaël Dillies said:

Euler's formula in full generality pertains to algebraic topology. For polyhedra, there are simplifications (because your paths are nicely behaved), but that's still far from what I would deem "a nice first project".

Okay, thank you for the insight. I think I'm starting to see what you mean.

[Joseph Myers]

I suggested in a previous discussion that Platonic solids might be considered a special case of classifying regular polytopes (not necessarily convex) in any Euclidean dimension, and that it might (in line with usual mathlib principles of generality) be appropriate to set up definitions for abstract polytopes before working on flag-transitive realizations thereof in Euclidean space. It seems Yaël has branch#polytopes for abstract polytopes but I don't know its status. And this may well be one of the cases where there's a choice between doing something for a specific case in the mathlib archive and checking the entry off the 100-theorems list, or doing the larger project to get the general definitions and results into mathlib proper.

[Yaël Dillies]

branch#polytopes has a bunch of material that's ready to be put in mathlib. The status is that docs#grade_order took the longest time to hit mathlib, so when it finally did I had moved onto something else.

[Yaël Dillies]

It's been on my todo list to empty this branch ever since, but I haven't yet come round to it :sweat_smile:

[Maxwell Thum]

Any advice on what to do from here (cleanly)? Anything I could clean up?

def abstr_simpl_complex {A : Type*} (K : set (finset A)) :=
  ∀ σ ∈ K, ∀ τ ⊆ σ, τ ∈ K

example (K : set (finset ℕ)) (hK : K = { ∅, {1}, {2}, {1, 2}, {3}}) : abstr_simpl_complex K :=
begin
  intros σ hσ τ hτ,
  rw hK at hσ,
  rcases hσ with ⟨σ⟩,
  --repeat {cases hσ},
  sorry
end

[Kevin Buzzard]

Lean 3 was not really designed to do examples, it's much better at proving abstract theorems. Move to lean 4? Or grit your teeth...

[Kevin Buzzard]

If you're lucky we have lemmas of the form "A \subset {x} iff A = {x} \or A = \empty` and analogous for sets with two elements.

[Maxwell Thum]

Ok, thanks.

[Maxwell Thum]

Is there something analogous to cases that will break h\sigma into 5 cases at once though? I thought rcases might but I guess I still don't have a great handle on it. I get something weird when I try rcases hσ with ⟨σ, rfl⟩, or repeat {cases h\sigma}.

[Ruben Van de Velde]

If your h\sigma is \sigma \in { ... }, then I'd try simp only [set.mem_insert, set.mem_singleton] at h\sigma, hoping that would turn it into \sigma = ... \or ... \or \sigma = ... and then obtain rfl|rfl|rfl|rfl|rfl := h\sigma

[Maxwell Thum]

simp only [set.mem_insert, set.mem_singleton] at h\sigma didn't work, but simp at h\sigma did! Thanks!

[Floris van Doorn]

Here is how you can do something similar, by letting Lean run a decision procedure.
To make sure that a decision procedure exists, I had to change the statement to use finsets only:

import data.finset.powerset

def abstr_simpl_complex {A : Type*} (K : finset (finset A)) :=
  ∀ σ ∈ K, ∀ τ ⊆ σ, τ ∈ K

example (K : finset (finset ℕ)) (hK : K = { ∅, {1}, {2}, {1, 2}, {3}}) : abstr_simpl_complex K :=
by { rw [hK, abstr_simpl_complex], dec_trivial }

[Reid Barton]

I think after rewriting with hK, it should also be possible to handle this in the decidability framework with set.

[Floris van Doorn]

hmm... maybe you're right. We would need instances like set.decidable_forall_mem_insert and set.decidable.forall_mem_empty

[Floris van Doorn]

It at least works out of the box with finset.

[Maxwell Thum]

Oh, wow, dec_trivial seems powerful.

[Maxwell Thum]

I guess finsets are plenty for my purposes, but I wanted to do things in as full generality as possible since I've heard that's what you're supposed to do in Mathlib.
On the other hand, I'm slightly worried that the set definition isn't general enough since mathlib has docs#sSet and docs#category_theory.simplicial_object.

[Yaël Dillies]

We have docs#geometry.simplicial_complex and @Shing Tak Lam adapted my API to ASC on a branch.

[Maxwell Thum]

Yaël Dillies said:

We have docs#geometry.simplicial_complex and Shing Tak Lam adapted my API to ASC on a branch.

Would this be on github?

[Yaël Dillies]

branch#shing-asc. I don't know whether he has more somewhere else.