## Stream: maths

### Topic: algebra is not scaling for me

#### Kevin Buzzard (Feb 17 2020 at 20:09):

artintate2.png

There's a proof from Atiyah--Macdonald. There are three rings $A\subseteq B\subseteq C$ and during the proof a fourth ring $B_0$ between $A$ and $C$ is introduced. All the fast and loose playing with elements of $B$ makes me want to write this entire proof using subsets of $C$ (i.e. $C$ is a big ring and everything else is a subset). However the following concepts are also used: $C$ is finitely-generated as an $A$-algebra, $C$ is finitely-generated as a $B$-module, $C$ is finitely-generated as a $B_0$-module, $B_0$ is a Noetherian ring, $B$ is finitely-generated as a $B_0$-module, $B_0$ is finitely-generated as an $A$-algebra, and $B$ is finitely-generated as an $A$-algebra, and this makes me want to write the proof using four different rings and lots of [algebra X Y] instances. Whichever option I choose will then cause me pain in the parts of the argument which work far more nicely with the other option. What am I supposed to be doing here?

#### Johan Commelin (Feb 17 2020 at 20:45):

This seems like a really nice test case.

#### Johan Commelin (Feb 17 2020 at 20:45):

I completely agree that things like this are an enormous pain in the back at the moment. And we have to find a way to make it go smoother.

#### Patrick Massot (Feb 17 2020 at 20:56):

We can ask @Assia Mahboubi and @Cyril Cohen how that would be handled in math-comp.

#### Kevin Buzzard (Feb 17 2020 at 21:43):

I wonder whether this is the sort of situation (when doing finite groups, say) which makes people want to work in some big underlying group like they do in Feit-Thompson?

