Zulip Chat Archive

Stream: maths

Topic: algebra is not scaling for me


view this post on Zulip Kevin Buzzard (Feb 17 2020 at 20:09):

artintate1.png

artintate2.png

There's a proof from Atiyah--Macdonald. There are three rings ABCA\subseteq B\subseteq C and during the proof a fourth ring B0B_0 between AA and CC is introduced. All the fast and loose playing with elements of BB makes me want to write this entire proof using subsets of CC (i.e. CC is a big ring and everything else is a subset). However the following concepts are also used: CC is finitely-generated as an AA-algebra, CC is finitely-generated as a BB-module, CC is finitely-generated as a B0B_0-module, B0B_0 is a Noetherian ring, BB is finitely-generated as a B0B_0-module, B0B_0 is finitely-generated as an AA-algebra, and BB is finitely-generated as an AA-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?

view this post on Zulip Johan Commelin (Feb 17 2020 at 20:45):

This seems like a really nice test case.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Feb 17 2020 at 20:56):

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

view this post on Zulip 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 B0B_0 is defined later on, and probably at this stage CC is an AA-algebra, but I'm going to need to make B0B_0 an AA-algebra and CC a B0B_0-algebra and hope that everything works out with CC now being an AA-algebra in two ways (actually maybe it isn't even an algebra in two ways, as that instance is not there I guess).

view this post on Zulip 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 AA, BB and CC 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ABCA\subseteq B\subseteq C..."

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:25):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:31):

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

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (Mar 21 2020 at 14:38):

@Kevin Buzzard I am lost : I though that in the proof AA, BB and CC are subsets, so what it is the problem with the "map" from AA to BB?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:39):

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

view this post on Zulip Assia Mahboubi (Mar 21 2020 at 14:39):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:40):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:40):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:40):

because there's an induced morphism

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:41):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:42):

but actually the problem is much worse

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:42):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:42):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:43):

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

view this post on Zulip Mario Carneiro (Mar 21 2020 at 14:43):

aren't they all the same though?

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:43):

sure

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:44):

and of course I could hack through some proof

view this post on Zulip Mario Carneiro (Mar 21 2020 at 14:44):

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

view this post on Zulip Assia Mahboubi (Mar 21 2020 at 14:44):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:45):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (Mar 21 2020 at 14:49):

Yes

view this post on Zulip Johan Commelin (Mar 21 2020 at 14:49):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 ABA\subseteq B, if I define integrality for this, then if I have rings AA' and BB' subsets of a large ring YY, with AA' isomorphic to AA and BB' isomorphic to BB and the diagram commuting, I can't deduce integrality of ABA'\to B' from integrality of ABA\to B

view this post on Zulip 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!)

view this post on Zulip 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?

view this post on Zulip 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 ABA\to B of rings.

view this post on Zulip Assia Mahboubi (Mar 21 2020 at 14:53):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:55):

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

view this post on Zulip 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"

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:57):

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

view this post on Zulip 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)

view this post on Zulip Chris Hughes (Mar 21 2020 at 14:58):

I forgot the commutativity assumption but you get the idea.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:05):

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

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Mar 21 2020 at 15:06):

Ooooh, that's bad

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 21 2020 at 15:06):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:06):

but my type is nothing to do with finGroupType?

view this post on Zulip Patrick Massot (Mar 21 2020 at 15:07):

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

view this post on Zulip 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).

view this post on Zulip Assia Mahboubi (Mar 21 2020 at 15:08):

@Patrick Massot What is the expected version?

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:08):

The expected version doesn't have the carrier type

view this post on Zulip Patrick Massot (Mar 21 2020 at 15:08):

Only one type, equipped with a group structure.

view this post on Zulip Assia Mahboubi (Mar 21 2020 at 15:08):

Because it is stated in set theory.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 21 2020 at 15:10):

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

view this post on Zulip Patrick Massot (Mar 21 2020 at 15:10):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:11):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Assia Mahboubi (Mar 21 2020 at 15:13):

oops, I have to go offline, sorry.

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:13):

thank you very much!

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 21 2020 at 15:22):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:23):

and the zero ring has 0=1

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 21 2020 at 15:24):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:24):

This doesn't matter

view this post on Zulip Mario Carneiro (Mar 21 2020 at 15:24):

and the inclusions are not ring homs

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:24):

Oh this matters

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:25):

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

view this post on Zulip Mario Carneiro (Mar 21 2020 at 15:25):

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

view this post on Zulip 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 *

view this post on Zulip Gabriel Ebner (Mar 21 2020 at 15:26):

Z/2Z * Z/3Z?

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:26):

It doesn't work

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:27):

they have different 1's

view this post on Zulip 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}

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Mar 21 2020 at 15:27):

Oh yes, you're right.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 21 2020 at 15:28):

compatible meaning divisible

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:29):

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

view this post on Zulip Mario Carneiro (Mar 21 2020 at 15:29):

this trick is only for inclusion maps, right?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:32):

Yes that is my guess too.

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:32):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:37):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 15:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 05 2020 at 09:36):

like define is_noetherian : ring_hom A B \to Prop

view this post on Zulip Kenny Lau (Jun 05 2020 at 09:38):

hmm maybe this doesn't solve the problem

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:27):

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

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:27):

They made that now

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:28):

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

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:28):

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

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:28):

It's "Hom(A,B)"

view this post on Zulip 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")

view this post on Zulip 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.

view this post on Zulip 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)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?

view this post on Zulip Scott Morrison (Jun 05 2020 at 10:38):

bundled all the way! :-)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 05 2020 at 10:43):

let's say this is the statement

view this post on Zulip Kenny Lau (Jun 05 2020 at 10:43):

