module refactoring

Stream: general

[Mario Carneiro]

I'm a bit late for my birthday deadline, but I have enough of the refactoring done that I'm ready to get feedback on it. See leanprover-community/module. Remarks:

• The main contributions here are the complete bundling of linear_map and submodule. In fact both of these were already present in mathlib, but making them primary makes everything go so much smoother.
• The structure of submodule and its category-theory-like interactions with linear_map are emphasized heavily. In particular, submodule is a complete lattice, map and comap are galois connections, there are tons of theorems about the map of an inf or the comap of fst and so on.
• The amount of duality here is staggering. I guess someone who is category theory minded will tell me that Mod is its own opposite category or some such thing, but it really shows in the equational theory. Even stuff like inl being dual to fst causes some nice properties, and some stuff plays even nicer than on Set like prod p q ⊔ prod p' q' = prod (p ⊔ p') (q ⊔ q').
• Injectivity and surjectivity of linear maps is expressed through ker and range (should I call it im?), and even linear_independent and basis can be expressed using properties of the lc.total function.

On the whole, I'm feeling really good about the results, and the proofs are much cleaner.

[Johan Commelin]

This is really cool! And yes, please call use im :lol:

[Mario Carneiro]

The name range is of course borrowed from terminology on set. I would rather not confuse with image which is map here

[Mario Carneiro]

map f p is the submodule f[p] where p is a submodule, and range f = map f \top = f[univ] which was previously called im on linear maps

[Mario Carneiro]

What is the common name for the coproduct pairing function? I called it copair since pair is used for the product pairing operation

[Kenny Lau]

but it's the same...

[Johan Commelin]

I think @Scott Morrison and @Reid Barton have the most experience with such decisions

[Johannes Hölzl]

this is really nice!

[Patrick Massot]

Mario, could you explain how all this solves the trouble we had with instance loops and multiple possible base rings?

[Kevin Buzzard]

I got caught up with something else this morning but later on today, when I have Lean time, I will just merge the patch and see how Hilbert basis goes with it. Does it compile sorry-free?

[Reid Barton]

copair/pair seems as good as anything else.
Normally we just write an arrow $A \oplus B \to C$ and let the reader do the boring work of figuring out what map we are actually talking about.

[Kenny Lau]

how about product or coproduct as a bifunctor?

[Mario Carneiro]

@Patrick Massot This doesn't address that issue, although it prepares the way a bit. I anticipate that this should be a comparatively simple change, but I didn't want the two refactorings to interact so I'm going to start on it as soon as this is done.

[Mario Carneiro]

@Kevin Buzzard It's not yet building. I finished the main linear algebra files, but I haven't finished up the cleanup of uses outside linear algebra. (There are no sorries, it just breaks.)

[Johannes Hölzl]

@Mario Carneiro by the way: the introduction of coe rewrites broke some proofs in set_theory/ordinal and cofinality. I fixed this, but you might want to do a different fix

[Mario Carneiro]

yeah, apologies for pushing stuff last night that broke things; my computer was running very slow and I was lacking feedback on whether my fixes worked

[Johannes Hölzl]

No problem. But I'm not sure if these are the intended changes. I didn't look too deep how these new simp rules are supposed to work.

[Mario Carneiro]

The idea is that coe will infer transitive instances, but since simp rules are only written on single coercions they won't fire on these composite instances. So we unfold them to multiple coe arrows first

[Mario Carneiro]

I don't think I realized this until lately, but lean will also infer transitive instances for coe + coe_fn and coe + coe_sort, and since the instances are different there are more simp lemmas associated to these

[Mario Carneiro]

I think the breakage is because some simp LHSs were written with composite instances, which now break because simp normal form doesn't have any composite instances. The fix is to make sure simp LHSs have multiple coercion in these cases

[Patrick Massot]

Ok, I'm less confused then (about modules, I'm still 100% confused about topological groups). I couldn't understand how those changes could help with the lost ring issue

[Chris Hughes]

Is it worth bundling ideals and subgroups as well?

[Johannes Hölzl]

I think we should replace ideals by submodules, so yes we want to have them bundled. I'm not sure about subgroups. We surely want a bundled version, but maybe still an unbundled one too

[Kevin Buzzard]

Johannes -- the idea about ideals was that submodule R M makes sense for varying R and M, but ideal R = submodule R R so only one input is needed.

[Chris Hughes]

But I think you want lattice and semiring on ideals as well, so you need bundles for that.

[Mario Carneiro]

I am of the opinion that subgroup and other such algebraic classes should also be bundled; almost all of the lattice structure theorems done here hold for anything that fits the structure of a universal algebra. ideal R := submodule R R can be defined as reducible so that all the theorems about submodules still apply.

[Mario Carneiro]

What are some examples where you think not having is_sub* will cause problems?

[Johan Commelin]

ideal R := submodule R R can be defined as reducible so that all the theorems about submodules still apply.

@Mario Carneiro I thought you said in Orsay that you couldn't think of any reason why a definition should be reducible. Has that changed? If so, can you explain?

[Kevin Buzzard]

If I open polynomial.lean (which I need for Hilbert basis) I just get 1000 errors. I think I would be happier to give feedback by trying to write Lean code and then getting stuck or finding things easier than before and reporting back. I find it hard to theorise about changes that I may not fully understand.

[Mario Carneiro]

Yeah, sorry about that. Mostly you can just open and read algebra.module and linear_algebra.basic for now. I'll let you know when it's really done (by pushing it to master, unless someone objects)

[Mario Carneiro]

I just didn't want to get too far afield with a change this sweeping without some input

[Mario Carneiro]

@Johan Commelin That's a fair point. There are three options here: (1) nonreducible def (2) reducible def (3) notation. In Orsay I argued that either (1) or (3) suffices in most cases where you think you want (2).

In this case, I don't think it matters too much, although (1) will require copying some instances like the complete_lattice instance, and possibly some theorems. Doing this would make the cleanest separation, allowing us to present a solid API for ideals that doesn't talk about modules half the time. (2) and (3) will entail some amount of API leakage here, moreso with (3) since it is submodule R R that will appear in all your statements.

The downsides of reducible defs (inconsistent handling in rw and simp) don't really apply when the def is a type since you don't usually do rewrites on a type, you just force it to be defeq to something else.

[Mario Carneiro]

This is a change I haven't implemented, but I'm considering it and want to get some feedback. Maybe a basis should be an injective function from some type into the module, i.e. the "basis" is really the range of this function, and the function gets to pick its indexing type. The reason is because we often tend to use a basis as an index for a sum, or as the domain of the free vector space to which to express isomorphism, or as the set whose cardinality is the dimension of the space - all of these roles are better accommodated by having an algebra of indexing types (which we already have courtesy of DTT) where measuring cardinality and indexing is more natural. (Also, it allows a basis to carry computational content, which isn't super important but indicates that this might be moving in the right direction.)

[Reid Barton]

From a mathematical perspective this change is very natural. We often write things like "let {b_1, ..., b_n} be a basis of V" but usually (whether we are aware of it or not) we really mean we are working with an indexed collection b_i, i.e., a function {1, ..., n} -> V.

[Reid Barton]

It's easy to say things which are false if taken literally in the "set style". For example: {x, y} is a linearly independent set in a vector space if and only if there do not exist nonzero a, b such that ax + by = 0. Well, not if x = y!

[Reid Barton]

On the other hand there are occasionally times when you genuinely need to work with subsets because you want to use the order structure and/or know that the collection of all possible bases is small, for example when proving that every vector space has a basis

[Mario Carneiro]

I think the statement about every vector space has a basis will explicitly use subsets

[Reid Barton]

I think the function approach is not really restrictive then anyways. You just say "a subset such that the inclusion is a basis".

[Mario Carneiro]

i.e. every vector space has a basis where the function is the subtype coercion and the indexing set is a subtype of the vector space

[Reid Barton]

(By the way, injectivity of the function is a consequence of being a basis, not a precondition.)

[Mario Carneiro]

I agree, I think under most circumstances you should be able to prove injectivity, except in trivial cases and in those cases you probably don't want to impose it additionally

[Mario Carneiro]

(bases over the zero ring are weird)

[Reid Barton]

Hmm... yes

[Mario Carneiro]

speaking of which... unit should be a ring

[Mario Carneiro]

it would fit nicely with the ring instance for products and Pis

[Reid Barton]

The nlab definition of basis is: A basis of a free R-module M (possibly a vector space, see basis of a vector space) is a linear isomorphism $B\colon M \to \oplus_{i\in I}R$ to a direct sum of copies of the ring R, regarded as a module over itself.

[Reid Barton]

I think this kind of property is more important than "for all i /= j, b_i /= b_j"

[Reid Barton]

... if you find yourself having to make some decision regarding the zero ring

[Reid Barton]

Yes okay, now I see you were saying the same thing regarding definition of bases over the zero ring

[Mario Carneiro]

so what does this say about linearly independent sets?

[Mario Carneiro]

I guess these should also be indexed

[Johan Commelin]

speaking of which... unit should be a ring

instance : comm_ring unit := by tidy

[Johan Commelin]

Good luck golfing that...

[Johan Commelin]

I'm pretty sure that tidy will also prove for you that it is the terminal object in Ring and CRing

[Kevin Buzzard]

I must confess I was surprised when I first saw that in Lean a basis was a subset. Mulling over this, I realised that it was because I was used to teaching students about bases of finite-dimensional vector spaces -- and this is not a conversation about bases, this is also a conversation about the concepts of linear independence and spanning -- and in these cases it seems more convenient when developing the theory to be considering lists of elements rather than subsets (so order matters, and repeats are OK). For a dumb example, consider the zero ring R. Then R^3=R and hence I want [0,0,0] to be a basis for R, which it is. This is the only case where bases can have repeated elements and also the only case where bases can have different cardinalities. A less pathological example is that if a basis of a fdvs is a list then a linear map is a matrix, rather than some weird concept of a matrix where we don't mind permuting the rows and columns which we'd get for sets. My students did a bunch of stuff involving this over the summer -- linear maps = matrices and so on -- and although their code is probably not mathlib-ready it would not surprise me if they had worked out some good useful and correct statements.

The only situation I know where subsets are better than maps from a type is in the Zorn proof that every vector space has a basis. But this result is in some sense a bit of a novelty, my impression is that working mathematicians very rarely think about infinite-dimensional vector spaces with no extra structure at all, and if there is extra structure (a topology or whatever) then the abstract notion of a basis is usually not what we want anyway (c.f. "basis" of a Hilbert space = lin ind subset with dense span).

[Johan Commelin]

If we are refactoring modules... would it make sense to rename span to generate? It would be more in line with all the other forms of generate...

[Mario Carneiro]

I was actually thinking about going the other way :)