Having thought about this more on the way home though, without touching Lean, I am beginning to think that actually the approach with everything a different type might work fine, after some sort of interface is written. Maybe I'm being naive. I guess one thing that will come up is that $B_0$ is defined later on, and probably at this stage $C$ is an $A$-algebra, but I'm going to need to make $B_0$ an $A$-algebra and $C$ a $B_0$-algebra and hope that everything works out with $C$ now being an $A$-algebra in two ways (actually maybe it isn't even an algebra in two ways, as that instance is not there I guess).

#### Assia Mahboubi (Mar 21 2020 at 13:46):

Hi, sorry for this answer one month later, and many thanks @Patrick Massot for inviting me in this discussion. I will try to write a mockup, mathcomp style, draft one of these days. (NB: this might well be outrageous wishful thinking, as the complete lockdown in France has considerably deteriorated my working conditions.) I would say that such a mockup would rely on two ingredients:

• Having $A$, $B$ and $C$ as (carrier) sets of a same type
• Attaching different algebraic structures to a same carrier set via the definition of different, convertible copies of the same carrier.

But I have been told at several occasion that this is considered as too brittle in mathlib (or in Lean?). I would love to understand better why so.

#### Johan Commelin (Mar 21 2020 at 13:52):

@Assia Mahboubi Cool! (And good luck with the tough situation.)
In this example, the maps A → B → C are injective, so we can regard them as subrings of some ambient ring. But in other situations the maps need not be injective. And then you can use sets in an ambient type...

#### Johan Commelin (Mar 21 2020 at 13:53):

This is my main reason why I think the "subsets of ambient type" cannot work for the general commutative algebra problem

#### Mario Carneiro (Mar 21 2020 at 13:53):

We use this trick in a few places in mathlib, notably in additive and multiplicative. In other places, like opposite, we have moved from the "defeq newtype" approach to a more locked down "irreducible defeq newtype" which still gives you up and down functions satisfying up (down x) = x and down (up x) = x definitionally. But it seems in lean 4 that these have been abolished in favor of singleton structures, which loses one of those two defeqs for the coercions.

#### Mario Carneiro (Mar 21 2020 at 13:56):

One issue you can run into if you use types like multiplicative nat is that it becomes easy to get confused since the notations are all wrong: 0 is actually 1 and if you aren't careful your goal might end up saying 1 * 1 = 2 where the 1 is carrying the instance from nat and * is carrying the instance from multiplicative nat.

#### Assia Mahboubi (Mar 21 2020 at 14:22):

@Mario Carneiro @Johan Commelin many thanks for your answers! This is really helpful. Note that I am not advocating this as an all-purpose solution, just trying to think about Kevin's problem, which is stated on paper using set inclusions. I am just suggesting to formalize these inclusions as, well, inclusions. Also, I am used to a different, more bundled approach to notations, and in any case I agree that the notation problem mentioned by Mario is of a different nature.

#### Kevin Buzzard (Mar 21 2020 at 14:24):

The statement and proof of the lemma work fine if A -> B -> C are maps of rings. I was surprised! One proof is "replacing A and B by their images in C, we can assume $A\subseteq B\subseteq C$..."

#### Kevin Buzzard (Mar 21 2020 at 14:25):

The intermediate construction B_0 really does seem to be a subset of B though.

#### Assia Mahboubi (Mar 21 2020 at 14:28):

@Kevin Buzzard ah ok! Then it is the same as what I was suggesting. Working with subsets when possible does not mean that one does not generalize statement afterwards. Thanks for this additional comment.

#### Kevin Buzzard (Mar 21 2020 at 14:29):

My problem was that I didn't know if I wanted [B : subring C] or [algebra B C]. In mathematics they're kind of the same

#### Assia Mahboubi (Mar 21 2020 at 14:30):

Does it make a different when you need to apply this lemma? I mean, in Lean of course.

#### Kevin Buzzard (Mar 21 2020 at 14:31):

But with this B_0 it really was built as a subring of B. So I just want to painlessly switch between the two concepts really. Maybe it just means writing a bunch of interface to enable me to do this. And then I will need things like "B is integral over A" which will have two definitions depending on whether B is an A-algebra or A is a subring of B, and we need that one is true if and only if the other is etc.

#### Kevin Buzzard (Mar 21 2020 at 14:31):

Yes I'm sure that applying it will be hopeless with the subring definition

#### Kevin Buzzard (Mar 21 2020 at 14:33):

so then everything has to be an algebra over everything else. But in the proof I really make B_0 a subring of B, and the map from A to B lands in B_0, so now I have to decide whether I want to make a new type B_0 with B_0 an A-algebra and B a B_0-algebra or whether to have some hybrid approach with some subrings and some algebras

#### Assia Mahboubi (Mar 21 2020 at 14:38):

@Kevin Buzzard I am lost : I though that in the proof $A$, $B$ and $C$ are subsets, so what it is the problem with the "map" from $A$ to $B$?

#### Kevin Buzzard (Mar 21 2020 at 14:39):

So I do not really know what I am supposed to be proving here. If I prove the subset version, then I can deduce the version with A -> B -> C. This is what I'd say to a mathematician.

#### Kevin Buzzard (Mar 21 2020 at 14:39):

But the subset version is probably not so easy to apply in practice because $\mathbb{N}$ is not a subset of $\mathbb{Z}$ even though mathematicians think it is.

#### Assia Mahboubi (Mar 21 2020 at 14:39):

Exactly, and that's the route I would go for in type theory as well.

#### Kevin Buzzard (Mar 21 2020 at 14:40):

The problem is that if I have a morphism of rings $A\to B$ then there are various common predicates, such as "the morphism is integral"

#### Kevin Buzzard (Mar 21 2020 at 14:40):

and if I have a subset $A\subseteq B$ then we get the same predicates

#### Kevin Buzzard (Mar 21 2020 at 14:40):

because there's an induced morphism

#### Kevin Buzzard (Mar 21 2020 at 14:41):

and some of these predicates are defined for subrings and some are defined for morphisms

#### Kevin Buzzard (Mar 21 2020 at 14:41):

and some are perhaps defined for both, and then you need some theorem saying that one is true iff the other is true

#### Kevin Buzzard (Mar 21 2020 at 14:42):

but actually the problem is much worse

#### Kevin Buzzard (Mar 21 2020 at 14:42):

because if A and B are both subsets of C in the sense that they are terms of type set C

#### Kevin Buzzard (Mar 21 2020 at 14:42):

then A is not a subset of B, at least in Lean

#### Kevin Buzzard (Mar 21 2020 at 14:42):

in the sense that A doesn't have type set B

#### Kevin Buzzard (Mar 21 2020 at 14:43):

so now I need another predicate: if A and B are both subsets of C then one can ask that the inclusion A -> B is integral as well

#### Kevin Buzzard (Mar 21 2020 at 14:43):

so this is now three ways of saying exactly the same thing

#### Mario Carneiro (Mar 21 2020 at 14:43):

aren't they all the same though?

sure

#### Kevin Buzzard (Mar 21 2020 at 14:44):

and of course I could hack through some proof

#### Mario Carneiro (Mar 21 2020 at 14:44):

like in lean that would just be one predicate and various kinds of coercion arrows

#### Assia Mahboubi (Mar 21 2020 at 14:44):

@Kevin Buzzard , in the first version of the lemma, the one about inclusions, then $A$, $B$ and $C$ are all sets of a same, larger type. Which does not even need to be equiped with a ring structure.

#### Kevin Buzzard (Mar 21 2020 at 14:45):

Right -- so in the odd order paper this is the way of thinking.

#### Kevin Buzzard (Mar 21 2020 at 14:45):

Make everything a subset of a large object, and then put the predicates on inclusions of subsets

#### Kevin Buzzard (Mar 21 2020 at 14:45):

But Mario is saying the exact opposite, he's saying put the predicate on A a ring and B an A-algebra

#### Assia Mahboubi (Mar 21 2020 at 14:47):

Kevin Buzzard said:

Make everything a subset of a large object, and then put the predicates on inclusions of subsets

And afterwards, when needed and possible, prove alternate versions for items with a different carrier type, images under an appropriate morphism.

#### Kevin Buzzard (Mar 21 2020 at 14:48):

so you're saying that I should define the concepts for A and B both subrings of some large X, and then if I happen to have a map of rings R -> S then the image of R is a subset of the universal subset of S

Yes

#### Johan Commelin (Mar 21 2020 at 14:49):

I think she wants A B and C subrings of large R.

#### Kevin Buzzard (Mar 21 2020 at 14:49):

but now if I have R -> S and S -> T and I get an induced map R -> T then aren't I in big trouble?

#### Kevin Buzzard (Mar 21 2020 at 14:50):

because my integrality predicate on R -> S is about an inclusion (image of R) -> (universal subset of S) in S

#### Kevin Buzzard (Mar 21 2020 at 14:50):

but I now want to talk about the image of R and the image of S in T which is a different thing

#### Assia Mahboubi (Mar 21 2020 at 14:51):

@Johan Commelin, in general the supertype does not need to have a very strong structure. The carrier type of finite groups in the odd order theorem formal development is not necessarily a group itself.

#### Kevin Buzzard (Mar 21 2020 at 14:52):

Isn't the issue here that if I define the predicate for two subsets A and B of a large ring X, with $A\subseteq B$, if I define integrality for this, then if I have rings $A'$ and $B'$ subsets of a large ring $Y$, with $A'$ isomorphic to $A$ and $B'$ isomorphic to $B$ and the diagram commuting, I can't deduce integrality of $A'\to B'$ from integrality of $A\to B$

#### Patrick Massot (Mar 21 2020 at 14:52):

Assia, are those lemmas stated in terms of an amorphous ambient type meant to be part of the public API, or are they hidden? (And thanks for joining us!)

#### Assia Mahboubi (Mar 21 2020 at 14:52):

@Kevin Buzzard sorry you lost me. We are no more talking about the same lemma, are we?

#### Kevin Buzzard (Mar 21 2020 at 14:53):

I am trying to work out how to define 100 predicates on a situation where I have an injective map $A\to B$ of rings.

#### Assia Mahboubi (Mar 21 2020 at 14:53):

Hi @Patrick Massot ! My pleasure, again, thank you!

#### Kevin Buzzard (Mar 21 2020 at 14:54):

I can model this situation in three ways. (1) I can define a structure algebra A B to mean that A and B are rings and we have a map A -> B (2) I can consider A as a subset of B or (3) I can consider both A and B as subsets of a larger structure.

#### Assia Mahboubi (Mar 21 2020 at 14:54):

It is not completly amorphous: it is equipped with a signature, which fixes the laws common to all sub-stuff under consideration (here, ring operations I guess).

#### Kevin Buzzard (Mar 21 2020 at 14:55):

I want to define 100 predicates and prove 100 lemmas about these predicates

#### Kevin Buzzard (Mar 21 2020 at 14:55):

and the lemmas are of the form "if A -> B has property P, and B -> C has property Q, then A -> C has property R"

#### Kevin Buzzard (Mar 21 2020 at 14:55):

or "if A -> B and B -> C are ring homomorphisms and if A -> B has property P and A -> C has property Q then B -> C has property R"

#### Kevin Buzzard (Mar 21 2020 at 14:56):

and all of these predicates make sense for general ring homomorphisms A -> B, but they only depend on the image of A in B

#### Kevin Buzzard (Mar 21 2020 at 14:57):

so we can imagine that they are predicates on a ring B and a subring A

#### Chris Hughes (Mar 21 2020 at 14:58):

The idea of making everything a subset of a big Type, is basically just the assumption that everything lives inside some big commutative diagram where the maps are injective. What do you lose by just assuming something like this, where there are no injectivity assumptions?

{ι : Type} [complete_lattice ι] (R : ι → Type*) [∀ i, comm_ring (R i)] (f : Π i j, i ≤ j → R i → R j)


#### Chris Hughes (Mar 21 2020 at 14:58):

I forgot the commutativity assumption but you get the idea.

#### Assia Mahboubi (Mar 21 2020 at 14:58):

But yes, it is part of the public API. The formal statement of the odd order theorem proved by our proof is

Theorem Feit_Thompson (gT : finGroupType) (G : {group gT}) : odd #|G| -> solvable G.


where finGroupType is the ambiant type, equipped with a distinguished element, a binary law, etc. and G is a subset thereof, equipped with a true structure of group. So yes, one quantifier more than expected on paper.

#### Kevin Buzzard (Mar 21 2020 at 14:58):

But what happens in practice is that when you are working with rings, sometimes you have two rings and a map between them, sometimes you have a ring and a subring, and sometimes you have two subrings of a ring, so I need all my theorems in all three situations and I also need them in "mixed" situations where A is a subring of B and there's a map from B to C

#### Assia Mahboubi (Mar 21 2020 at 15:00):

@Kevin Buzzard sorry I am not fast enough to answer all the messages. I am trying in order.

#### Assia Mahboubi (Mar 21 2020 at 15:01):

First I would like to make a disclaimer: I am still not quite sure about how to do commutative algebra right.

#### Kevin Buzzard (Mar 21 2020 at 15:03):

Yes, as a mathematician I was very surprised when I started to learn about this area that these issues, which simply do not exist in mathematics, are very subtle and perhaps not completely understood in this community.

#### Kevin Buzzard (Mar 21 2020 at 15:04):

Can you apply the odd order theorem? If I create just an abstract group by putting a group structure on some type with precisely one term, can you prove that it is solvable using Feit-Thompson?

#### Kevin Buzzard (Mar 21 2020 at 15:05):

some people might say that this is using a sledgehammer to crack a nut I guess

#### Assia Mahboubi (Mar 21 2020 at 15:05):

Things are currently broken in mathcomp (which you can guess from this line in the definition of a ring structure in the hierarchy).

#### Assia Mahboubi (Mar 21 2020 at 15:06):

Kevin Buzzard said:

Can you apply the odd order theorem? If I create just an abstract group by putting a group structure on some type with precisely one term, can you prove that it is solvable using Feit-Thompson?

Of course you can.

#### Patrick Massot (Mar 21 2020 at 15:06):

Why not stating the expected version of Feit-Thompson after your weird statement?

#### Kevin Buzzard (Mar 21 2020 at 15:06):

but my type is nothing to do with finGroupType?

#### Patrick Massot (Mar 21 2020 at 15:07):

At least it would make it easier to read for mathematicians.

#### Assia Mahboubi (Mar 21 2020 at 15:08):

@Kevin Buzzard you will define the instance of group carrier type from your singleton type, and then the group you want to work with is the trivial group on this group type (yes, the library has defined this for you).

#### Assia Mahboubi (Mar 21 2020 at 15:08):

@Patrick Massot What is the expected version?

#### Kevin Buzzard (Mar 21 2020 at 15:08):

The expected version doesn't have the carrier type

#### Patrick Massot (Mar 21 2020 at 15:08):

Only one type, equipped with a group structure.

#### Assia Mahboubi (Mar 21 2020 at 15:08):

Because it is stated in set theory.

#### Assia Mahboubi (Mar 21 2020 at 15:10):

Patrick Massot said:

Only one type, equipped with a group structure.

I am not sure. My feeling is that mathematicians do not speak about types, just about sets.

#### Patrick Massot (Mar 21 2020 at 15:10):

I mean Theorem Feit_Thompson (G : Group) : odd #|G| -> solvable G. (assuming bundled groups).

#### Patrick Massot (Mar 21 2020 at 15:10):

or Theorem Feit_Thompson (G : Type*) [group G] [finite G] : odd #|G| -> solvable G. if unbundled.

#### Kevin Buzzard (Mar 21 2020 at 15:11):

That was the question I was trying to ask with my group of order 1 question.

#### Kevin Buzzard (Mar 21 2020 at 15:12):

I am trying to prove theorems about rings in this thread, and I am just beginning to understand that the statement of Feit-Thompson above is not in some sense a statement about the most general concept of a group

#### Assia Mahboubi (Mar 21 2020 at 15:12):

@Kevin Buzzard In fact, you would apply the statement to the singleton set. And then inference of implicit stuff does the rest.

#### Assia Mahboubi (Mar 21 2020 at 15:13):

Kevin Buzzard said:

I am trying to prove theorems about rings in this thread, and I am just beginning to understand that the statement of Feit-Thompson above is not in some sense a statement about the most general concept of a group

Why not?

#### Assia Mahboubi (Mar 21 2020 at 15:13):

oops, I have to go offline, sorry.

#### Kevin Buzzard (Mar 21 2020 at 15:13):

thank you very much!

#### Patrick Massot (Mar 21 2020 at 15:13):

Maybe you shouldn't care, but if you tell a mathematician "I've formalized Feit-Thompson, the statement is Theorem Feit_Thompson (G : Group) : odd #|G| -> solvable G" they agree this is the expected statement, even without having ever heard of type theory, whereas Theorem Feit_Thompson (gT : finGroupType) (G : {group gT}) : odd #|G| -> solvable G. looks alien.

#### Kevin Buzzard (Mar 21 2020 at 15:14):

So solvable here is a predicate on subsets of some ambient type. We can prove what Patrick and I would think of as the "normal" version by defining solvable G to be solvable (set.univ G)

#### Kevin Buzzard (Mar 21 2020 at 15:21):

I am only guessing at what is happening with Assia's link above, but here is some observation. If we have finitely many groups and for some technical type theory reason we want them all to be subgroups of a big object with a 1 and a * and an inv, we can just take the product of the groups and then each group naturally embeds as a subset.

#### Mario Carneiro (Mar 21 2020 at 15:22):

it doesn't even have to be a finite set of groups

#### Kevin Buzzard (Mar 21 2020 at 15:22):

But this same trick cannot work with rings. If you have finitely many rings then each has a 0 and a 1 and a +, and if you want them all to be subsets of a big object with a universal 0 and 1 and +, then you're in trouble, because maybe 1 + 1 = 0 in some of the rings, but not in others, and if they all have the same 0 and the same 1 and the same + then they all have the same 2

#### Kevin Buzzard (Mar 21 2020 at 15:23):

and the zero ring has 0=1

#### Mario Carneiro (Mar 21 2020 at 15:23):

although possibly the big not-a-group in F-T is actually finite; I'm not sure whether it gets enforced there or on the groups themselves

#### Chris Hughes (Mar 21 2020 at 15:24):

Kevin Buzzard said:

I am only guessing at what is happening with Assia's link above, but here is some observation. If we have finitely many groups and for some technical type theory reason we want them all to be subgroups of a big object with a 1 and a * and an inv, we can just take the product of the groups and then each group naturally embeds as a subset.

I don't think that really works particularly well, because they also have to embed in a way such that all the maps you care about between these groups become inclusions

#### Mario Carneiro (Mar 21 2020 at 15:24):

But Kevin, the big object is not a group/ring/whatever structure

#### Kevin Buzzard (Mar 21 2020 at 15:24):

This doesn't matter

#### Mario Carneiro (Mar 21 2020 at 15:24):

and the inclusions are not ring homs

Oh this matters

#### Kevin Buzzard (Mar 21 2020 at 15:25):

My understanding was that they were all inheriting the structure from the big type

#### Mario Carneiro (Mar 21 2020 at 15:25):

oh wait, they are not ring homs but they are +,*,0,1 homs

#### Kevin Buzzard (Mar 21 2020 at 15:26):

Mario, concretely I'm saying that there is no big object with 0,1,+,* such that Z/2Z and Z/3Z are both subsets containing the 0 and 1 and closed under + and *

Z/2Z * Z/3Z?

It doesn't work

#### Kevin Buzzard (Mar 21 2020 at 15:27):

they have different 1's

#### Kevin Buzzard (Mar 21 2020 at 15:27):

Z/2Z x Z/3Z = Z/6Z and Z/2Z ={0,3} and Z/3Z={0,2,4}

#### Mario Carneiro (Mar 21 2020 at 15:27):

However I'm not sure that this is a problem. So what if the big not-a-ring fixes the characteristic? All rings in the commutative diagram will have compatible characteristics anyway

#### Gabriel Ebner (Mar 21 2020 at 15:27):

Oh yes, you're right.

#### Kevin Buzzard (Mar 21 2020 at 15:28):

It's not true that the rings will have the same characteristic. There is a perfectly good map Z/6Z -> Z/3Z

#### Mario Carneiro (Mar 21 2020 at 15:28):

compatible meaning divisible

#### Kevin Buzzard (Mar 21 2020 at 15:29):

This is weird. In the A-M situation it's a question about inclusions $A\subseteq B$ but there is a more general statement about maps $A\to B$

#### Mario Carneiro (Mar 21 2020 at 15:29):

this trick is only for inclusion maps, right?

#### Kevin Buzzard (Mar 21 2020 at 15:29):

and in the more general statement you certainly can't embed everything into an ambient type, but in the inclusion situation you can

#### Kevin Buzzard (Mar 21 2020 at 15:31):

I think @Chris Hughes suggestion is really interesting. It feels like a much more Lean-idiomatic way to do things.

#### Mario Carneiro (Mar 21 2020 at 15:31):

I think this trick is not generally applicable. It's good for groups, but I can't possibly see this generalizing to all the other interesting algebraic objects, given the constraints already in rings

#### Kevin Buzzard (Mar 21 2020 at 15:32):

Yes that is my guess too.

#### Kevin Buzzard (Mar 21 2020 at 15:32):

I don't understand what properties groups have that make the technique so powerful for them

#### Mario Carneiro (Mar 21 2020 at 15:33):

for it to be generally applicable, it needs to put basically no restrictions on the "mathematical content". If the embeddings were more unstructured, for example if they each pick their own 0,1,+,* operations, then this could work, but then you are basically just doing set theory

#### Kevin Buzzard (Mar 21 2020 at 15:33):

I feel like I am very interested in one structure consisting of three rings A, B, C and a commuting triangle A -> B -> C (in the maths sense, i.e. maps A -> B and B -> C)

#### Kevin Buzzard (Mar 21 2020 at 15:34):

and I am not at all sure that I want to assume that the image of A in B is isomorphic to the image of A in C

#### Mario Carneiro (Mar 21 2020 at 15:36):

I think what makes groups work is just what you said earlier: you can product a bunch of groups together to embed whatever you want. The category of groups has coproducts

#### Kevin Buzzard (Mar 21 2020 at 15:37):

the category of rings has coproducts too but the maps aren't in general injective

#### Kevin Buzzard (Mar 21 2020 at 15:37):

the coproduct of Z/2 and Z/3 is 0

#### Kevin Buzzard (Mar 21 2020 at 15:37):

if R is a ring and I have a map Z/2Z -> R and a map Z/3Z -> R (ring homs) then 2=0 and 3=0 in R so 1=0

#### Kenny Lau (Jun 05 2020 at 09:36):

how about we refactor algebra in terms of ring_hom like https://github.com/leanprover-community/mathlib/blob/a130c73a36a15ae2b98933e31ffb49a83c7f7420/src/field_theory/splitting_field.lean

#### Kenny Lau (Jun 05 2020 at 09:36):

like define is_noetherian : ring_hom A B \to Prop

#### Kenny Lau (Jun 05 2020 at 09:38):

hmm maybe this doesn't solve the problem

#### Kevin Buzzard (Jun 05 2020 at 10:27):

Another possibiilty is to do it all in the concrete category of rings

#### Kevin Buzzard (Jun 05 2020 at 10:28):

so you have all the flexibility of category theory notation and your ring stuff too

#### Kevin Buzzard (Jun 05 2020 at 10:28):

The reasom algebra is so interesting is because it is a bundled mophism

It's "Hom(A,B)"

#### Kevin Buzzard (Jun 05 2020 at 10:30):

and in some sense category theory or not category theory is the question about whether we want to do abstract homs ("sure you can compose them, here's the answer") or concrete homs ("this is a functional programming language, I will compose the functions")

#### Chris Hughes (Jun 05 2020 at 10:33):

The issue with algebra is that it gives rise to a module structure so it kind of has to be a class. If you've got some diagram of rings, then you have a ton of modules lying around, and it's quite difficult to synthesise the instances.

#### Kevin Buzzard (Jun 05 2020 at 10:37):

"I am a morphism of rings" is a troublesome concept. There seem to be several ways of setting up $Hom(A,R)$.. algebra A R is one way (bundled homs and coe_to_fun, which there are apparently problems with) or  A \to R plus a huge amount of typeclass inference ("Yes of course a division ring is a semimonoid, stop wasting my time" -- the curse of the invisible maps) or do you want to try some category theory A \hom B now @Scott Morrison has made it a concrete category?

#### Scott Morrison (Jun 05 2020 at 10:38):

bundled all the way! :-)

