Commutative diagrams

Stream: maths

[Chris Hughes]

We've got a bit of a problem at the moment with dealing with commutative diagrams. If I have a theorem about a chain of fields $[M:L:K]$, then assuming that the "canonical map" from $K$ to $M$ is by definition the composition of the maps from $K \to L$ and $L \to M$ would make it hard to apply this theorem to say $\mathbb{C}: \mathbb{R}:\mathbb{Q}$. So we have to assume that there are three maps and include the assumption that they commute. However, supposing we have more than three fields in a row, then there are a lot of commutativity assumptions.

One solution to this that is used in Coq, and has been suggested to me is to assume everything is a subset of some bigger field, or everything is a subgroup of some bigger group. However, this approach has two downsides, one of which is that is makes theorems hard to apply when the objects in question are not defined to be subfields, for example to $\mathbb{Q}$, $\mathbb{R}$ and $\mathbb{C}$. The other downside is that it forces all the maps in the diagram to be injective, which isn't a problem if the objects in my diagram are fields, but is a problem in other categories.

The better solution would be to have an indexing Type iota, which should be a preorder and a functor from this type into my category (a functor, but not necessarily an actual term of type category_theory.functor). This gets rid of the second downside of the subfield approach, and lessens the effect of the first downside, although I would still have to construct an explicit fin 3 → Type which would be a little awkward, but not as bad as tranferring theorems from set.range rat.cast back to ℚ.

Is this a good approach? Are there any downsides of this versus using subgroups/subfields?

[Kevin Buzzard]

In the category theory library there are explicit (very) small categories containing just a couple of objects and arrows; one could use such an object instead of fin 3 and then define the maps using the equation compiler. It's not as if there are hundreds of theorems about fin 3 which we want to access easily. I think this approach sounds nicer than the "everything is a subthing of an artificial big thing" approach. In my thesis I had to deal with commutative diagrams with 8 or more objects in and I wasn't doing anything particularly abstract, I was just working with objects defined over a base.

[Johan Commelin]

I think that @Chris Hughes is pointing at one of the big hurdles for moving commutative algebra forward. Like he says, putting everything as subobject of a big ambient object is problematic as soon as you want to reason about general homomorphisms (for example quotients).
Does anyone know of a comparison article (e.g. by the Coq community) that discusses possible approaches. Any "no-go" results would be valuable to know.
I've been thinking we might want to create some hideous data structure that is not fit for human consumption, but that registers commutativity of bunch of maps (maybe "aka diagram"). It should come with a companion tactic commutes, and this should discharge proof obligations with (by commutes). I have no idea if something like that would work, but I know that we are at a serious impasse right now. Nobody has defined predicates on ring morphisms (flat, finite, finite_type, etale, unramified, finite_presentation, smooth) etc. Nobody has put a B-module structure on B \otimes[A] M. Nobody has defined a construction that turns a ring hom between A-algebras into a ringhom between B-algebras by extension of scalar.
And I think it is mostly because of this issue. Because as soon as you write down a first lemma about these objects, you want all sorts of commutativity constraints. And currently it's really awkward to write those down, or provide proof that they are satisfied.

[Johan Commelin]

If we develop such a hideous data structure, it can use some iota under the hood. But whether this is fin 3 or not, should be completely transparent to the user.

[Kevin Buzzard]

These predicates are very natural things to want. Our MSc commutative algebra course deals with about half of them and the moment you go into modern algebraic geometry you need all of them. Flatness is a great place to start. There is an API of standard results about flat modules which is very well-known to mathematicians and it works be very interesting to try to get it into lean and see where the problems are

[Rob Lewis]

Does anyone know of a comparison article (e.g. by the Coq community) that discusses possible approaches. Any "no-go" results would be valuable to know.

I don't know of a particular algorithm, but it's absolutely worth talking to e.g. some of the math-comp people about this. (Sounds like maybe Chris has already?) It's not a new question and they've definitely gone through the possibilities.

[Johan Commelin]

@Chris Hughes Did you talk with some of the math-comp people? Or do you know some paper that discusses this?

[Chris Hughes]

I asked Cyril Cohen about this and he recommended the substructure approach, although I didn't mention this approach to him. I think most of Galois theory in Coq is about subextensions of the algebraic closure. The odd order theorem paper discusses this a bit, and they prove everything on subsets of some large "ambient" group.

[Kevin Buzzard]

My impression was that we preferred the "partially bundled" approach to the full category theory style bundled approach because with the partially bundled approach, morphisms were still functions. However in Galois theory all the morphisms are going to be K-algebra maps or K-module maps, for K the smallest field in the story, so this benefit is lost anyway. I've been doing a bunch of basic algebraic geometry in Lean as part of my course this term and for varieties over $k$, everything is a $k$-algebra map. Would a fully bundled approach make things better or worse, or just not change anything? Work directly in the category of fields (or even rings)?

[Chris Hughes]

I don't understand this. Do you mean bundled object or morphisms? Why are K-algebra maps not functions?

[Kevin Buzzard]

I'm saying that bundling the morphisms is what is going to happen in practice, so one is losing "the power of the function" anyway, so why not bundle the objects as well?

[Kevin Buzzard]

I thought that one issue with bundling objects is that it forces you to bundle morphisms