[Mario Carneiro]

specifically as relates to other "closure" operations e.g. subgroup closure and normal closure

[Mario Carneiro]

For set-of-set operations like filter and topology I prefer generate, but maybe that's not principled enough

[Mario Carneiro]

I agree some uniformity of naming would be a good thing

[Johan Commelin]

Ok, I don't really care which one gets chosen :lol:

[Mario Carneiro]

So I've got to working on ideal now, and I have come to realize that ideal theory is not simply a specialization of submodule theory. It's obvious in hindsight, but as a category the homs are different - a ring hom is not a linear map, and a linear map is not a ring hom

[Mario Carneiro]

So this means that things like map and comap don't work the same way on rings

[Mario Carneiro]

In particular I don't even think there is a notion of ideal.map unless you assume the map is surjective

[Mario Carneiro]

Is there a way to make sense of a ring-changing hom from (R,M) to (R',M') modules?

[Scott Morrison]

Perhaps there's a notion of a map (R,M) to (R',M') as a linear map f : M to M', and a ring hom g : R' to R (note this is backwards), satisfying g(r') m = r' f(m).

[Scott Morrison]

I'm not sure it's particularly useful.

[Mario Carneiro]

yeah I was thinking the ring part might end up contravariant

[Mario Carneiro]

so I guess this does not generalize ring homs as maps (R,R) -> (R', R')

[Johan Commelin]

Is there a way to make sense of a ring-changing hom from (R,M) to (R',M') modules?

@Mario Carneiro What exactly do you mean with this question?

[Mario Carneiro]