#### Kevin Buzzard (Jun 05 2020 at 10:39):

It seems to me that if the typeclass system is completely refactored in Lean 4 then perhaps it is worth attempting unbundled classes for ring homs again

#### Kevin Buzzard (Jun 05 2020 at 10:40):

Scott -- if you think everything should be bundled, then are you suggesting that category theory is a solution which will somehow avoid all the issues involved with carrying around boilerplate?

#### Johan Commelin (Jun 05 2020 at 10:42):

We want to pick one term of algebra R A (aka R →* A) and say: Hey, this one is special.
Lean is bad at composing special maps.

#### Kenny Lau (Jun 05 2020 at 10:43):

import ring_theory.adjoin

universes u v w

-- algebra.comap A B C is defeq to C
variables {A : Type u} [comm_ring A] [is_noetherian_ring A]
variables {B : Type v} [comm_ring B] [algebra A B]
variables {C : Type w} [comm_ring C] [algebra B C]
variables (hac : (⊤ : subalgebra A (algebra.comap A B C)).fg)
variables (hbc : (⊤ : submodule B (algebra.comap A B C)).fg)
include hac hbc

theorem Artin_Tate : (⊤ : subalgebra A B).fg :=
sorry


#### Kenny Lau (Jun 05 2020 at 10:43):