then I think I should be able to prove this

view this post on Zulip Johan Commelin (Jun 05 2020 at 10:44):

But will you be able to use it?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jun 05 2020 at 10:45):

oh well oh no

view this post on Zulip Kenny Lau (Jun 05 2020 at 10:45):

is there just no way to state the theorem then?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 05 2020 at 10:48):

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

view this post on Zulip Kenny Lau (Jun 05 2020 at 10:48):

yeah...

view this post on Zulip Kenny Lau (Jun 05 2020 at 10:49):

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

view this post on Zulip Kenny Lau (Jun 05 2020 at 10:49):

and then hence the title of this post

view this post on Zulip Johan Commelin (Jun 05 2020 at 10:49):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jun 05 2020 at 10:50):

how did the ZFC people never realize this problem?

view this post on Zulip Johan Commelin (Jun 05 2020 at 10:50):

Because it isn't?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 05 2020 at 10:52):

And maybe this is the way to go...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 05 2020 at 10:53):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:57):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:00):

@Markus Himmel Can your diagram machinery help us here?

view this post on Zulip 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.

view this post on Zulip 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) :
  ...

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jun 05 2020 at 11:06):

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

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:06):

But we need it.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jun 05 2020 at 11:07):

Agreed.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)Hom(R,A) turns out to be?

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:10):

What are the laws?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 11:10):

it's certainly transitive

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 11:10):

it's most definitely never a global instance

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 11:13):

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

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 11:13):

The canonical map from a vector space to its double dual

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 05 2020 at 11:18):

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

view this post on Zulip 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"

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:20):

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

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:20):

How would you write the statement of that result?

view this post on Zulip Scott Morrison (Jun 05 2020 at 11:20):

No idea :-)

view this post on Zulip Scott Morrison (Jun 05 2020 at 11:20):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 11:21):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Jun 05 2020 at 11:21):

The definition of canonical is part of the specification.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 11:22):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 11:23):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:26):

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

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:27):

It could even use coe_to_fun maybe.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:30):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:43):

For some value of duh

view this post on Zulip Chris Hughes (Jun 05 2020 at 11:44):

What information do you want to give the duh tactic?

view this post on Zulip 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...

view this post on Zulip Chris Hughes (Jun 05 2020 at 11:46):

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

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:46):

No, it should just collect morphisms from the context

view this post on Zulip Johan Commelin (Jun 05 2020 at 11:47):

The smart tactics are the ones that consume diagram_commutes

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 05 2020 at 12:01):

Hmm, I see

view this post on Zulip Johan Commelin (Jun 05 2020 at 12:01):

Nevertheless... it might work in most cases?

view this post on Zulip Johan Commelin (Jun 05 2020 at 12:02):

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

view this post on Zulip Scott Morrison (Jun 05 2020 at 12:31):

and rewrite_search is very good at commutative diagrams...

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jun 30 2020 at 04:35):

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

view this post on Zulip Johan Commelin (Jun 30 2020 at 04:35):

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

view this post on Zulip Kenny Lau (Jun 30 2020 at 04:36):

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

view this post on Zulip Kenny Lau (Jun 30 2020 at 04:36):

(and then a fact that they commute)

view this post on Zulip Johan Commelin (Jun 30 2020 at 04:39):

Exactly

view this post on Zulip Johan Commelin (Jun 30 2020 at 04:39):

That's what I was thinking of somewhere upstairs

view this post on Zulip 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))

view this post on Zulip Kenny Lau (Jun 30 2020 at 04:53):

how does this look?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 30 2020 at 05:16):

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

view this post on Zulip Johan Commelin (Jun 30 2020 at 05:43):

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

view this post on Zulip Kenny Lau (Jun 30 2020 at 05:44):

why not?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 30 2020 at 05:44):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 }

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:02):

hey this worked like a charm!

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:03):

@Johan Commelin @Kevin Buzzard

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:04):

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

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 06:05):

Yes, but tomorrow

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:05):

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

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 06:05):

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

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:07):

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

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 06:09):

Sure. But I also care about this Artin Tate lemma

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:13):

Artin--Tate is false!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:18):

@Kenny Lau How about that?

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:18):

what's the difference?

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:18):

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

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:18):

It's not tying itself down to algebras

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:19):

I care about commutative diagrams of modules

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:19):

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

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:19):

oh ok

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:25):

no no no this is all wrong

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:25):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:27):

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

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:27):

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

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:27):

hence what I said about fin n

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:28):

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

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 06:31):

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

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:34):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:38):

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

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:38):

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

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:40):

I think this is an interesting nontrivial problem

view this post on Zulip Kenny Lau (Jun 30 2020 at 06:41):

@Johan Commelin come to my livestream to find out!

view this post on Zulip Johan Commelin (Jun 30 2020 at 06:42):

@Kenny Lau I'm on my way

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 07:00):

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

view this post on Zulip 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"

view this post on Zulip Johan Commelin (Jun 30 2020 at 07:49):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 01 2020 at 11:34):

What are reasons preferring one over the other?

view this post on Zulip 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(σ)M^{(\sigma)} or something

view this post on Zulip Johan Commelin (Jul 01 2020 at 11:55):

aka a type synonym (-;

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 27 2020 at 07:31):

#4282

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 29 2020 at 07:41):

rss-bot said:

feat(ring_theory/algebra_tower): Artin--Tate lemma (#4282)
feat(ring_theory/algebra_tower): Artin--Tate lemma (#4282)

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
https://github.com/leanprover-community/mathlib/commit/0bb5e5d94d688bdbde8615d924742315cbe19def


Last updated: May 09 2021 at 11:09 UTC