I wonder if there is a common generalization of ring homs, (R,R) -> (R', R') and linear maps (R,M) -> (R, M')

[Mario Carneiro]

is there a category theory operation for taking a "total space" over the categories R-Mod where R is an object in the category Ring?

[Johan Commelin]

Sure.

[Johan Commelin]

That's a fibered category

[Johan Commelin]

And this one is one of the first examples

[Johan Commelin]

A map (R,M) → (R',M') is a pair R → R' + R' \otimes_R M → M'. (Or do I need commutativity for that tensor product?)

[Johan Commelin]

Yes, I do.

[Johan Commelin]

This doesn't work for arbitrary R → R'.

[Johan Commelin]

@Mario Carneiro Were you planning on doing left- right- and two-sided-ideals?

[Johan Commelin]

Or only ideals in comm_rings?

[Mario Carneiro]

Just comm ring ideals, since that's what's there now

[Johan Commelin]

Ok, so for comm_ring modules you get this really nice fibered category Mod.

[Johan Commelin]

Is that what you were looking for?

[Johan Commelin]

Note that by adjunction you can also just give a map M → M' that is R-linear

[Mario Carneiro]

R' \otimes_R M

what is this

[Johan Commelin]

Tensor product

[Johan Commelin]

turning M into an R'-module

[Mario Carneiro]

so R' is viewed as a R-module here?

[Johan Commelin]

Yes

[Mario Carneiro]

oh, there's an interesting construction we don't have

[Johan Commelin]

Which one?

[Mario Carneiro]

a ring hom R -> R' yields a R-module structure on R'

[Johan Commelin]

You mean the forgetful functor?

[Johan Commelin]

From R'-mod to R-mod?

[Mario Carneiro]

It's not forgetful, right?

[Johan Commelin]

Not really

[Mario Carneiro]

The hom could be anything

[Johan Commelin]

I still think of it as "forgetting"

[Johan Commelin]

We have R is an R-mod

[Johan Commelin]

So if you chain that to the "forget" instance, you have what you want.

[Mario Carneiro]

I don't follow

[Johan Commelin]

I tried adding "forget" about 3 months ago, and I ran into trouble.

[Mario Carneiro]

what forget instance?

[Johan Commelin]

But maybe with the refactor, you can now do it.

[Johan Commelin]

I mean R' is an R'-mod + every R'-mod is an R-mod.

[Johan Commelin]

I want your instance to be broken into 2 steps.

[Johan Commelin]

what forget instance?

The "forgetful" functor instance

[Mario Carneiro]

every R'-mod is an R-mod

This one requires an explicit ring hom input

[Johan Commelin]

Hmmm, it does... unless we turn R' into an algebra

[Johan Commelin]

over R

[Mario Carneiro]

ah, we don't have anything like that yet

[Mario Carneiro]

I needed assoc algebras around this time in metamath, now I forget why

[Mario Carneiro]

Ah - multivariate polynomials are the free assoc algebra

[Johan Commelin]

The ones we have are also commutative

[Johan Commelin]

At some point we might want non-commutative polynomials as well

[Mario Carneiro]

I have never touched noncomm polynomials, but I guess it's not so hard with the group ring construction

[Mario Carneiro]

... + free monoid construction which we already have

[Johan Commelin]

So, could we have f^* M'?

[Mario Carneiro]

I think so, what does that mean?

[Johan Commelin]

where f is a ring hom R → R' and M' is an R'-mod

[Johan Commelin]

So f^* is the functor R'-mod → R-mod

[Mario Carneiro]

ah, okay so this is the contravariant thing that scott mentioned

[Johan Commelin]

Right, and it is adjoint to tensoring.

[Johan Commelin]

Which is covariant

[Johan Commelin]

no, that's bullcrap

[Johan Commelin]

I'm brainfarting

[Johan Commelin]

tensor is adjoint to hom

[Johan Commelin]

Lol. So you get to choose: either you use f^* which is contravariant. Or you use tensor products, and you get something covariant, but "harder to parse".

[Johan Commelin]

@Mario Carneiro How would all this abstract nonsense help with:

So I've got to working on ideal now, and I have come to realize that ideal theory is not simply a specialization of submodule theory. It's obvious in hindsight, but as a category the homs are different - a ring hom is not a linear map, and a linear map is not a ring hom

[Kenny Lau]

And nobody here has pointed out that extensions of ideals exist, c.f. Atiyah-Macdonald P.9

[Kenny Lau]

In particular I don't even think there is a notion of ideal.map unless you assume the map is surjective

if f:A->B is a ring hom and L is an ideal in A then L^e is the ideal generated by f(L)

[Kenny Lau]

2018-10-08.png

[Mario Carneiro]

yeah, okay that's a better idea

[Mario Carneiro]

just close the resulting set under ideal operations

[Johan Commelin]

@Mario Carneiro Do you have some sort of todo list of what remains for this refactor?

[Mario Carneiro]

@Johan Commelin It's just some idle speculation on my part, I don't really have any concrete implementation ideas

[Mario Carneiro]

I'm currently in "tying up loose ends" mode in the refactor, I don't want to introduce new things

[Johan Commelin]

Great!

[Mario Carneiro]

it's already behind schedule too much

[Mario Carneiro]

although it has made several other projects come to the fore, which I will probably have to start working on after I'm done

[Mario Carneiro]

foremost of which is the multiple scalar field thing

[Johan Commelin]

After you are done, I think faster should be the first thing on your list. :lol:

[Mario Carneiro]

I'm actually working on that ATM

[Johan Commelin]

Wonderful! Thanks for doing that!

[Kevin Buzzard]

Here are some thoughts. The fundamental notion in algebraic geometry is an "f-map" -- see 6.21.7 in the stacks project. Lemma 6.21.8 shows that this is a natural idea. Although it's dressed up in a geometric language, this is something related to the conversation here. The notion of an f-map shows up in the definition of a morphism of ringed spaces in definition 6.21. In the discussion just below 6.26.3 here we see the notion of an f-map of sheaves of modules. Note in particular in that discussion that the f-maps from G to F are in canonical bijection with two other hom sets, one involving only sheaves on X and one involving only sheaves on Y.

Now of course all this needs a lot of unravelling, and the way to unravel is to ask how what de Jong writes translates into the case of affine schemes, which are just commutative rings in disguise. If I got it right, then he says to focus on the following idea: if $f:A\to B$ is a map of rings and if $G$ is an $A$-module and $F$ a $B$-module, an $f$-map $G\to F$ is simply an $A$-module homomorphism from $G$ to $F$, and the observation is that such maps naturally biject with the $B$-module homomorphisms from $G\otimes_AB$ to $F$. I think this is different to what Scott suggests -- he went the other way.

[Kevin Buzzard]

I wonder if there is a common generalization of ring homs, (R,R) -> (R', R') and linear maps (R,M) -> (R, M')

I think $f$-maps give this. An $f$-map $(R,M)\to (R',M')$ is a ring map $R\to R'$ and an $R$-module map $M\to M'$ (note I'm constantly using this trick of, the moment I have a ring map $R\to R'$, considering all $R'$-modules as $R$-modules). If $R\to R'$ is the identity then this is just an $R$-module homomorphism, and an example of an $f$-map $(R,R)\to(R',R')$ is given by $(f,f)$, but given $f:R\to R'$ there are $f$-maps $(R,R)\to (R',R')$ which are not $(f,f)$.

[Kevin Buzzard]

OK so Johan has isolated exactly the same idea, but somehow it seems that he has come from a completely different viewpoint (I don't know what a fibred category is). Regarding commutative v non-commutative, I think it's a good idea to push commutative here. Someone impressed on me decades ago that one should not think of commutative ring theory as a special case of non-commutative ring theory but regard them as completely different areas. I don't know anything about research into non-commutative ring theory, but commutative ring theory is very much alive and kicking -- e.g. ideas from the theory of perfectoid spaces were used here https://arxiv.org/abs/1608.08882 to resolve a the direct summand conjecture. Commutative algebra is the foundation of modern algebraic geometry and I have always been of the opinion (even before I knew anything about formal proof verification software) that books like Atiyah--Macdonald and Matsumura (both standard commutative algebra textbooks) somehow "operated close to the axioms" whilst still being of great modern interest. If we want to push Lean as a tool for algebraic geometry, which it one day might become, then there's no harm focussing on commutative algebra. When someone eventually decides to do some basic representation theory of finite groups we might have to plough through basics of semisimple algebras but that is somehow a completely different project.

[Johan Commelin]

@Kevin Buzzard A fibered category is the thing that underlies a stack.

[Johan Commelin]

Basically it abstracts $f$-maps

[Kevin Buzzard]

every R'-mod is an R-mod

This one requires an explicit ring hom input

Patrick mentioned recently that sometimes it's best to concentrate on the morphisms, not the objects. In alg geom we even see it in the name -- an $f$-map is a construction which depends on a map $f$ of rings. In fact Johan is saying all the right things, I need to get up much earlier to get ahead of him. Given $f:R\to R'$ there are then adjoint functors $(R-mod)\to(R'-mod)$ and $(R'-mod)\to(R-mod)$ and hopefully Kenny proved enough about universal property of tensor products to show that these are adjoints. I think that Scott's punt went in the wrong direction. There is a time when you get maps one way and the other way, but that's when you go back to schemes.

[Johan Commelin]

In fact Johan is saying all the right things, I need to get up much earlier to get ahead of him.

I've got a 2-year old daughter. You can't win.

[Johan Commelin]

Well, what I think that Scott meant that f → f^* is contravariant.

[Kevin Buzzard]

Kenny's construction is something else though. If $L$ is an ideal of $A$ then $L^e$, the pushforward ideal, is less well-behaved. $L^e$ is the image of $L\otimes_AB$ (the canonical thing when it comes to modules) under the natural map from this guy to $B$ corresponding by adjointness to the map $L\to B$. So it might satisfy some universal property for ideals, but probably not for modules.

[Kevin Buzzard]

OK I think that's all I have to say and I think that most of it had been said already, but at least I caught up.

[Johan Commelin]

For ideals it will probably give you a Galois connection. Here! I said it. Without checking.

[Mario Carneiro]

But I guess $L^e$ is the best you can do when you have a ring hom A->B and an ideal L?

[Johan Commelin]

If you want an ideal of B, yes.

[Johan Commelin]

Otherwise, you could just tensor, and treat it as a module.

[Mario Carneiro]

Is this a thing we can currently do?

[Johan Commelin]

What?

[Mario Carneiro]

tensoring like that

[Johan Commelin]

I guess almost

[Johan Commelin]

@Kenny Lau Did you include extension of scalars in your work on tensor products?

[Johan Commelin]

@Mario Carneiro Given what we have, it shouldn't be too hard

[Kenny Lau]

I don’t think I did.

[Kevin Buzzard]

Oh I see. The issue is that if $M$ is an $A$-module and $B$ is an $A$-algebra (and hence an $A$-module) then $M\otimes_AB$ is not just an $A$-module but a $B$-module.

[Johan Commelin]

Right, we don't have something like that atm

[Johan Commelin]

But it shouldn't be hard to put a B-mod structure on the tensor product.

[Johan Commelin]

I don't know if it should "extend" the A-mod structure, in the sense that if you "restrict" scalars you get an A-mod that is defeq to what you started with.

[Patrick Massot]

foremost of which is the multiple scalar field thing

I'm completely lost: I thought this module refactor was mostly about multiple scalars

[Kenny Lau]

How's it going? @Mario Carneiro

[Mario Carneiro]

waiting on my school work to decrease in intensity

[Mario Carneiro]

hopefully I should be able to find some time for it this week

[Kenny Lau]

https://github.com/leanprover-community/mathlib/commits/module

[Kenny Lau]

@Mario Carneiro is there anything we can help with?

[Mario Carneiro]

Possibly... I'm just short on time these days. The main work is done, I think, but a bunch of files still need to be updated

[Kenny Lau]

what can we do?

[Kenny Lau]

should I fix the errors?

[Mario Carneiro]

go in there and make the red squiggles go away

[Kenny Lau]

roger that

[Mario Carneiro]

Don't get too attached to anything that you write there, I'll probably have a look through all the files anyway, but it will be a lot easier if it's not already broken

[Kenny Lau]

@Mario Carneiro there are things that you deleted and things that depend on them, right

[Kenny Lau]

I'll just leave those untouched

[Mario Carneiro]

like what? I think all deleted files have equivalents

[Kenny Lau]

like the order embedding of submodules of submodules, and the prime ideal, and the trivial ideal

[Kenny Lau]

and also this:

@[simp] theorem Union_set_of_directed {ι} (hι : nonempty ι)
  (S : ι → submodule α β)
  (H : ∀ i j, ∃ k, S i ≤ S k ∧ S j ≤ S k) :
  ((supr S : submodule α β) : set β) = ⋃ i, S i :=

[Mario Carneiro]

prime ideals are still there

[Mario Carneiro]

search for that, it moved somewhere else

[Mario Carneiro]

I think it is Union_coe now

[Kenny Lau]

prime_ideal doesn't give me anything

[Kenny Lau]

and i wouldn't search for prime

[Mario Carneiro]

the trivial ideal is bottom

[Kenny Lau]

ok I searched for prime and I found it

[Kenny Lau]

@Mario Carneiro what about the embedding “submodules of N” -> “submodules of M” where N is a submodule of M?

[Mario Carneiro]

I think that's map N.subtype or map_subtype.order_iso

[Kenny Lau]

@Mario Carneiro I've pushed a partial fix

[Kenny Lau]

I'll see what more I can do

[Kenny Lau]

@Mario Carneiro for principal ideal domains, the situation is that {x | a ∣ x} is a set not an ideal, so these definitions are a bit troublesome:

class is_principal_ideal [comm_ring α] (S : set α) : Prop :=
(principal : ∃ a : α, S = {x | a ∣ x})

class principal_ideal_domain (α : Type*) extends integral_domain α :=
(principal : ∀ (S : ideal α), is_principal_ideal (S : set α))

[Kenny Lau]

what should I do?

[Kenny Lau]

@Mario Carneiro ideal.quotient.eq is missing

[Kenny Lau]

(and submodule.quotient.eq doesn't count)

[Kenny Lau]

Successfully reduced to 4 errors. Pushed.

[Mario Carneiro]

the ideal {x | a ∣ x} is now spelled span {a}

[Kenny Lau]

@Mario Carneiro by "now" do you mean "I've changed that in my private copy" or "I should change that and then push it"?

[Mario Carneiro]

I mean in the module branch that's how it is currently used

[Mario Carneiro]

so if you find it elsewhere you should use that

[Kenny Lau]

so it's the latter?

[Kenny Lau]

ok

[Mario Carneiro]

is_principal_ideal should be a property of S : ideal

[Kenny Lau]

and what is to become of ideal.quotient.eq? @Mario Carneiro

[Mario Carneiro]

what does quotient_ring look like now?

[Kenny Lau]

it looks like ideal.quotient now

[Kenny Lau]

we have ideal.quotient.mk := submodule.quotient.mk and we have submodule.quotient,eq

[Kenny Lau]

but not ideal.quotient.eq

[Mario Carneiro]

oh sure, you can state ideal.quotient.eq

[Kenny Lau]

ok

[Mario Carneiro]

it's just a defeq copy paste job

[Kenny Lau]

I just thought I wouldn't add things without first asking you

[Mario Carneiro]

I have not added all theorems from submodules to ideals, I intended to add them as needed

[Mario Carneiro]

you can often just use the submodule version directly, but it is slightly less ergonomic

[Kenny Lau]

I agree (with the latter statement)

[Kenny Lau]

lemma mem_span_singleton {x y : α} :
  x ∈ span ({y} : set α) ↔ ∃ a, a * y = x :=

[Kenny Lau]

@Mario Carneiro can I change this to use dvd?

[Mario Carneiro]

maybe make another theorem

[Kenny Lau]

but nobody uses that theorem

[Kenny Lau]

you added that theorem yourself

[Kenny Lau]

lemma is_maximal_of_irreducible {p : α} (hp : irreducible p) :
  is_maximal (span ({p} : set α)) :=

Should this be an instance?

[Mario Carneiro]

oh I see, it's copy pasted from the analogous theorem on submodule, where you can't use dvd

[Mario Carneiro]

as for that last one - probably not. Things like irreducible and maximal and nat.prime are forming a new kind of idiom, where the predicate is a class but most of the theorems use it like normal assumptions

[Mario Carneiro]

This is primarily intended to support the few cases where you have to use typeclass inference, like in Z/nZ is a field

[Kevin Buzzard]

I want there to be an "is_an_integer" predicate on eg rat to save me from coercions.

[Kenny Lau]

@Kevin Buzzard wrong thread?

[Kevin Buzzard]

Isn't that a predicate which is a class?

[Kenny Lau]

oh well this is going off track

[Chris Hughes]

Why is it a class?

[Mario Carneiro]

I don't just mean a predicate that is a class, we have plenty of those like first_countable X. I mean predicates that are classes that we use without instance brackets in most theorems

[Kenny Lau]

I feel like there is not enough transparency with the module refactoring, so I've decided to write something about it.

Major changes made:

• semimodule α β and module α β and vector_space α β now take one more argument, that β is an add_comm_group, i.e. before making an instance of a module, you need to prove that it's an abelian group first.
• vector space is no longer over a field, but a discrete field.
• The idiom for making an instance module α β (after proving that β is an abelian group) is module.of_core { smul := sorry, smul_add := sorry, add_smul := sorry, mul_smul := sorry, one_smul := sorry }.
• is_linear_map and linear_map are now both structures, and they are independent, meaning that linear_map is no longer defined as subtype is_linear_map. The idiom for making linear_map from is_linear_map is is_linear_map.mk' (f : M -> N) (sorry : is_linear_map f), and the idiom for making is_linear_map from linear_map is f.is_linear (i.e. linear_map.is_linear f).
• is_linear_map.add etc no longer exist. instead, you can now add two linear maps together, etc.
• the classis_submodule is gone, replaced by the structure submodule which contains a carrier, i.e. if N : submodule R M then N.carrier is a type. And there is an instance module R N in the same situation.
• similarly, the class is_ideal is gone, replaced by the structure ideal, which also contains a carrier.
• endomorphism ring and general linear group are defined.
• submodules form a complete lattice. the trivial ideal is now idiomatically the bottom element, and the universal ideal the top element.
• linear_algebra/quotient_module.lean is deleted, and it's now submodule.quotient (so if N : submodule R M then submodule R N.quotient) Similarly, quotient_ring.quotient is replaced by ideal.quotient. The canonical map from N to N.quotient is submodule.quotient.mk, and the canonical map from the ideal I to I.quotient is ideal.quotient.mk I.
• linear_equiv is now based on a linear map and an equiv, and the difference being that now you need to prove that the inverse is also linear, and there is currently no interface to get around that.
• Everything you want to know about linear independence and basis is now in the newly created file linear_algebra/basis.lean.
• Everything you want to know about linear combinations is now in the newly created file linear_algebra/lc.lean.
• linear_algebra/linear_map_module.lean and linear_algebra/prod_module.lean and linear_algebra/quotient_module.lean and linear_algebra/submodule.lean and linear_algebra/subtype_module.lean are deleted (with their contents placed elsewhere).

[Mario Carneiro]

Ha, this was my secret plan all along

[Kenny Lau]

I think one would prefer transparency

[Mario Carneiro]

now that kenny had to read the stuff he knows what changed

[Mario Carneiro]

and can write a nice summary for us

[Kenny Lau]

lol

[Mario Carneiro]

A remark on module.of_core: it's only intended for use when you aren't proving it's a semimodule first

[Mario Carneiro]

like if you don't care about semimodules

[Kenny Lau]

I'm sure Kevin doesn't

[Mario Carneiro]

By the way, is_linear_map is a late addition. I'm hoping it will not be needed much at all, but it's useful to have as a mixin occasionally

[Kenny Lau]

one would have to refactor tensor_product to get rid of all the dependencies thereto, I believe

[Mario Carneiro]

I really want linear_map to be the primary one

[Mario Carneiro]

oh, I may have done that already

[Kenny Lau]

not entirely

[Mario Carneiro]

shoot, I have an unsaved file in vscode

[Kenny Lau]

lol

[Mario Carneiro]

re: interface for linear_equiv, you don't need to prove the inverse is linear, that's not in the structure

[Mario Carneiro]

it's just the union (pushout?) of linear_map and equiv

[Kenny Lau]

oh, right

[Kenny Lau]

@Mario Carneiro are you going to push your file?

[Mario Carneiro]

oh wait, looks like I already pushed most of it

[Mario Carneiro]

you already had the important stuff

[Kenny Lau]

but tensor product still depends on is_linear_map right?

[Kenny Lau]

protected def id : R ⊗ M ≃ₗ M :=
{ inv_fun := (⊗ₜ) 1,
  left_inv := lift.ext
    (linear_map.is_linear $ linear_map.comp (is_linear_map.mk' _ $ (bilinear _ _).linear_right 1) (lift _ _))
    linear_map.id.is_linear
    (λ x y, by simp; rw [← tmul_smul, ← smul_tmul, smul_eq_mul, mul_one]),
  right_inv := λ m, by simp,
  .. (lift (λ c x, c • x)
    ⟨λ m, linear_map.is_linear (linear_map.smul_right linear_map.id m),
    λ r, linear_map.is_linear (r • linear_map.id)⟩ : R ⊗ M →ₗ M) }

[Kenny Lau]

I don't think anyone wants to see this

[Mario Carneiro]

what is your objection exactly?

[Kenny Lau]

1. the linear map needs to be put after ..; 2. lack of is_linear_map.comp and the fact that lift.ext and most of the things in tensor_product depend on is_linear_map make proofs very long and cumbersome

[Mario Carneiro]

I've only done the first half of that file, so some things may still need to be hashed out

[Mario Carneiro]

lift.ext should take linear maps as input

[Mario Carneiro]

You shouldn't feel bound to the current way statements of theorems are written, that's what refactoring is about

[Mario Carneiro]

Ideally, this construction should be easy, just cobbling together functions we already know are linear

[Mario Carneiro]

I think we need another constructor for is_bilinear_map, or is_linear_map, that takes a linear function and asks you to prove equality to the target function

[Mario Carneiro]

which corresponds to the alternate definition def is_linear_map (f : β → γ) := ∃ g : β →ₗ γ, ∀ x, f x = g x

[Kenny Lau]

lift.ext should take linear maps as input

I don't think that will work, because there are things that need to be proved to be linear

[Kenny Lau]

do you think I should change is_bilinear_map to bilinear_map?

[Mario Carneiro]

Huh? lift.ext takes two functions and proofs that they are linear

[Mario Carneiro]

that can always be contracted to a function taking a linear_map arg

[Mario Carneiro]

I thought about it, but do the set of all bilinear maps have a nice structure like linear maps? Like can you add them and such

[Kenny Lau]

yes

[Kenny Lau]

they're even a module

[Kenny Lau]

they're as nice as linear maps

[Kenny Lau]

(because of the universal property of tensor product :P)

[Mario Carneiro]

well okay then

[Mario Carneiro]

I think bilinear_map still needs to reference is_linear_map though

[Kenny Lau]

@[reducible] def bilinear_map := M →ₗ N →ₗ P

[Kenny Lau]

how about this

[Mario Carneiro]

oh! does that work?

[Kenny Lau]

I'm experimenting with it now

[Mario Carneiro]

is Mod(R) a CCC?

[Kenny Lau]

CCC?

[Mario Carneiro]

cartesian closed category

[Mario Carneiro]

i.e. that thing means what you want it to

[Kenny Lau]

yes

[Kenny Lau]

actually I don't know

[Kenny Lau]

I just know that Hom(M tensor N, P) = Hom(M, Hom(N, P))

[Kenny Lau]

so (- tensor N) is right adjoint to Hom(N, -)

[Mario Carneiro]

that looks a lot like the universal property of the exponential

[Mario Carneiro]

Hom(N,P) there is actually an object of the category

[Kenny Lau]

import group_theory.free_abelian_group
import linear_algebra.basic tactic.squeeze

variables (R : Type*) [comm_ring R]
variables (M : Type*) (N : Type*) (P : Type*) {Q : Type*}
variables [add_comm_group M] [add_comm_group N] [add_comm_group P] [add_comm_group Q]
variables [module R M] [module R N] [module R P] [module R Q]
include R

@[reducible] def bilinear_map := M →ₗ N →ₗ P

variables {R M N P}

namespace bilinear_map
variables {M N P Q}

section mk
variable (f : M → N → P)
variable (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
variable (H2 : ∀ c m n, f (c • m) n = c • f m n)
variable (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
variable (H4 : ∀ c m n, f m (c • n) = c • f m n)

def bilinear_map.mk :
  bilinear_map R M N P :=
⟨λ m, ⟨f m, H3 m, λ c, H4 c m⟩,
λ m₁ m₂, linear_map.ext $ H1 m₁ m₂,
λ c m, linear_map.ext $ H2 c m⟩

theorem bilinear_map.mk_apply (m : M) (n : N) :
  bilinear_map.mk f H1 H2 H3 H4 m n = f m n := rfl

end mk

variables (f : bilinear_map R M N P)

def comm : bilinear_map R N M P :=
bilinear_map.mk (λ n m, f m n)
  (λ n₁ n₂ m, (f m).map_add _ _)
  (λ c n m, (f m).map_smul _ _)
  (λ n m₁ m₂, by rw f.map_add; refl)
  (λ c n m, by rw f.map_smul; refl)

@[simp] theorem comm_apply (m : M) (n : N) : f.comm n m = f m n := rfl

def left (y : N) : M →ₗ P := f.comm y
def right (x : M) : N →ₗ P := f x

@[simp] theorem left_apply (x : M) (y : N) : f.left y x = f x y := rfl
@[simp] theorem right_apply (x : M) (y : N) : f.right x y = f x y := rfl

theorem zero_left (y) : f 0 y = 0 := (f.left y).map_zero
theorem zero_right (x) : f x 0 = 0 := (f.right x).map_zero

theorem neg_left (x y) : f (-x) y = -f x y := (f.left y).map_neg _
theorem neg_right (x y) : f x (-y) = -f x y := (f.right x).map_neg _

theorem add_left (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y := (f.left y).map_add _ _
theorem add_right (x y₁ y₂) : f x (y₁ + y₂) = f x y₁ + f x y₂ := (f.right x).map_add _ _

theorem smul_left (r x y) : f (r • x) y = r • f x y := (f.left y).map_smul _ _
theorem smul_right (r x y) : f x (r • y) = r • f x y := (f.right x).map_smul _ _

def comp₁ (g : Q →ₗ M) : bilinear_map R Q N P :=
linear_map.comp f g

@[simp] theorem comp₁_apply (g : Q →ₗ M) (q : Q) (n : N) :
  f.comp₁ g q n = f (g q) n := rfl

def comp₂ (g : Q →ₗ N) : bilinear_map R M Q P :=
linear_map.comp ⟨λ x, linear_map.comp x g, λ _ _, rfl, λ _ _, rfl⟩ f

@[simp] theorem comp₂_apply (g : Q →ₗ N) (m : M) (q : Q) :
  f.comp₂ g m q = f m (g q) := rfl

def comp₃ (g : P →ₗ Q) : bilinear_map R M N Q :=
linear_map.comp ⟨g.comp, λ x y, linear_map.ext $ λ n, g.map_add _ _,
  λ c x, linear_map.ext $ λ n, g.map_smul _ _⟩ f

@[simp] theorem comp₃_apply (g : P →ₗ Q) (m : M) (n : N) :
  f.comp₃ g m n = g (f m n) := rfl

end bilinear_map

[Kenny Lau]

looking good

[Mario Carneiro]

maybe I'm spoiled, but I would hope that there was a direct way to get comm

[Mario Carneiro]

maybe it requires the tensor product though

[Mario Carneiro]

I guess it is equivalent to saying that left is a linear map

[Mario Carneiro]

If apply : M -> (M ->l N) ->l N was linear we would have it

[Kenny Lau]

and if comp was also linear.. :P

[Mario Carneiro]

yeah, there should be a principled way to do this using CCCs

[Kenny Lau]

but that would be too category-theoretical for our purposes

[Mario Carneiro]

I mean with the categories unfolded away

[Mario Carneiro]

We know that CCCs interpret lambda calculus, so literally anything you can write down that is type correct will be linear

[Mario Carneiro]

we just need the right building blocks to get everything else

[Kenny Lau]

but we also know that lambda calculus is generated by abstraction and application?

[Mario Carneiro]

yes

[Kenny Lau]

but abstraction isn't a linear map?

[Mario Carneiro]

That's apply

[Kenny Lau]

so what's the conclusion?

[Mario Carneiro]

er, no - abstraction is the UMP of apply

[Mario Carneiro]

it works because the families we are considering are themselves linear in their free variables

[Mario Carneiro]

so you get a "lambda" like operator

[Mario Carneiro]

In this context we wouldn't actually be able to write down lambda, because we have "the wrong lambda", it isn't linear because we don't have the right notion of family for the category

[Mario Carneiro]

but we can run any lambda term through the CCC translation to get a term using only CCC primitives, and we can prove these are all linear

[Johan Commelin]

I really like where this is going! Keep up the good work!

[Kevin Buzzard]

Yes many thanks Kenny for trying to get the show back on the road. Does this stuff compile yet? Is it worth going back to Hilbert basis theorem yet?

[Kenny Lau]

Fixed

[Kenny Lau]

@Mario Carneiro what's the next step?

[Mario Carneiro]

is it compiling now?

[Kenny Lau]

yes

[Mario Carneiro]

sweet

[Mario Carneiro]

unfortunately I still need to finish and review it myself, so it's in the queue with the other PRs now

[Mario Carneiro]

If things go well I will have time this weekend for it

[Kenny Lau]

nice

[Mario Carneiro]

but if you see any other ways to improve it, add more theorems etc, now's the time

[Mario Carneiro]

the CCC laws seem like a good place to start

[Mario Carneiro]

prove that curry : (A X B -> C) -> (A -> B -> C) is a linear map

[Mario Carneiro]

an equiv, even

[Kenny Lau]

ok

[Kenny Lau]

I don't think that's true

[Mario Carneiro]

put l everywhere

[Mario Carneiro]

that's homs in the category

[Kenny Lau]

it's (M tensor N) -> P equiv M -> (N -> P)

[Kenny Lau]

1. (M ⊗ N) ⊗ P -> M ⊗ (N ⊗ P)
2. (M ⊗ N) -> P -> M ⊗ (N ⊗ P)
3. P -> (M ⊗ N) -> M ⊗ (N ⊗ P)
4. P -> M -> N -> M ⊗ (N ⊗ P)
5. M -> P -> N -> M ⊗ (N ⊗ P)
6. M -> N -> P -> M ⊗ (N ⊗ P)
7. M -> N ⊗ P -> M ⊗ (N ⊗ P)
````

[Mario Carneiro]

yes

[Mario Carneiro]

linear equiv I assume

[Mario Carneiro]

But I chose that one specifically because it's one of the CCC primitives

[Johan Commelin]

canonical linear equiv, even... :grinning_face_with_smiling_eyes:

[Mario Carneiro]

apply is another: (M -> N) X M -> N

[Mario Carneiro]

it's trivial with that equiv though

[Mario Carneiro]

I think the hom adjunction is equivalent to a few terms that you can compose

[Mario Carneiro]

like apply and curry

[Mario Carneiro]

do we have everything we need for the tensor product to be a product?

[Mario Carneiro]

Is it also the coproduct?

[Johan Commelin]

Nope

[Johan Commelin]

Coproduct is the direct sum, which is also the product

[Johan Commelin]

Tensor product is in fact the coproduct in the category of commutative rings

[Kevin Buzzard]

Yes but for modules over a commutative ring it's a different story. You can see something funny is going on because there aren't natural maps from M to M tensor N or from M tensor N to M

[Kevin Buzzard]

Other than the zero map

[Mario Carneiro]

wait what?

[Mario Carneiro]

this is a funny product indeed

[Kenny Lau]

1. (M ⊗ N) ⊗ P -> M ⊗ (N ⊗ P)
2. (M ⊗ N) -> P -> M ⊗ (N ⊗ P)
3. M -> N -> P -> M ⊗ (N ⊗ P)
4. M -> N ⊗ P -> M ⊗ (N ⊗ P)

[Kenny Lau]

(N ≃ₗ P) -> ((M →ₗ N) ≃ₗ (M →ₗ P))

[Johan Commelin]

Are you listing the things that you are currently proving?

[Mario Carneiro]

I think he's just enumerating type correct statements and looking for inhabited types?

[Johan Commelin]

Do we have dual?

[Johan Commelin]

Because M.dual \otimes N = Hom(M,N) might be an interesting statement...

[Kenny Lau]

that's just M ->L R

[Kenny Lau]

and what you said is only true for M finitely dimensional vector space

[Johan Commelin]

Of course, but it is a useful concept.

[Johan Commelin]

I'm probably missing some hypotheses...

[Mario Carneiro]

don't let truth get in the way of beauty

[Kenny Lau]

protected def assoc : (M ⊗ N) ⊗ P ≃ₗ M ⊗ (N ⊗ P) :=
linear_equiv.of_linear
  (lift $ lift $ comp (unlift' _ _ _ _) $ unlift id)
  (lift $ comp (lift' _ _ _ _) $ unlift $ unlift id)
  (lift.ext' $ linear_map.ext $ λ m, lift.ext' $ bilinear_map.ext $ λ n p,
    by repeat { rw lift.tmul <|> rw comp₃_apply <|> rw comp_apply <|> rw mk_apply <|>
        rw lift'_apply <|> rw comm'_apply <|> rw unlift_apply <|> rw unlift'_apply <|> rw id_apply })
  (lift.ext' $ comm_inj $ linear_map.ext $ λ p, lift.ext' $ bilinear_map.ext $ λ m n,
    by repeat { rw lift.tmul <|> rw comp₃_apply <|> rw comp_apply <|> rw comm_apply <|> rw mk_apply <|>
        rw lift'_apply <|> rw comm'_apply <|> rw unlift_apply <|> rw unlift'_apply <|> rw id_apply })

[Johan Commelin]

@Kenny Lau How far are we from defining the category of commutative R-algebras?

[Kenny Lau]

oh well

[Kenny Lau]

what's the concrete version of your question?

[Johan Commelin]

Flat ring homs

[Kenny Lau]

@[reducible] def bilinear_map := M →ₗ N →ₗ P

[Kenny Lau]

should we just remove bilinear_map entirely?

[Johan Commelin]

I think we can leave it out till people start complaining.

[Johan Commelin]

I would encourage everyone to use linear maps out of the tensor product.

[Johan Commelin]

Anyway, I would be really happy if we have flat ring homs. Especially if it is readable, instead of the obfuscated kludge that we sometimes see... I think flat ring homs can be a good test case to see if mathlib is ready for the 25 other properties of ring homs that algebraic geometry depends upon.

[Kenny Lau]

what are the 25 other properties?

[Kenny Lau]

def map (f : M →ₗ P) (g : N →ₗ Q) : M ⊗ N →ₗ P ⊗ Q :=
lift $ comp₁ (comp₂ (mk _ _ _) g) f

man my interface is really good

[Johan Commelin]

https://stacks.math.columbia.edu/tag/02WE most of these have an equivalent for rings

[Kenny Lau]

def map (f : M →ₗ P) (g : N →ₗ Q) : M ⊗ N →ₗ P ⊗ Q :=
lift $ comp₁ (comp₂ (mk _ _ _) g) f

@[simp] theorem map_tmul (f : M →ₗ P) (g : N →ₗ Q) (m : M) (n : N) :
  map f g (m ⊗ₜ n) = f m ⊗ₜ g n :=
rfl

how on earth is this rfl

[Mario Carneiro]

of course it is, it's a quotient

[Kenny Lau]

well then why isn't this rfl:

@[simp] lemma lift.tmul (x y) :
  lift f (x ⊗ₜ y) = f x y :=

[Kenny Lau]

@[simp] lemma lift.tmul (x y) :
  lift f (x ⊗ₜ y) = f x y :=
zero_add _

[Kenny Lau]

I guess that's why

[Mario Carneiro]

where'd that come from?

[Kenny Lau]

the free group

[Chris Hughes]

@[simp] lemma lift.tmul (x y) :
  lift f (x ⊗ₜ y) = f x y :=
zero_add _

I love proofs like this.

[Mario Carneiro]

free_abelian_group.lift also isn't rfl

[Kenny Lau]

right

[Kenny Lau]

it's zero_add as well

[Mario Carneiro]

but why? It's built out of pieces that are rfl

[Mario Carneiro]

is it free_group.to_group?

[Mario Carneiro]

ah yes

[Mario Carneiro]

def to_group.aux : list (α × bool) → β :=
λ L, list.prod $ L.map $ λ x, cond x.2 (f x.1) (f x.1)⁻¹

def to_group : free_group α → β :=
quot.lift (to_group.aux f) $ λ L₁ L₂ H, red.step.to_group H

[Mario Carneiro]

@[simp] lemma to_group.of {x} : to_group f (of x) = f x :=
one_mul _

[Kenny Lau]

so it's all in list.prod

[Kenny Lau]

under which semantics is by simp; simp only [linear_equiv.apply_symm_apply] supposed to work where by simp [linear_equiv.apply_symm_apply] fails?

[Mario Carneiro]

lol, now this has got me thinking about rewriting free_group again

[Mario Carneiro]

one way to get the right defeqs here is to have the actual definition of free_group be the quotient of expressions in the language of groups with the group laws, and then prove that this is isomorphic to lists

[Kenny Lau]

and how would one implement "expressions"?

[Mario Carneiro]

expressions in the language of groups means trees

[Mario Carneiro]

you just have a symbol for one and inv and mul

[Mario Carneiro]

and the basis elements

[Mario Carneiro]

and you get trees

[Kenny Lau]

and what do you mean by tree?

[Mario Carneiro]

inductive group_expr (A) : Type
| one : group_expr
| inv : group_expr -> group_expr
| mul : group_expr -> group_expr -> group_expr

[Kenny Lau]

aha

[Kenny Lau]

how would that help?

[Mario Carneiro]

if you define this as an inductive, and define the relations as a quotient, you will get really nice defeq

[Mario Carneiro]

lift (x * y) = lift x * lift y, lift 1 = 1, lift x = f x

[Kenny Lau]

I don't see how this is different from redefining list.prod so that list.prod [f] is definitionally equivalent to f?

[Kenny Lau]

oh

[Kenny Lau]

fair enough

[Johan Commelin]

one way to get the right defeqs here is to have the actual definition of free_group be the quotient of expressions in the language of groups with the group laws, and then prove that this is isomorphic to lists

Wait... in the other thread you said we shouldn't focus on getting all the right defeqs... :sad:

[Mario Carneiro]

lol

[Mario Carneiro]

sometimes it matters

[Mario Carneiro]

The reason quotient types exist is because of defeqs

[Mario Carneiro]

otherwise we would just use sets of sets

[Johan Commelin]

/me doesn't follow... noob alert...

[Mario Carneiro]

there is no way to build quotient types like lean's without an axiom

[Mario Carneiro]

we can get something provably isomorphic, but it won't have the defeq on lift

[Johan Commelin]

I probably haven't experience the pain of working without lean's quotient types... what is wrong with sets of sets?

[Mario Carneiro]

It allows you to define functions that have a certain behavior by definition on the basis elements

[Mario Carneiro]

You can live without defeq, in set theory they do this

[Kenny Lau]

@Mario Carneiro so, are you going to do it, or do you intend me to do it? :P

[Mario Carneiro]

but it is nice to have for computational purposes

[Mario Carneiro]

I think I have enough major projects to do :) Like Johan says, it's not essential

[Kenny Lau]

ok

[Mario Carneiro]

but if it interests you, feel free

[Johan Commelin]

I encourage both of you to first get this merged into mathlib before embarking on new projects...

[Johan Commelin]

(or expanding the scope of this refactor)

[Kenny Lau]

ok I pushed the tensor product

[Kenny Lau]

@Mario Carneiro should we PR it now?

[Mario Carneiro]

sure, that will give it more exposure

[Kenny Lau]

more exposure to what?

[Mario Carneiro]

people with ideas

[Mario Carneiro]

or who like to read about new things on github

[Mario Carneiro]

obviously I'm already aware of this PR, and I will merge it when ready

[Kenny Lau]

and when is it ready?

[Mario Carneiro]

when I am satisfied with all the changes? It was unfinished when I last reviewed it

[Mario Carneiro]

thank you for fixing the bugs, but some things still take time

[Patrick Massot]

Thank you very much @Kenny Lau for the documentation effort (and help with actual Lean)! Should we already copy that to docs/theories/linear_algebra or could it still change?

[Kenny Lau]

It could still change

[Patrick Massot]

Ok. It would be very useful if you could update it when it will stabilize, so that we'll be able to incorporate it to the docs

[Kenny Lau]

@Mario Carneiro ok I pushed the refactored free_group.lean

[Kenny Lau]

(it won't build now; I'll fix the errors if you like the new free_group)

[Kenny Lau]

also, I don't understand why it is ok that linear_map doesn't take the ring as an argument

[Kenny Lau]

ok I put the free group in a new branch and resetted the PR'ed branch

[Kevin Buzzard]

So I thought I'd try and get the hang of modules in Lean. Is this construction somewhere in the module branch:

import linear_algebra.basic

example (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type)
  [add_comm_group M] (HM : module S M) : module R M := sorry

?

[Kevin Buzzard]

Idly trying to prove it myself:

import linear_algebra.basic

example (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type)
  [add_comm_group M] [HM : module S M] : module R M :=
{ smul_add := sorry,
  add_smul := sorry,
  mul_smul := sorry,
  one_smul := sorry,
  zero_smul := sorry,
  smul_zero := sorry
}
/-

failed to synthesize type class instance for
R S : Type,
_inst_1 : comm_ring R,
_inst_2 : comm_ring S,
f : R → S,
_inst_3 : is_ring_hom f,
M : Type,
_inst_4 : add_comm_group M,
HM : module S M
⊢ has_scalar R M

-/

[Chris Hughes]

It's a new structure. Don't you just have to define a has_scalar instance first?

[Kevin Buzzard]

import linear_algebra.basic

instance has_scalar_of_ring_hom (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type) [has_scalar S M] :
has_scalar R M := {
  smul := λ r m, (f r) • m
}

example (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type)
  [add_comm_group M] [HM : module S M] : module R M :=
{ smul_add := sorry,
  add_smul := sorry,
  mul_smul := sorry,
  one_smul := sorry,
  zero_smul := sorry,
  smul_zero := sorry
}
-- maximum class-instance resolution depth has been reached

My question is whether this is already in the module refactoring, which I think was to a certain extent inspired by the fact that this used to be hard to do

[Chris Hughes]

I don't think type class inference knows how to infer f. Try making the first things a def, and then giving to_has_scalar or whatever explicitly. Thinking about it, I don't think the second thing can be an instance with the current setup either.

[Kevin Buzzard]

Oh this is exactly one of those situations where I don't know how to put something into the type class inference machine because I'm in term mode.

[Chris Hughes]

by haveI := _; exact _

[Kevin Buzzard]

import linear_algebra.basic

def has_scalar_of_ring_hom (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type) [has_scalar S M] :
has_scalar R M := {
  smul := λ r m, (f r) • m
}

example (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type)
  [add_comm_group M] [HM : module S M] : module R M :=
  begin haveI := has_scalar_of_ring_hom R S f M,
  exact
{ smul_add := sorry,
  add_smul := sorry,
  mul_smul := sorry,
  one_smul := sorry,
  zero_smul := sorry,
  smul_zero := sorry
}
end

[Kevin Buzzard]

no errors :D

[Kevin Buzzard]

so I have to go into tactic mode to put something into the type class inference machine?

[Chris Hughes]

I think so.

[Chris Hughes]

This should also work I think.

example (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type)
  [add_comm_group M] [HM : module S M] : module R M :=
{ to_has_scalar := has_scalar_of_ring_hom R S f M,
  smul_add := sorry,
  add_smul := sorry,
  mul_smul := sorry,
  one_smul := sorry,
  zero_smul := sorry,
  smul_zero := sorry }
end

[Kevin Buzzard]

Now I have problems with two smuls. @Kenny Lau Is this done already? I don't want to waste my time if it's already there, but this is exactly what I have always needed for Hilbert basis.

[Chris Hughes]

I would wait until after module refactorign

[Kenny Lau]

the right thing to do is just say smul := sorry, right

[Kenny Lau]

no, this hasn’t been done

[Kevin Buzzard]

I thought module refactoring had happened

[Kenny Lau]

you should also read my summary of the changes, this is mentioned there

[Kenny Lau]

and also you should use module.of_core

[Kenny Lau]

and also you should use module.of_core

[Kevin Buzzard]

I thought I had read your summary of the changes :-/

[Kevin Buzzard]

Chris your version is better:

example (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type)
  [add_comm_group M] [HM : module S M] : module R M :=
{ to_has_scalar := has_scalar_of_ring_hom R S f M,
  smul_add := λ r x y,smul_add (f r) x y, -- works
  add_smul := sorry,
  mul_smul := sorry,
  one_smul := sorry,
  zero_smul := sorry,
  smul_zero := sorry }

example (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type)
  [add_comm_group M] [HM : module S M] : module R M :=
by haveI := has_scalar_of_ring_hom R S f M;
  exact
{ smul_add := λ r x y, smul_add (f r) x y, -- fails
  add_smul := sorry,
  mul_smul := sorry,
  one_smul := sorry,
  zero_smul := sorry,
  smul_zero := sorry
}

[Kevin Buzzard]

I see. I think Kenny is pointing out that by "The idiom for making an instance module α β (after proving that β is an abelian group) is module.of_core" he means the strong statement that end users should actually never make modules directly. Is that right Kenny? I still need an instance of module R M though -- how do I get it?

[Kevin Buzzard]

example (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type)
  [add_comm_group M] [HM : module S M] : module R M := module.of_core {
    smul := sorry,
    smul_add := sorry,
    add_smul := sorry,
    mul_smul := sorry,
    one_smul := sorry
  }

Maybe I'm on the right lines now

[Kenny Lau]

right

[Kevin Buzzard]

    add_smul := λ r s m, -- (is_ring_hom.map_add f).symm ▸ (add_smul (f r) (f s) m), -- stupid triangle never works for me
      begin show f (r + s) • m = f r • m + f s • m, rw is_ring_hom.map_add f, exact add_smul (f r) (f s) m,end,

[Kenny Lau]

i think you are missing two arguments

[Kevin Buzzard]

import linear_algebra.basic

example (R S : Type) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] (M : Type)
  [add_comm_group M] [HM : module S M] : module R M := module.of_core {
    smul := λ r m, (f r) • m,
    smul_add := λ r, smul_add $ f r,
    add_smul := λ r s m, -- (is_ring_hom.map_add f).symm ▸ (add_smul (f r) (f s) m), -- stupid triangle never works for me
      begin show f (r + s) • m = f r • m + f s • m, rw is_ring_hom.map_add f, exact add_smul (f r) (f s) m,end,
    mul_smul := λ r s m, begin show f (r * s) • m = f r • (f s • m), rw is_ring_hom.map_mul f, exact mul_smul (f r) (f s) m,end,
    one_smul := λ m, begin show f 1 • m = m, rw is_ring_hom.map_one f, exact one_smul m, end
  }

Still haven't lost my touch ;-) [ugh]

[Kevin Buzzard]

well so far I got 0% of the way through proving Hilbert basis, but at least I learnt not to use module

[Kevin Buzzard]

Does this completely fundamental fact have a name?

Current version:

import linear_algebra.basic

instance module_of_module_of_ring_hom {R : Type*} [ring R] {S : Type*} [ring S] (f : R → S) [is_ring_hom f] {M : Type*}
  [add_comm_group M] [HM : module S M] : module R M := module.of_core {
    smul := λ r m, (f r) • m,
    smul_add := λ r, smul_add $ f r,
    add_smul := λ r s m, -- (@is_ring_hom.map_add _ _ _ _ f _ r s) ▸ (add_smul (f r) (f s) m), -- stupid triangle never works for me
      begin show f (r + s) • m = f r • m + f s • m, rw is_ring_hom.map_add f, exact add_smul (f r) (f s) m,end,
    mul_smul := λ r s m, begin show f (r * s) • m = f r • (f s • m), rw is_ring_hom.map_mul f, exact mul_smul (f r) (f s) m,end,
    one_smul := λ m, begin show f 1 • m = m, rw is_ring_hom.map_one f, exact one_smul m, end
  }

[Kevin Buzzard]

rw doesn't do unfolding (i.e. if I tell it rw H with H : X = Y and X isn't directly in view, it won't start unfolding things in an attempt to find X, even if something immediately unfolds to give X). Is the same true for the stupid triangle?

[Chris Hughes]

Yes. What about erw

[Kevin Buzzard]

I still seem to need the show for add_smul.

[Kevin Buzzard]

add_smul := λ r s m, (((@is_ring_hom.map_add _ _ _ _ f _ r s).symm ▸ (add_smul (f r) (f s) m)) : f (r + s) • m = f r • m + f s • m),

[Kevin Buzzard]

longer than the tactic proof ;-)

[Johan Commelin]

It ought to be by tidy.

[Kevin Buzzard]

does tidy know to try a theorem called add_smul when proving something called add_smul?

[Johan Commelin]

Only if it is a simp-lemma

[Johan Commelin]

But maybe, once backwords reasoning is merged, this could realistically done by tidy.

[Kevin Buzzard]

Will this instance ever trigger?

[Chris Hughes]

I doubt it. It will have to find a ring hom out of nowhere.

[Kenny Lau]

maybe we should make ring_hom just like linear_map

[David Michael Roberts]

is Mod(R) a CCC?

No, because the monoidal structure is not cartesian. What you want is https://ncatlab.org/nlab/show/closed+monoidal+category

[Kenny Lau]

(deleted)

[Kenny Lau]

(deleted)

[Mario Carneiro]

okay, my other obligations are done, so I'm working on finishing the refactoring tonight

[Kenny Lau]

import data.polynomial

local attribute [instance, priority 1] classical.prop_decidable

universes u v w

open polynomial

theorem leading_term_aux {R} [nonzero_comm_ring R] {f g : polynomial R} (Hle : nat_degree f ≤ nat_degree g)
  (Hf : f ≠ 0) (Hg : g ≠ 0) (Hh : leading_coeff f + leading_coeff g ≠ 0) :
leading_coeff (f * X ^ (nat_degree g - nat_degree f) + g) = leading_coeff f + leading_coeff g :=
sorry

def ideal.leading_coeff {R : Type u} [nonzero_comm_ring R] (I : ideal (polynomial R)) : ideal R :=
{ carrier := leading_coeff '' I,
  zero := ⟨0, I.zero_mem, rfl⟩,
  add := λ a b ⟨f, hf1, hf2⟩ ⟨g, hg1, hg2⟩, sorry/-begin
    by_cases h0 : a + b = 0, rw h0, exact ⟨0, I.zero_mem, rfl⟩,
    by_cases hf : f = 0, rw [← hf2, ← hg2, hf, leading_coeff_zero, zero_add], exact ⟨g, hg1, rfl⟩,
    by_cases hg : g = 0, rw [← hf2, ← hg2, hg, leading_coeff_zero, add_zero], exact ⟨f, hf1, rfl⟩,
    cases le_total (nat_degree f) (nat_degree g) with hd hd, -- can't get WLOG to work
    { refine ⟨f * X ^ (nat_degree g - nat_degree f) + g,
        I.add_mem (I.mul_mem_right hf1) hg1, _⟩,
      have := leading_term_aux hd hf hg (by rwa [hf2, hg2]),
      rwa [hf2, hg2] at this },
    { refine ⟨g * X ^ (nat_degree g - nat_degree f) + f,
        I.add_mem (I.mul_mem_right hg1) hf1, _⟩,
      have := leading_term_aux hd hg hf (by rwa [hf2, hg2, add_comm]),
      rwa [hf2, hg2] at this }
  end-/,
  smul := λ c a ⟨f, hf1, hf2⟩, begin
    by_cases hcr : c • a = 0, rw hcr, exact ⟨0, I.zero_mem, rfl⟩,
    refine ⟨C c * f, I.mul_mem_left hf1, _⟩,
    have : leading_coeff (C c) * leading_coeff f ≠ 0,
    { rwa [leading_coeff_C, hf2, ← smul_eq_mul] },
    rw [leading_coeff_mul' this, leading_coeff_C, hf2, smul_eq_mul]
  end }

[Kenny Lau]

@Mario Carneiro why does this time out?

[Mario Carneiro]

polynomials have had problems with long elaboration in the past

[Mario Carneiro]

check that it isn't doing any crazy typeclass searches?

[Kenny Lau]

it's searching for has_one nat and has_add nat like a billion times

[Mario Carneiro]

still profiling (slow business, of course) but it looks like the second block takes much longer than the first

[Kenny Lau]

oh, thanks

[Kenny Lau]

@Kevin Buzzard should I push what I have in my kmb_hilbert_basis?

[Mario Carneiro]

it takes 3.5 seconds with the sorry in, which is bad but not that bad so I guess you are worried about the commented out bit

[Kenny Lau]

but why does polynomial have long elaboration time?

[Mario Carneiro]

If I replace the last rwa in the second block with rw, the final state is:

...
this : leading_coeff (g * X ^ (nat_degree f - nat_degree g) + f) = b + a
⊢ leading_coeff (g * X ^ (nat_degree g - nat_degree f) + f) = a + b

I'm not sure how assumption is supposed to close that

[Kenny Lau]

ah

[Mario Carneiro]

it's probably taking forever unfolding all the things to see if those are actually the same

[Kenny Lau]

should I add two submodules together?

[Kenny Lau]

import algebra.module

universes u v

variables {R : Type u} [ring R]
variables {M : Type v} [add_comm_group M] [module R M]

instance submodule.has_add' : has_add (submodule R M) :=
⟨λ N₁ N₂, {
  carrier := { z | ∃ (x ∈ N₁) (y ∈ N₂), x + y = z },
  zero := ⟨0, N₁.zero_mem, 0, N₂.zero_mem, add_zero _⟩,
  add := λ z₁ z₂ ⟨x₁, hx₁, y₁, hy₁, hz₁⟩ ⟨x₂, hx₂, y₂, hy₂, hz₂⟩,
    ⟨x₁ + x₂, N₁.add_mem hx₁ hx₂, y₁ + y₂, N₂.add_mem hy₁ hy₂,
    by rw [← hz₁, ← hz₂, add_assoc, add_left_comm x₂, ← add_assoc]⟩,
  smul := λ c z ⟨x, hx, y, hy, hz⟩,
    ⟨c • x, N₁.smul_mem c hx, c • y, N₂.smul_mem c hy,
    by rw [← hz, smul_add]⟩ }⟩

[Mario Carneiro]

isn't this \sup?

[Kenny Lau]

oh

[Kenny Lau]

lol

[Mario Carneiro]

I realize that ring theorists prefer the notations $A + B$ and $A\cap B$ to $A\vee B$ and $A\wedge B$, but I think we should go for more notational uniformity

[Kenny Lau]

oh, coeff_is_linear uses is_linear_map, should I refactor that? @Mario Carneiro

[Kenny Lau]

def map_mk (I J : ideal α) : ideal I.quotient :=
{ carrier := mk I '' J,
  zero := ⟨0, J.zero_mem, rfl⟩,
  add := by rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩;
    exact ⟨x + y, J.add_mem hx hy, rfl⟩,
  smul := by rintro ⟨c⟩ _ ⟨x, hx, rfl⟩;
    exact ⟨c * x, J.mul_mem_left hx, rfl⟩ }

I think we can generalize this @Mario Carneiro

[Mario Carneiro]

to what?

[Mario Carneiro]

yes on coeff btw, you may need a second function though

[Kenny Lau]

@Mario Carneiro and how far away are we from the refactoring?

[Mario Carneiro]

plan is to finish it today; I am currently rejiggering some stuff with is_unit and nonunits prompted by some of Rob's applications

[Kenny Lau]

are you working on a separate branch or a private repo or something? i.e. should I just push to that branch?

[Mario Carneiro]

I'm working locally, feel free to keep committing to the module branch and I'll merge when I push

[Kenny Lau]

do you want to push your work to the community branches?

[Kevin Buzzard]

Kenny and I are just chatting on Skype

[Kevin Buzzard]

For Hilbert basis

[Kevin Buzzard]

one perhaps needs that there's some inclusion of lattices -- if R -> S is a ring hom and M is an S-module

[Kevin Buzzard]

then there's an order preserving injection from the lattice of sub-S-modules to the lattice of sub-R-modules

[Mario Carneiro]

okay, it's broken tho

[Kevin Buzzard]

A sub-R-module is just a sub-f(R)-module where f(R) is the subring of S

[Kevin Buzzard]

If R -> S is an injection with M an S-module then there's an injection from the sub-S-modules to the sub-R-modules

[Kevin Buzzard]

If R -> S is a surjection and M is an R-module then the submodule of M consisting of stuff which is annihiliated by the kernel of R->S is an S-module

[Kevin Buzzard]

and that way you get an injection from sub-S-modules to sub-R-modules

[Kenny Lau]

import data.polynomial

universe u

variables {R : Type u} [comm_ring R] [decidable_eq R]
variable (I : ideal (polynomial R))

def ideal.of_polynomial : submodule R (polynomial R) :=
{ carrier := (@submodule.carrier (polynomial R) (polynomial R) _ _ ring.to_module I : set (polynomial R)),
  zero := sorry, add := sorry, smul := sorry }

def ideal.of_polynomial' : submodule R (polynomial R) :=
{ carrier := (I.carrier : set (polynomial R)), -- doesn't work
  zero := sorry, add := sorry, smul := sorry }

@Mario Carneiro

[Mario Carneiro]

it's probably guessing the wrong scalar ring here

[Kevin Buzzard]

I thought it never had to guess anything nowadays?

[Mario Carneiro]

that's the next thing on the list after the module refactor

[Kevin Buzzard]

There's a _list_??

[Johan Commelin]

I feel there is a need for module refactor 2.0 :rolling_on_the_floor_laughing:

[Kevin Buzzard]

I never realised modules were so hard :-)

[Kenny Lau]

yeah that's 'coz you're a mathematician

[Mario Carneiro]

the list is my todo list, and it's on the list because people want modules to have multiple scalar rings

[Kevin Buzzard]

I am just trying to formalise various standard results in undergraduate algebra like Hilbert basis and reporting back on what mathematicians use

[Mario Carneiro]

@Kenny Lau @Johannes Hölzl The final draft of the module refactor is pushed

[Kenny Lau]

so... coeff is linear?

[Mario Carneiro]

it is now

[Kenny Lau]

thanks

[Kevin Buzzard]

So how do I make an S-module into an R-module if I have a ring hom $f : R \to S$?

[Kevin Buzzard]

thanks too

[Mario Carneiro]

Maybe there should be a way to put chosen ring homs in the typeclass infrastructure?

[Mario Carneiro]

Otherwise you just have to introduce it locally every time

[Mario Carneiro]

I assume you aren't asking how to define the R-module structure, that's not difficult at all

[Johan Commelin]

Maybe there should be a way to put chosen ring homs in the typeclass infrastructure?

I think we could also try using a structure algebra.

[Kevin Buzzard]

I assume you aren't asking how to define the R-module structure, that's not difficult at all

Right -- I'm asking for the idiomatic way to do it.

[Johannes Hölzl]

@Mario Carneiro why is it now a mixing, i.e. why is the group structure not part of modules anymore?

[Mario Carneiro]

Because the parent coercion module R M => add_comm_group M was causing much of the module typeclass issues

[Mario Carneiro]

plus if R becomes not an out_param then it won't even work

[Johannes Hölzl]

the module PR looks very good to me

[Johan Commelin]

It's merged :tada: :thumbs_up: :octopus:

[Johannes Hölzl]

COMMIT 1000

[Neil Strickland]

Bases should definitely be maps or lists. Some treatments of finite-dimensional linear algebra purport to use subsets, but they are almost always wrong if read literally, and would require fiddly side-conditions to make them right. Also, to talk about the standard algorithms you need efficient translation between bases and matrices, which becomes very awkward if you use subsets.

[Johan Commelin]

It isn't too hard to convert between a subset and a map. But maybe there should be a bit more API for this. Is there something specific that you are missing?

[Johan Commelin]

Matrices are currently indexed by fintypes (not necessarily ordered).

[Kenny Lau]

... is this related to the previous discussion?

[Neil Strickland]

I think not, sorry. Zulip sometimes gets in a funny state where it shows me very old posts mixed in with new ones, and I was accidentally replying to one of those. I am not quite sure what is going on with that.