let's say this is the statement

#### Kenny Lau (Jun 05 2020 at 10:43):

then I think I should be able to prove this

#### Johan Commelin (Jun 05 2020 at 10:44):

But will you be able to use it?

#### Johan Commelin (Jun 05 2020 at 10:44):

I think Chris pointed out some time ago that we shouldn't have comap in theorem statements.

oh well oh no

#### Kenny Lau (Jun 05 2020 at 10:45):

is there just no way to state the theorem then?

#### Johan Commelin (Jun 05 2020 at 10:48):

How about you have an A-algebra structure on C and an A-alg-hom from B to C as argument?

#### Johan Commelin (Jun 05 2020 at 10:48):

Then you need to think about how you turn C into a B-module...

yeah...

#### Kenny Lau (Jun 05 2020 at 10:49):

and then we would need to define algebras on top of algebra

#### Kenny Lau (Jun 05 2020 at 10:49):

and then hence the title of this post

#### Johan Commelin (Jun 05 2020 at 10:49):

Yup... it hasn't been scaling for me either

#### Johan Commelin (Jun 05 2020 at 10:49):

I think that there has been almost no commutative algebra getting into mathlib for quite a long time. And it's mostly because of this issue, I think.

#### Kenny Lau (Jun 05 2020 at 10:50):

