algebra is not scaling for me

Stream: maths

[Kevin Buzzard]

artintate1.png

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]

This seems like a really nice test case.

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

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]

@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]

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

[Mario Carneiro]

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]

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]

@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]

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]

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

[Assia Mahboubi]

@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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

@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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

because there's an induced morphism

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

but actually the problem is much worse

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

aren't they all the same though?

[Kevin Buzzard]

sure

[Kevin Buzzard]

and of course I could hack through some proof

[Mario Carneiro]

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

[Assia Mahboubi]

@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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Assia Mahboubi]

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]

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

[Assia Mahboubi]

Yes

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

@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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Chris Hughes]

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]

I forgot the commutativity assumption but you get the idea.

[Assia Mahboubi]

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]

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]

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

[Assia Mahboubi]

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

[Kevin Buzzard]

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]

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]

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

[Assia Mahboubi]

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

[Patrick Massot]

Ooooh, that's bad

[Assia Mahboubi]

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]

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

[Kevin Buzzard]

but my type is nothing to do with finGroupType?

[Patrick Massot]

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

[Assia Mahboubi]

@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]

@Patrick Massot What is the expected version?

[Kevin Buzzard]

The expected version doesn't have the carrier type

[Patrick Massot]

Only one type, equipped with a group structure.

[Assia Mahboubi]

Because it is stated in set theory.

[Assia Mahboubi]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Assia Mahboubi]

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]

oops, I have to go offline, sorry.

[Kevin Buzzard]

thank you very much!

[Patrick Massot]

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]

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]

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]

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

[Kevin Buzzard]

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]

and the zero ring has 0=1

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

This doesn't matter

[Mario Carneiro]

and the inclusions are not ring homs

[Kevin Buzzard]

Oh this matters

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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 *

[Gabriel Ebner]

Z/2Z * Z/3Z?

[Kevin Buzzard]

It doesn't work

[Kevin Buzzard]

they have different 1's

[Kevin Buzzard]

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

[Mario Carneiro]

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]

Oh yes, you're right.

[Kevin Buzzard]

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

[Mario Carneiro]

compatible meaning divisible

[Kevin Buzzard]

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]

this trick is only for inclusion maps, right?

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

Yes that is my guess too.

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

like define is_noetherian : ring_hom A B \to Prop

[Kenny Lau]

hmm maybe this doesn't solve the problem

[Kevin Buzzard]

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

[Kevin Buzzard]

They made that now

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It's "Hom(A,B)"

[Kevin Buzzard]

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]

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]

"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]

bundled all the way! :-)

[Kevin Buzzard]

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]

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]

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]

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]

let's say this is the statement

[Kenny Lau]

then I think I should be able to prove this

[Johan Commelin]

But will you be able to use it?

[Johan Commelin]

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

[Kenny Lau]

oh well oh no

[Kenny Lau]

is there just no way to state the theorem then?

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

yeah...

[Kenny Lau]

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

[Kenny Lau]

and then hence the title of this post

[Johan Commelin]

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

[Johan Commelin]

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]

how did the ZFC people never realize this problem?

[Johan Commelin]

Because it isn't?

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

And maybe this is the way to go...

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Hughes]

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]

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]

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

[Johan Commelin]

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]

@Markus Himmel Can your diagram machinery help us here?

[Chris Hughes]

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

[Johan Commelin]

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]

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]

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]

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]

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

[Johan Commelin]

But we need it.

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Hughes]

Agreed.

[Johan Commelin]

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]

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]

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]

What are the laws?

[Kevin Buzzard]

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]

it's certainly transitive

[Kevin Buzzard]

it's most definitely never a global instance

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

The canonical map from a vector space to its double dual

[Kevin Buzzard]

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]

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]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

How would you write the statement of that result?

[Scott Morrison]

No idea :-)

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

The definition of canonical is part of the specification.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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

[Johan Commelin]

It could even use coe_to_fun maybe.

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

  (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]

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]

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]

Ideally this would become

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

[Johan Commelin]

For some value of duh

[Chris Hughes]

What information do you want to give the duh tactic?

[Johan Commelin]

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

[Chris Hughes]

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

[Johan Commelin]

No, it should just collect morphisms from the context

[Johan Commelin]

The smart tactics are the ones that consume diagram_commutes

[Chris Hughes]

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.

[Johan Commelin]

Hmm, I see

[Johan Commelin]

Nevertheless... it might work in most cases?

[Johan Commelin]

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

[Scott Morrison]

and rewrite_search is very good at commutative diagrams...

[Kenny Lau]

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]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Kenny Lau]

(and then a fact that they commute)

[Johan Commelin]

Exactly

[Johan Commelin]

That's what I was thinking of somewhere upstairs

[Kenny Lau]

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]

how does this look?

[Kenny Lau]

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]

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

[Johan Commelin]

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

[Kenny Lau]

why not?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

hey this worked like a charm!

[Kenny Lau]

@Johan Commelin @Kevin Buzzard

[Kenny Lau]

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]

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

[Kevin Buzzard]

Yes, but tomorrow

[Kenny Lau]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

Sure. But I also care about this Artin Tate lemma

[Kenny Lau]

Artin--Tate is false!

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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]

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

[Johan Commelin]

@Kenny Lau How about that?

[Kenny Lau]

what's the difference?

[Johan Commelin]

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

[Johan Commelin]

It's not tying itself down to algebras

[Johan Commelin]

I care about commutative diagrams of modules

[Kenny Lau]

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

[Kenny Lau]

oh ok

[Johan Commelin]

Kenny Lau said:

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

Snake lemma

[Kenny Lau]

no no no this is all wrong

[Kenny Lau]

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]

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

[Kenny Lau]

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]

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

[Kenny Lau]

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

[Kenny Lau]

hence what I said about fin n

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

I think this is an interesting nontrivial problem

[Kenny Lau]

@Johan Commelin come to my livestream to find out!

[Johan Commelin]

@Kenny Lau I'm on my way

[Kevin Buzzard]

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

[Kenny Lau]

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]

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

[Kenny Lau]

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

[Kenny Lau]

What are reasons preferring one over the other?

[Kevin Buzzard]

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]

aka a type synonym (-;

[Chris Hughes]

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.

[Kenny Lau]

#4282

[Kevin Buzzard]

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.

[Kenny Lau]

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