how did the ZFC people never realize this problem?

#### Johan Commelin (Jun 05 2020 at 10:50):

Because it isn't?

#### Kevin Buzzard (Jun 05 2020 at 10:51):

Mathematicians are only interested in what can be done in theory, not in what can be done in practice.

#### Johan Commelin (Jun 05 2020 at 10:52):

Just add an instance algebra A C to your statement, and drop the comap stuff. Then add H : the_diagram_commutes

#### Johan Commelin (Jun 05 2020 at 10:52):

And maybe this is the way to go...

#### Johan Commelin (Jun 05 2020 at 10:52):

Just have lots of explicit the_diagram_commutes hypothesis. And hope that we can build and API (and automation) around that.

#### Johan Commelin (Jun 05 2020 at 10:53):

But I feel like we need something better than function.comp for such machinery.

#### Chris Hughes (Jun 05 2020 at 10:56):

I think this is definitely the way to go. Just have functors from preorders, and a bunch of standard diagram shapes, and we'll use ring_hom.comp. For the standard shapes you'd be able to synthesize module instances as well, i.e., if the diagram in fin3 with the usual order, then field 2 is a module over field 0 and so on.

#### Kevin Buzzard (Jun 05 2020 at 10:56):

Kenny I never made it to the end of NSS :-( and I was really into that for a while, when I was teaching alg geom for the first time and trying to formalise it as well (just backing up Johan's claim that algebra has slowed down).

#### Kevin Buzzard (Jun 05 2020 at 10:57):

On the other hand, Amelia has completely refactored localisations, so progress is still being made.

#### Johan Commelin (Jun 05 2020 at 11:00):

Chris Hughes said:

I think this is definitely the way to go. Just have functors from preorders, and a bunch of standard diagram shapes, and we'll use ring_hom.comp.

1. I would like to abstract overring_hom.comp. So use category theory.
2. You need the diagrams to glue in an unobtrusive way. Whatever approach I think of with these diagrams... it always seems to lead to something really ugly and unreadable.

#### Johan Commelin (Jun 05 2020 at 11:00):

@Markus Himmel Can your diagram machinery help us here?

#### Chris Hughes (Jun 05 2020 at 11:02):

That is another problem actually. You want the fact that the corresponding diagram of polynomial rings commutes and all this stuff.

#### Johan Commelin (Jun 05 2020 at 11:02):

Ideally, I would like to be able to write (in 95% of the cases):

lemma blabla
(f : A → B) (g : B → D) (h : A → C) (i : B → D)
(hc : by obvious_diagram_commutes) :
...


#### Johan Commelin (Jun 05 2020 at 11:03):

by obvious_diagram_commutes should spit out some data structure that can be as ugly and complex as it wants, as long as I don't have to see it or write it!

#### Johan Commelin (Jun 05 2020 at 11:04):

And then whenever we have to prove such a hypothesis, another tactic steps in, and eats up all these complex data structures, and spits out the proof that is needed.

#### Chris Hughes (Jun 05 2020 at 11:04):

But this becomes quite complicated quite quickly. You also want the fact that ideal.quotient (I.map (ring_hom.of C)) \~- polynomial (ideal.quotient I) and there are hundreds of these little things.

#### Chris Hughes (Jun 05 2020 at 11:06):

This requires something quite powerful, I think it's probably possible but a big job.

But we need it.

#### Johan Commelin (Jun 05 2020 at 11:06):

Of course we can just do everything by hand. But that feels like admitting defeat to me.

#### Johan Commelin (Jun 05 2020 at 11:07):

Also, we'll never reach a proof of the big theorems in alg.geom / number theory if we have to do everything by hand.

Agreed.

#### Johan Commelin (Jun 05 2020 at 11:08):

The le/lt vs ge/gt issue already feels like defeat to me. But I can see past it. This one, I can't.

#### Chris Hughes (Jun 05 2020 at 11:08):

I have to do a fourth year project, and I was thinking about potentially doing something related to this. I have a lot of time, but maybe not enough

#### Kevin Buzzard (Jun 05 2020 at 11:09):

At some point someone said that Lean was "bad at carrying around a canonical instance". Type class inference seems to carry around the canonical 0, but we sometimes want to carry around the canonical map (and most definitely we do not want to do this all the time). How about an is_canonical typeclass for whatever $Hom(R,A)$ turns out to be?

#### Johan Commelin (Jun 05 2020 at 11:10):

What are the laws?

#### Kevin Buzzard (Jun 05 2020 at 11:10):

Many A-strutures are R-structures, but it's always comapping along the canonical map from R to A so we don't even bother noting that they're R-structures eplicitly

#### Kevin Buzzard (Jun 05 2020 at 11:10):

it's certainly transitive

#### Kevin Buzzard (Jun 05 2020 at 11:10):

it's most definitely never a global instance

#### Kevin Buzzard (Jun 05 2020 at 11:11):

because sometimes the identity is canonical but sometimes I'm checking that some diagram commutes under some explicit change of convention

#### Kevin Buzzard (Jun 05 2020 at 11:12):

e,g, once you picked a basis, the map from the vector space to the lists of real numbers is now canonical

#### Kevin Buzzard (Jun 05 2020 at 11:12):

Maybe canonicality is a purely local notion, which is why the global attempt to define it in Wikipedia is so atrocious.

#### Kevin Buzzard (Jun 05 2020 at 11:13):

I need a badge saying $v\mapsto(f\mapsto(-f(v)))$

#### Kevin Buzzard (Jun 05 2020 at 11:13):

The canonical map from a vector space to its double dual

#### Kevin Buzzard (Jun 05 2020 at 11:15):

There are two canonical maps from an idele group to the abelianisation of an absolute Galois group of Q, you choose which one you want (Artin or Deligne) and then all the maps between the objects will be the canonical ones under that normalisation in your paper on Shimura varieties.

#### Scott Morrison (Jun 05 2020 at 11:17):

canonical should mean a "flat section" of a functor C ⥤ Type. That is, a function f : Π X : C, F.obj X, with the property that for any iso i : X ≅ Y, we have F.map (i.hom) (f x) = f y.

#### Scott Morrison (Jun 05 2020 at 11:18):

(and you get to design the morphisms in C appropriately to make this fit examples)

#### Scott Morrison (Jun 05 2020 at 11:18):

as trivial examples, (λ R : Ring, (0 : R)) is a flat section of the forgetful functor Ring ⥤ Type, and hence "0 is canonical"

#### Johan Commelin (Jun 05 2020 at 11:20):

@Scott Morrison But will this help with Artin_Tate that Kenny posted above?

#### Johan Commelin (Jun 05 2020 at 11:20):

How would you write the statement of that result?

No idea :-)

#### Scott Morrison (Jun 05 2020 at 11:20):

I just want people to stop hoping canonical means something magical. :-)

#### Scott Morrison (Jun 05 2020 at 11:21):

I'm pretty sure the "canonical" map V to V-double-dual is canonical in this sense.

#### Kevin Buzzard (Jun 05 2020 at 11:21):

I am just explaining the specification, I don't know anything about the implementation :-)

#### Kevin Buzzard (Jun 05 2020 at 11:21):

Yes, the canonical map from V to its double-dual is also canonical, that's the point

#### Chris Hughes (Jun 05 2020 at 11:21):

The definition of canonical is part of the specification.

#### Kevin Buzzard (Jun 05 2020 at 11:22):

The definition is just that I want it to spit out the term I ask for.

#### Kevin Buzzard (Jun 05 2020 at 11:23):

And then you let me train it while I prove the Artin-Tate lemma with rings A,B,C and canonical maps between them

#### Kevin Buzzard (Jun 05 2020 at 11:23):

If A -> B is injective, and c is the canonical element of B, and it is in the image of A, then we just got a canonical element of A

#### Kevin Buzzard (Jun 05 2020 at 11:23):

They'll just come up as I think of them I think

#### Kevin Buzzard (Jun 05 2020 at 11:24):

Or maybe these rings A, B and C are somehow only rings up to isomorphism or up to canonical isomorphism perhaps

#### Johan Commelin (Jun 05 2020 at 11:26):

From the thesis of @Markus Himmel

meta structure chase_data :=
(morphisms : list morphism)
(comm_lemmas : list commutativity_lemma)
(elem_lemmas : list element_lemma)
(exact_lemmas : list exactness_lemma)


#### Johan Commelin (Jun 05 2020 at 11:26):

Maybe we need a similar data structure. And some tactics to prove commutativity diagrams.

#### Johan Commelin (Jun 05 2020 at 11:27):

It could even use coe_to_fun maybe.

#### Johan Commelin (Jun 05 2020 at 11:28):

Here's a concrete question: can you write me a tactic that collects all terms in the context that can be coerced to a function?

#### Johan Commelin (Jun 05 2020 at 11:29):

And then another one that asserts that any two possible paths with the same endpoints (via those collected functions) are propositionally equal.

#### Johan Commelin (Jun 05 2020 at 11:30):

Actually, I'm fine with providing all the maps in the diagram, for now.

#### Johan Commelin (Jun 05 2020 at 11:32):

  (hc : diagram_commutes [algebra_map A B, algebra_map B C, algebra_map A C])


The problem is that this doesn't type check, because algebra_map A B doesn't have the same type as algebra_map B C.

#### Chris Hughes (Jun 05 2020 at 11:37):

Johan Commelin said:

And then another one that asserts that any two possible paths with the same endpoints (via those collected functions) are propositionally equal.

I think this is essentially a finite problem, there are only finitely many (and not that many) ways of composing the paths together, and you can compute the transitive closure of a relation on a finite type, so I would say yes.

#### Johan Commelin (Jun 05 2020 at 11:42):

import ring_theory.adjoin

universe variables u

def list_of_functions :=
list (Σ (X Y : Type u), X → Y)

def diagram_commutes (l : list_of_functions) : Prop := sorry

section test
variables {A : Type u} [comm_ring A] [is_noetherian_ring A]
variables {B : Type u} [comm_ring B] [algebra A B]
variables {C : Type u} [comm_ring C] [algebra B C] [algebra A C]
variables (hac : (⊤ : subalgebra A C).fg)
variables (hbc : (⊤ : submodule B C).fg)
include hac hbc

theorem artin_tate
(hc : diagram_commutes [⟨A, B, algebra_map A B⟩,
⟨A, C, algebra_map A C⟩,
⟨B, C, algebra_map B C⟩]) :
(⊤ : subalgebra A B).fg := sorry

end test


#### Johan Commelin (Jun 05 2020 at 11:43):

Ideally this would become

theorem artin_tate
(hc : diagram_commutes (by duh) :
(⊤ : subalgebra A B).fg := sorry


#### Johan Commelin (Jun 05 2020 at 11:43):

For some value of duh

#### Chris Hughes (Jun 05 2020 at 11:44):

What information do you want to give the duh tactic?

#### Johan Commelin (Jun 05 2020 at 11:45):

It could just look through the context for assumptions that are arrow like: →, →+, →*, algebra A B, etc...

#### Chris Hughes (Jun 05 2020 at 11:46):

Do you want it to use things like polynomial.map_map?

#### Johan Commelin (Jun 05 2020 at 11:46):

No, it should just collect morphisms from the context

#### Johan Commelin (Jun 05 2020 at 11:47):

The smart tactics are the ones that consume diagram_commutes

#### Chris Hughes (Jun 05 2020 at 11:56):

I see. I'm not sure the smart tactics should consume diagram_commutes. Just like you can't prove equalities of ring expressions using simp [ring_axioms] you need something smarter to prove equality of expressions in categories that use standard category theory things like functors.

Hmm, I see

#### Johan Commelin (Jun 05 2020 at 12:01):

Nevertheless... it might work in most cases?

#### Johan Commelin (Jun 05 2020 at 12:02):

I mean... obviously can prove a lot of stuff in the category library.

#### Scott Morrison (Jun 05 2020 at 12:31):

and rewrite_search is very good at commutative diagrams...

#### Kenny Lau (Jun 30 2020 at 04:35):

So the solution (as of the current state of mathlib) is to have three maps between A, B, and C, and a claim that they commute?

#### Kenny Lau (Jun 30 2020 at 04:35):

(this thread has become kinda long for me to scroll through it)

#### Johan Commelin (Jun 30 2020 at 04:35):

That's whay I would like to have.
Plus automation to figure out why diagrams commute.

#### Kenny Lau (Jun 30 2020 at 04:36):

or maybe [algebra A B] [algebra B C] [algebra A C]?

#### Kenny Lau (Jun 30 2020 at 04:36):

(and then a fact that they commute)

Exactly

#### Johan Commelin (Jun 30 2020 at 04:39):

That's what I was thinking of somewhere upstairs

#### Kenny Lau (Jun 30 2020 at 04:53):

import ring_theory.integral_closure

universes u v w

variables (A : Type u) [comm_ring A]
variables (B : Type v) [comm_ring B]
variables (C : Type w) [comm_ring C]
variables [algebra A B] [algebra B C] [algebra A C]

class is_commute₃ : Prop :=
(smul_assoc : ∀ {x : A} {y : B} {z : C}, (x • y) • z = x • (y • z))


#### Kenny Lau (Jun 30 2020 at 04:53):

how does this look?

#### Kenny Lau (Jun 30 2020 at 05:15):

import ring_theory.integral_closure

universes u v w

variables (A : Type u) [comm_ring A]
variables (B : Type v) [comm_ring B]
variables (C : Type w) [comm_ring C]
variables [algebra A B] [algebra B C] [algebra A C]

class is_commute₃ : Prop :=
(smul_assoc : ∀ {x : A} {y : B} {z : C}, (x • y) • z = x • (y • z))

variables [is_commute₃ A B C]

theorem is_integral_trans' (hab : ∀ {y : B}, is_integral A y) {z : C}
(hz : is_integral B z) : is_integral A z :=
sorry


#### Kenny Lau (Jun 30 2020 at 05:16):

I will try (and maybe livestream on discord) to prove this after 30 minutes from now

#### Johan Commelin (Jun 30 2020 at 05:43):

@Kenny Lau I'm not sure whether is_commute3 should be a class.

why not?

#### Johan Commelin (Jun 30 2020 at 05:44):

I don't think tc is the correct sort of automation to take 5 is_commute instances and prove number 6

#### Johan Commelin (Jun 30 2020 at 05:44):

I want a solution that will also work in the statement of the snake lemma

#### Johan Commelin (Jun 30 2020 at 05:45):

In particular, my gut feeling is that we should state the condition in terms of composition of ordinary functions.

#### Johan Commelin (Jun 30 2020 at 05:46):

And probably a dedicated tactic can build proofs of is_commute by looking through the context for other terms of is_commute and then doing some elementary chase through the diagram.

#### Kenny Lau (Jun 30 2020 at 06:02):

import ring_theory.integral_closure

universes u v w

variables (A : Type u) [comm_ring A]
variables (B : Type v) [comm_ring B]
variables (C : Type w) [comm_ring C]
variables [algebra A B] [algebra B C] [algebra A C]

class is_commute₃ : Prop :=
(smul_assoc : ∀ {x : A} {y : B} {z : C}, (x • y) • z = x • (y • z))

variables [is_commute₃ A B C]

-- I hope this will never be used.
@[ext] lemma algebra.ext {R : Type u} {A : Type v}
[comm_semiring R] [semiring A] (h1 h2 : algebra R A)
(h : ∀ {r : R} {x : A}, (by clear h2; exact r • x) = r • x) : h1 = h2 :=
begin
unfreezingI { cases h1 with f1 g1 h11 h12, cases h2 with f2 g2 h21 h22,
cases f1, cases f2, congr', { ext r x, exact h },
ext r, erw [← mul_one (g1 r), ← h12, ← mul_one (g2 r), ← h22, h], refl }
end

-- I hope this will never be used.
theorem is_commute₃.comap_eq : algebra.comap.algebra A B C = _inst_6 :=
algebra.ext _ _ \$ λ x (z : C),
calc  algebra_map A B x • z
= (x • 1 : B) • z : by rw algebra.algebra_map_eq_smul_one
... = x • (1 : B) • z : by rw is_commute₃.smul_assoc
... = (by exact x • z : C) : by rw one_smul

theorem is_integral_trans' (hab : ∀ {y : B}, is_integral A y) {z : C}
(hz : is_integral B z) : is_integral A z :=
by { convert is_integral_trans @hab z hz, rw is_commute₃.comap_eq }


#### Kenny Lau (Jun 30 2020 at 06:02):

hey this worked like a charm!

#### Kenny Lau (Jun 30 2020 at 06:03):

@Johan Commelin @Kevin Buzzard

#### Kenny Lau (Jun 30 2020 at 06:03):

Johan Commelin said:

I want a solution that will also work in the statement of the snake lemma

I guess at this moment I'm only interested at formalizing a C/B/A situation

#### Johan Commelin (Jun 30 2020 at 06:04):

Will there be D/C/B/A situations?

#### Kevin Buzzard (Jun 30 2020 at 06:05):

Yes, but tomorrow

#### Kenny Lau (Jun 30 2020 at 06:05):

then I can have (if I still remember my combinatorics) four is_commute\3 instances

#### Kevin Buzzard (Jun 30 2020 at 06:05):

That might be like asking whether there will be a quotient.induction_on4 function one day

#### Johan Commelin (Jun 30 2020 at 06:07):

@Kevin Buzzard Well, you do care about the snake lemma, do you?

#### Kenny Lau (Jun 30 2020 at 06:13):

Artin--Tate is false!

#### Kenny Lau (Jun 30 2020 at 06:14):

Take A any Noetherian ring, B = A[x1, x2, ...], C = A, where B -> C sends each xi to 0

#### Kenny Lau (Jun 30 2020 at 06:14):

then C/A is algebra-finite and C/B is module-finite but B/A is not algebra-finite

#### Kenny Lau (Jun 30 2020 at 06:17):

So we need some injective hypothesis...? If so then why don't we just assume B is a subring of C to begin with?

#### Johan Commelin (Jun 30 2020 at 06:18):

section
variables {X Y Z : Type*} (f : X → Y) (g : Y → Z) (h : X → Z)

structure is_commute :=
(comm : g ∘ f = h)

variables {f g h}

lemma is_commute.apply_apply (H : is_commute f g h) (x : X) : g (f x) = h x :=
by rw [← H.comm]

end

section

variables (A : Type*) [comm_ring A]
variables (B : Type*) [comm_ring B]
variables (C : Type*) [comm_ring C]
variables [algebra A B] [algebra B C] [algebra A C]

abbreviation is_commute_alg := is_commute (algebra_map A B) (algebra_map B C) (algebra_map A C)

lemma is_commute_alg.smul_assoc (hc : is_commute_alg A B C) {x : A} {y : B} {z : C} :
(x • y) • z = x • (y • z) :=
by simp only [algebra.smul_def, ring_hom.map_mul, hc.apply_apply, mul_assoc]

end


#### Kenny Lau (Jun 30 2020 at 06:18):

what's the difference?

#### Johan Commelin (Jun 30 2020 at 06:18):

That the base structure would mix with group homs and ring homs etc...

#### Johan Commelin (Jun 30 2020 at 06:18):

It's not tying itself down to algebras

#### Johan Commelin (Jun 30 2020 at 06:19):

I care about commutative diagrams of modules

#### Kenny Lau (Jun 30 2020 at 06:19):

I've never seen a statement involving a tower of group extensions

oh ok

#### Johan Commelin (Jun 30 2020 at 06:19):

Kenny Lau said:

I've never seen a statement involving a tower of group extensions

Snake lemma

#### Kenny Lau (Jun 30 2020 at 06:25):

no no no this is all wrong

#### Kenny Lau (Jun 30 2020 at 06:25):

the correct definition of a diagram is a functor from a small category on fin n to the category of rings/modules/whatever

#### Kenny Lau (Jun 30 2020 at 06:25):

this doesn't mean we have to use the category theory library

#### Kenny Lau (Jun 30 2020 at 06:26):

Johan Commelin said:

def list_of_functions :=
list (Σ (X Y : Type u), X → Y)

def diagram_commutes (l : list_of_functions) : Prop := sorry


#### Kenny Lau (Jun 30 2020 at 06:27):

This won't work because we would have to use type equality

#### Kenny Lau (Jun 30 2020 at 06:27):

and then the workaround would be just to index the types with natural numbers

#### Kenny Lau (Jun 30 2020 at 06:27):

hence what I said about fin n

#### Kenny Lau (Jun 30 2020 at 06:28):

Again, when I say "category", I just mean a concrete implementation of category into Lean

#### Kevin Buzzard (Jun 30 2020 at 06:31):

Yes I think A can be anything but B to C has to be injective

#### Kevin Buzzard (Jun 30 2020 at 06:33):

There's an intermediate A-algebra B0 in the AM proof which has to be a subring of B (and of C)

#### Kenny Lau (Jun 30 2020 at 06:34):

so what's the point of using this if B is always a subring of C

#### Kenny Lau (Jun 30 2020 at 06:34):

anyway, I'm trying to make commutative diagrams, and I would like to know what it means for f1, f2: A -> B to commute

#### Johan Commelin (Jun 30 2020 at 06:37):

Kenny Lau said:

Johan Commelin said:

def list_of_functions :=
list (Σ (X Y : Type u), X → Y)

def diagram_commutes (l : list_of_functions) : Prop := sorry


Yup, I proposed something like that higher up in the thread... and I agree that we should generalise is_commute3.

#### Johan Commelin (Jun 30 2020 at 06:38):

But it's not obvious how to get it right. Because type equality, like you said.

#### Johan Commelin (Jun 30 2020 at 06:38):

And I want to take unions of diagrams, and add a vertex, etc...

#### Johan Commelin (Jun 30 2020 at 06:40):

I think this is an interesting nontrivial problem

#### Kenny Lau (Jun 30 2020 at 06:41):

@Johan Commelin come to my livestream to find out!

#### Johan Commelin (Jun 30 2020 at 06:42):

@Kenny Lau I'm on my way

#### Kevin Buzzard (Jun 30 2020 at 07:00):

I'll be there once I've got my daughter off to school

#### Kenny Lau (Jun 30 2020 at 07:48):

A question that has arisen from the livestream is whether algebra A B or A \to+* B should be the "simp-normal form"

#### Johan Commelin (Jun 30 2020 at 07:49):

Oooh, I thought the question was which side of algebra.smul_def should be SNF

#### Kenny Lau (Jul 01 2020 at 11:33):

what do we do with situations where the map is the Frobenius map? Then we would have two [algebra R R] instances

#### Kenny Lau (Jul 01 2020 at 11:34):

What are reasons preferring one over the other?

#### Kevin Buzzard (Jul 01 2020 at 11:36):

Usually in maths when one considers an R-module M as an R-module via the Frobenius there is some kind of notational indication of this, like $M^{(\sigma)}$ or something

#### Johan Commelin (Jul 01 2020 at 11:55):

aka a type synonym (-;

#### Chris Hughes (Jul 01 2020 at 12:29):

Sometimes the algebra type class is used when the module structure isn't really being considered, but maybe it was considered somewhere in a proof. I'm not sure it should be, I think perhaps the algebra type-class should only be used when you are really stating something about the algebra structure, i.e. the statement uses the module structure.

#4282

#### Kevin Buzzard (Sep 27 2020 at 08:18):

So the problem I ran into has been solved with is_scalar_tower. To summarise this thread, if you're proving things about three rings A subset B subset C then ideally you would have A a subring of B, B a subring of C, A a subring of C, B an A-algebra, C a B-algebra and C an A-algebra all at once. With the current set up in mathlib it doesn't even make sense to say all of these things at once. In the odd order work for groups this is fixed by making A,B,C all subgroups of a big group but this trick can't be done in general and one world rather work with types than terms anyway. This is a proof of concept that is_scalar_tower can be used instead.