Zulip Chat Archive

Stream: general

Topic: module refactoring


view this post on Zulip Mario Carneiro (Sep 21 2018 at 06:31):

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.

view this post on Zulip Johan Commelin (Sep 21 2018 at 06:33):

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

view this post on Zulip Mario Carneiro (Sep 21 2018 at 06:34):

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

view this post on Zulip Mario Carneiro (Sep 21 2018 at 06:36):

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

view this post on Zulip Mario Carneiro (Sep 21 2018 at 06:38):

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

view this post on Zulip Kenny Lau (Sep 21 2018 at 06:42):

but it's the same...

view this post on Zulip Johan Commelin (Sep 21 2018 at 06:43):

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

view this post on Zulip Johannes Hölzl (Sep 21 2018 at 08:03):

this is really nice!

view this post on Zulip Patrick Massot (Sep 21 2018 at 08:21):

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

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 10:51):

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?

view this post on Zulip Reid Barton (Sep 21 2018 at 10:56):

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

view this post on Zulip Kenny Lau (Sep 21 2018 at 10:57):

how about product or coproduct as a bifunctor?

view this post on Zulip Mario Carneiro (Sep 21 2018 at 16:21):

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

view this post on Zulip Mario Carneiro (Sep 21 2018 at 16:22):

@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.)

view this post on Zulip Johannes Hölzl (Sep 21 2018 at 16:26):

@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

view this post on Zulip Mario Carneiro (Sep 21 2018 at 16:39):

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

view this post on Zulip Johannes Hölzl (Sep 21 2018 at 16:45):

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.

view this post on Zulip Mario Carneiro (Sep 21 2018 at 16:46):

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

view this post on Zulip Mario Carneiro (Sep 21 2018 at 16:47):

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

view this post on Zulip Mario Carneiro (Sep 21 2018 at 16:49):

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

view this post on Zulip Patrick Massot (Sep 21 2018 at 16:58):

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

view this post on Zulip Chris Hughes (Sep 21 2018 at 17:05):

Is it worth bundling ideals and subgroups as well?

view this post on Zulip Johannes Hölzl (Sep 21 2018 at 17:12):

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

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 17:36):

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.

view this post on Zulip Chris Hughes (Sep 21 2018 at 17:43):

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

view this post on Zulip Mario Carneiro (Sep 21 2018 at 18:44):

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.

view this post on Zulip Mario Carneiro (Sep 21 2018 at 18:45):

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

view this post on Zulip Johan Commelin (Sep 21 2018 at 20:38):

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?

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 23:40):

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.

view this post on Zulip Mario Carneiro (Sep 22 2018 at 00:26):

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)

view this post on Zulip Mario Carneiro (Sep 22 2018 at 00:27):

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

view this post on Zulip Mario Carneiro (Sep 22 2018 at 00:33):

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

view this post on Zulip Mario Carneiro (Sep 27 2018 at 23:46):

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.)

view this post on Zulip Reid Barton (Sep 27 2018 at 23:59):

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.

view this post on Zulip Reid Barton (Sep 28 2018 at 00:00):

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!

view this post on Zulip Reid Barton (Sep 28 2018 at 00:01):

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

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:01):

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

view this post on Zulip Reid Barton (Sep 28 2018 at 00:02):

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

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:02):

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

view this post on Zulip Reid Barton (Sep 28 2018 at 00:02):

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

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:03):

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

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:04):

(bases over the zero ring are weird)

view this post on Zulip Reid Barton (Sep 28 2018 at 00:05):

Hmm... yes

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:05):

speaking of which... unit should be a ring

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:06):

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

view this post on Zulip Reid Barton (Sep 28 2018 at 00:08):

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:MiIRB\colon M \to \oplus_{i\in I}R to a direct sum of copies of the ring R, regarded as a module over itself.

view this post on Zulip Reid Barton (Sep 28 2018 at 00:09):

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

view this post on Zulip Reid Barton (Sep 28 2018 at 00:09):

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

view this post on Zulip Reid Barton (Sep 28 2018 at 00:15):

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

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:47):

so what does this say about linearly independent sets?

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:48):

I guess these should also be indexed

view this post on Zulip Johan Commelin (Sep 28 2018 at 01:31):

speaking of which... unit should be a ring

instance : comm_ring unit := by tidy

view this post on Zulip Johan Commelin (Sep 28 2018 at 01:34):

Good luck golfing that...

view this post on Zulip Johan Commelin (Sep 28 2018 at 01:38):

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

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 07:48):

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).

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:50):

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...

view this post on Zulip Mario Carneiro (Oct 04 2018 at 14:41):

I was actually thinking about going the other way :)

view this post on Zulip Mario Carneiro (Oct 04 2018 at 14:42):

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

view this post on Zulip Mario Carneiro (Oct 04 2018 at 14:43):

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

view this post on Zulip Mario Carneiro (Oct 04 2018 at 14:43):

I agree some uniformity of naming would be a good thing

view this post on Zulip Johan Commelin (Oct 04 2018 at 14:49):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 03:45):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 03:46):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 03:46):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 03:53):

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

view this post on Zulip Scott Morrison (Oct 08 2018 at 04:02):

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).

view this post on Zulip Scott Morrison (Oct 08 2018 at 04:03):

I'm not sure it's particularly useful.

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:03):

yeah I was thinking the ring part might end up contravariant

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:03):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:17):

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?

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:18):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:19):

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?

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:19):

Sure.

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:19):

That's a fibered category

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:19):

And this one is one of the first examples

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:21):

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?)

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:21):

Yes, I do.

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:21):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:22):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:22):

Or only ideals in comm_rings?

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:23):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:23):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:23):

Is that what you were looking for?

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:23):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:24):

R' \otimes_R M

what is this

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:24):

Tensor product

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:24):

turning M into an R'-module

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:24):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:24):

Yes

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:25):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:25):

Which one?

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:25):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:25):

You mean the forgetful functor?

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:25):

From R'-mod to R-mod?

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:26):

It's not forgetful, right?

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:26):

Not really

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:26):

The hom could be anything

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:26):

I still think of it as "forgetting"

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:26):

We have R is an R-mod

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:27):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:27):

I don't follow

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:27):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:27):

what forget instance?

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:27):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:27):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:28):

I want your instance to be broken into 2 steps.

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:28):

what forget instance?

The "forgetful" functor instance

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:28):

every R'-mod is an R-mod

This one requires an explicit ring hom input

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:29):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:29):

over R

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:29):

ah, we don't have anything like that yet

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:30):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:32):

Ah - multivariate polynomials are the free assoc algebra

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:33):

The ones we have are also commutative

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:34):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:35):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:35):

... + free monoid construction which we already have

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:35):

So, could we have f^* M'?

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:36):

I think so, what does that mean?

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:36):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:36):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 04:37):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:37):

Right, and it is adjoint to tensoring.

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:37):

Which is covariant

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:37):

no, that's bullcrap

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:37):

I'm brainfarting

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:38):

tensor is adjoint to hom

view this post on Zulip Johan Commelin (Oct 08 2018 at 04:38):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 06:40):

@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

view this post on Zulip Kenny Lau (Oct 08 2018 at 06:41):

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

view this post on Zulip Kenny Lau (Oct 08 2018 at 06:42):

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)

view this post on Zulip Kenny Lau (Oct 08 2018 at 06:43):

2018-10-08.png

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:45):

yeah, okay that's a better idea

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:45):

just close the resulting set under ideal operations

view this post on Zulip Johan Commelin (Oct 08 2018 at 06:46):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:46):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:47):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 06:47):

Great!

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:47):

it's already behind schedule too much

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:48):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:48):

foremost of which is the multiple scalar field thing

view this post on Zulip Johan Commelin (Oct 08 2018 at 06:48):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:48):

I'm actually working on that ATM

view this post on Zulip Johan Commelin (Oct 08 2018 at 06:49):

Wonderful! Thanks for doing that!

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 07:15):

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:ABf:A\to B is a map of rings and if GG is an AA-module and FF a BB-module, an ff-map GFG\to F is simply an AA-module homomorphism from GG to FF, and the observation is that such maps naturally biject with the BB-module homomorphisms from GABG\otimes_AB to FF. I think this is different to what Scott suggests -- he went the other way.

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 07:20):

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

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

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 07:26):

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.

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:27):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:27):

Basically it abstracts ff-maps

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 07:33):

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 ff-map is a construction which depends on a map ff 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:RRf:R\to R' there are then adjoint functors (Rmod)(Rmod)(R-mod)\to(R'-mod) and (Rmod)(Rmod)(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.

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:34):

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.

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:35):

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

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 07:35):

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

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 07:36):

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.

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:36):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:38):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:38):

If you want an ideal of B, yes.

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:39):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:39):

Is this a thing we can currently do?

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:39):

What?

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:39):

tensoring like that

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:39):

I guess almost

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:40):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:40):

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

view this post on Zulip Kenny Lau (Oct 08 2018 at 07:49):

I don’t think I did.

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 08:07):

Oh I see. The issue is that if MM is an AA-module and BB is an AA-algebra (and hence an AA-module) then MABM\otimes_AB is not just an AA-module but a BB-module.

view this post on Zulip Johan Commelin (Oct 08 2018 at 08:08):

Right, we don't have something like that atm

view this post on Zulip Johan Commelin (Oct 08 2018 at 08:09):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 08:10):

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.

view this post on Zulip Patrick Massot (Oct 08 2018 at 18:55):

foremost of which is the multiple scalar field thing

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

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:44):

How's it going? @Mario Carneiro

view this post on Zulip Mario Carneiro (Oct 23 2018 at 00:22):

waiting on my school work to decrease in intensity

view this post on Zulip Mario Carneiro (Oct 23 2018 at 00:22):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 09:59):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 09:59):

@Mario Carneiro is there anything we can help with?

view this post on Zulip Mario Carneiro (Nov 01 2018 at 10:09):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 10:09):

what can we do?

view this post on Zulip Kenny Lau (Nov 01 2018 at 10:09):

should I fix the errors?

view this post on Zulip Mario Carneiro (Nov 01 2018 at 10:09):

go in there and make the red squiggles go away

view this post on Zulip Kenny Lau (Nov 01 2018 at 10:10):

roger that

view this post on Zulip Mario Carneiro (Nov 01 2018 at 10:12):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 12:44):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 12:44):

I'll just leave those untouched

view this post on Zulip Mario Carneiro (Nov 01 2018 at 12:46):

like what? I think all deleted files have equivalents

view this post on Zulip Kenny Lau (Nov 01 2018 at 12:47):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 12:48):

and also this:

@[simp] theorem Union_set_of_directed {ι} ( : nonempty ι)
  (S : ι  submodule α β)
  (H :  i j,  k, S i  S k  S j  S k) :
  ((supr S : submodule α β) : set β) =  i, S i :=

view this post on Zulip Mario Carneiro (Nov 01 2018 at 12:48):

prime ideals are still there

view this post on Zulip Mario Carneiro (Nov 01 2018 at 12:49):

search for that, it moved somewhere else

view this post on Zulip Mario Carneiro (Nov 01 2018 at 12:49):

I think it is Union_coe now

view this post on Zulip Kenny Lau (Nov 01 2018 at 12:49):

prime_ideal doesn't give me anything

view this post on Zulip Kenny Lau (Nov 01 2018 at 12:49):

and i wouldn't search for prime

view this post on Zulip Mario Carneiro (Nov 01 2018 at 12:50):

the trivial ideal is bottom

view this post on Zulip Kenny Lau (Nov 01 2018 at 12:50):

ok I searched for prime and I found it

view this post on Zulip Kenny Lau (Nov 01 2018 at 14:32):

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

view this post on Zulip Mario Carneiro (Nov 01 2018 at 15:25):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 18:54):

@Mario Carneiro I've pushed a partial fix

view this post on Zulip Kenny Lau (Nov 01 2018 at 18:54):

I'll see what more I can do

view this post on Zulip Kenny Lau (Nov 02 2018 at 09:54):

@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 α))

view this post on Zulip Kenny Lau (Nov 02 2018 at 09:54):

what should I do?

view this post on Zulip Kenny Lau (Nov 02 2018 at 12:32):

@Mario Carneiro ideal.quotient.eq is missing

view this post on Zulip Kenny Lau (Nov 02 2018 at 12:33):

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

view this post on Zulip Kenny Lau (Nov 02 2018 at 16:17):

Successfully reduced to 4 errors. Pushed.

view this post on Zulip Mario Carneiro (Nov 02 2018 at 19:22):

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

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:06):

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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:06):

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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:06):

so if you find it elsewhere you should use that

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:06):

so it's the latter?

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:06):

ok

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:07):

is_principal_ideal should be a property of S : ideal

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:10):

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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:11):

what does quotient_ring look like now?

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:12):

it looks like ideal.quotient now

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:12):

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

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:13):

but not ideal.quotient.eq

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:13):

oh sure, you can state ideal.quotient.eq

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:13):

ok

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:13):

it's just a defeq copy paste job

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:13):

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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:13):

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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:14):

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

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:16):

I agree (with the latter statement)

view this post on Zulip Kenny Lau (Nov 02 2018 at 21:38):

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

view this post on Zulip Kenny Lau (Nov 02 2018 at 21:38):

@Mario Carneiro can I change this to use dvd?

view this post on Zulip Mario Carneiro (Nov 02 2018 at 21:39):

maybe make another theorem

view this post on Zulip Kenny Lau (Nov 02 2018 at 21:40):

but nobody uses that theorem

view this post on Zulip Kenny Lau (Nov 02 2018 at 21:40):

you added that theorem yourself

view this post on Zulip Kenny Lau (Nov 02 2018 at 22:04):

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

Should this be an instance?

view this post on Zulip Mario Carneiro (Nov 02 2018 at 22:11):

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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 22:13):

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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 22:14):

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

view this post on Zulip Kevin Buzzard (Nov 02 2018 at 23:27):

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

view this post on Zulip Kenny Lau (Nov 02 2018 at 23:29):

@Kevin Buzzard wrong thread?

view this post on Zulip Kevin Buzzard (Nov 02 2018 at 23:30):

Isn't that a predicate which is a class?

view this post on Zulip Kenny Lau (Nov 02 2018 at 23:30):

oh well this is going off track

view this post on Zulip Chris Hughes (Nov 02 2018 at 23:33):

Why is it a class?

view this post on Zulip Mario Carneiro (Nov 02 2018 at 23:37):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:03):

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).

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:03):

Ha, this was my secret plan all along

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:04):

I think one would prefer transparency

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:04):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:04):

and can write a nice summary for us

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:04):

lol

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:05):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:06):

like if you don't care about semimodules

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:07):

I'm sure Kevin doesn't

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:07):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:08):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:08):

I really want linear_map to be the primary one

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:08):

oh, I may have done that already

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:08):

not entirely

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:08):

shoot, I have an unsaved file in vscode

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:09):

lol

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:11):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:11):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:15):

oh, right

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:27):

@Mario Carneiro are you going to push your file?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:31):

oh wait, looks like I already pushed most of it

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:31):

you already had the important stuff

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:33):

but tensor product still depends on is_linear_map right?

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:36):

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) }

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:36):

I don't think anyone wants to see this

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:39):

what is your objection exactly?

view this post on Zulip Kenny Lau (Nov 03 2018 at 00:41):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 01:02):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 01:02):

lift.ext should take linear maps as input

view this post on Zulip Mario Carneiro (Nov 03 2018 at 01:04):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 01:05):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 01:07):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 01:08):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 02:35):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 02:37):

do you think I should change is_bilinear_map to bilinear_map?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 02:40):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 02:40):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 02:42):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 02:45):

yes

view this post on Zulip Kenny Lau (Nov 03 2018 at 02:45):

they're even a module

view this post on Zulip Kenny Lau (Nov 03 2018 at 02:46):

they're as nice as linear maps

view this post on Zulip Kenny Lau (Nov 03 2018 at 02:46):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:02):

well okay then

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:03):

I think bilinear_map still needs to reference is_linear_map though

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:03):

@[reducible] def bilinear_map := M  N  P

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:03):

how about this

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:03):

oh! does that work?

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:03):

I'm experimenting with it now

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:03):

is Mod(R) a CCC?

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:04):

CCC?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:04):

cartesian closed category

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:04):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:04):

yes

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:05):

actually I don't know

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:05):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:05):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:05):

that looks a lot like the universal property of the exponential

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:06):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:37):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:37):

looking good

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:41):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:41):

maybe it requires the tensor product though

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:42):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:45):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:45):

and if comp was also linear.. :P

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:46):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:47):

but that would be too category-theoretical for our purposes

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:47):

I mean with the categories unfolded away

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:48):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:48):

we just need the right building blocks to get everything else

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:49):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:49):

yes

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:49):

but abstraction isn't a linear map?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:49):

That's apply

view this post on Zulip Kenny Lau (Nov 03 2018 at 03:50):

so what's the conclusion?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:50):

er, no - abstraction is the UMP of apply

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:51):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:51):

so you get a "lambda" like operator

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:52):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 03:53):

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

view this post on Zulip Johan Commelin (Nov 03 2018 at 07:25):

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

view this post on Zulip Kevin Buzzard (Nov 03 2018 at 08:14):

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?

view this post on Zulip Kenny Lau (Nov 03 2018 at 11:39):

Fixed

view this post on Zulip Kenny Lau (Nov 03 2018 at 11:46):

@Mario Carneiro what's the next step?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:47):

is it compiling now?

view this post on Zulip Kenny Lau (Nov 03 2018 at 11:47):

yes

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:48):

sweet

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:49):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:49):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 11:50):

nice

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:50):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:51):

the CCC laws seem like a good place to start

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:51):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:52):

an equiv, even

view this post on Zulip Kenny Lau (Nov 03 2018 at 11:53):

ok

view this post on Zulip Kenny Lau (Nov 03 2018 at 11:54):

I don't think that's true

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:01):

put l everywhere

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:01):

that's homs in the category

view this post on Zulip Kenny Lau (Nov 03 2018 at 12:02):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 12:06):

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)
````

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:18):

yes

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:19):

linear equiv I assume

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:19):

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

view this post on Zulip Johan Commelin (Nov 03 2018 at 12:19):

canonical linear equiv, even... :grinning_face_with_smiling_eyes:

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:20):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:21):

it's trivial with that equiv though

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:21):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:21):

like apply and curry

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:22):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:22):

Is it also the coproduct?

view this post on Zulip Johan Commelin (Nov 03 2018 at 12:23):

Nope

view this post on Zulip Johan Commelin (Nov 03 2018 at 12:23):

Coproduct is the direct sum, which is also the product

view this post on Zulip Johan Commelin (Nov 03 2018 at 12:24):

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

view this post on Zulip Kevin Buzzard (Nov 03 2018 at 12:25):

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

view this post on Zulip Kevin Buzzard (Nov 03 2018 at 12:26):

Other than the zero map

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:26):

wait what?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:27):

this is a funny product indeed

view this post on Zulip Kenny Lau (Nov 03 2018 at 12:42):

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)

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:01):

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

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:07):

Are you listing the things that you are currently proving?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 13:26):

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

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:28):

Do we have dual?

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:29):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:29):

that's just M ->L R

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:30):

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

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:30):

Of course, but it is a useful concept.

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:30):

I'm probably missing some hypotheses...

view this post on Zulip Mario Carneiro (Nov 03 2018 at 13:30):

don't let truth get in the way of beauty

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:51):

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 })

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:51):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:51):

oh well

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:51):

what's the concrete version of your question?

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:52):

Flat ring homs

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:52):

@[reducible] def bilinear_map := M  N  P

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:52):

should we just remove bilinear_map entirely?

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:53):

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

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:53):

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

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:55):

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.

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:56):

what are the 25 other properties?

view this post on Zulip Kenny Lau (Nov 03 2018 at 13:58):

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

man my interface is really good

view this post on Zulip Johan Commelin (Nov 03 2018 at 13:58):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:01):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:02):

of course it is, it's a quotient

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:03):

well then why isn't this rfl:

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:06):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:06):

I guess that's why

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:06):

where'd that come from?

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:08):

the free group

view this post on Zulip Chris Hughes (Nov 03 2018 at 14:08):

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

I love proofs like this.

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:08):

free_abelian_group.lift also isn't rfl

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:09):

right

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:09):

it's zero_add as well

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:10):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:10):

is it free_group.to_group?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:11):

ah yes

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:12):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:12):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:14):

so it's all in list.prod

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:17):

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?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:17):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:19):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:19):

and how would one implement "expressions"?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:19):

expressions in the language of groups means trees

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:19):

you just have a symbol for one and inv and mul

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:20):

and the basis elements

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:20):

and you get trees

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:20):

and what do you mean by tree?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:20):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:21):

aha

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:21):

how would that help?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:21):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:22):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:22):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:22):

oh

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:22):

fair enough

view this post on Zulip Johan Commelin (Nov 03 2018 at 14:23):

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:

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:23):

lol

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:23):

sometimes it matters

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:24):

The reason quotient types exist is because of defeqs

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:24):

otherwise we would just use sets of sets

view this post on Zulip Johan Commelin (Nov 03 2018 at 14:25):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:25):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:26):

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

view this post on Zulip Johan Commelin (Nov 03 2018 at 14:26):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:27):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:28):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:28):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:28):

but it is nice to have for computational purposes

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:29):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:29):

ok

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:29):

but if it interests you, feel free

view this post on Zulip Johan Commelin (Nov 03 2018 at 14:30):

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

view this post on Zulip Johan Commelin (Nov 03 2018 at 14:30):

(or expanding the scope of this refactor)

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:31):

ok I pushed the tensor product

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:31):

@Mario Carneiro should we PR it now?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:32):

sure, that will give it more exposure

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:33):

more exposure to what?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:33):

people with ideas

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:34):

or who like to read about new things on github

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:34):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 14:35):

and when is it ready?

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:38):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 14:39):

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

view this post on Zulip Patrick Massot (Nov 03 2018 at 16:57):

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?

view this post on Zulip Kenny Lau (Nov 03 2018 at 16:58):

It could still change

view this post on Zulip Patrick Massot (Nov 03 2018 at 16:58):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 22:11):

@Mario Carneiro ok I pushed the refactored free_group.lean

view this post on Zulip Kenny Lau (Nov 03 2018 at 22:11):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 22:27):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 22:57):

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

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:21):

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

?

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:27):

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

-/

view this post on Zulip Chris Hughes (Nov 04 2018 at 18:30):

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

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:31):

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

view this post on Zulip Chris Hughes (Nov 04 2018 at 18:33):

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.

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:39):

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.

view this post on Zulip Chris Hughes (Nov 04 2018 at 18:39):

by haveI := _; exact _

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:40):

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

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:40):

no errors :D

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:40):

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

view this post on Zulip Chris Hughes (Nov 04 2018 at 18:41):

I think so.

view this post on Zulip Chris Hughes (Nov 04 2018 at 18:42):

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

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:46):

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.

view this post on Zulip Chris Hughes (Nov 04 2018 at 18:47):

I would wait until after module refactorign

view this post on Zulip Kenny Lau (Nov 04 2018 at 18:47):

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

view this post on Zulip Kenny Lau (Nov 04 2018 at 18:47):

no, this hasn’t been done

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:48):

I thought module refactoring had happened

view this post on Zulip Kenny Lau (Nov 04 2018 at 18:48):

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

view this post on Zulip Kenny Lau (Nov 04 2018 at 18:48):

and also you should use module.of_core

view this post on Zulip Kenny Lau (Nov 04 2018 at 18:48):

and also you should use module.of_core

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:48):

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

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:49):

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
}

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:53):

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?

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:55):

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

view this post on Zulip Kenny Lau (Nov 04 2018 at 18:55):

right

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:02):

    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,

view this post on Zulip Kenny Lau (Nov 04 2018 at 19:04):

i think you are missing two arguments

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:06):

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]

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:07):

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

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:16):

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
  }

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:18):

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?

view this post on Zulip Chris Hughes (Nov 04 2018 at 19:18):

Yes. What about erw

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:19):

I still seem to need the show for add_smul.

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:22):

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),

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:22):

longer than the tactic proof ;-)

view this post on Zulip Johan Commelin (Nov 04 2018 at 19:23):

It ought to be by tidy.

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:24):

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

view this post on Zulip Johan Commelin (Nov 04 2018 at 19:24):

Only if it is a simp-lemma

view this post on Zulip Johan Commelin (Nov 04 2018 at 19:25):

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

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 19:58):

Will this instance ever trigger?

view this post on Zulip Chris Hughes (Nov 04 2018 at 20:37):

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

view this post on Zulip Kenny Lau (Nov 04 2018 at 20:41):

maybe we should make ring_hom just like linear_map

view this post on Zulip David Michael Roberts (Nov 04 2018 at 21:16):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 06:21):

(deleted)

view this post on Zulip Kenny Lau (Nov 05 2018 at 06:21):

(deleted)

view this post on Zulip Mario Carneiro (Nov 05 2018 at 06:35):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 06:39):

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 }

view this post on Zulip Kenny Lau (Nov 05 2018 at 06:39):

@Mario Carneiro why does this time out?

view this post on Zulip Mario Carneiro (Nov 05 2018 at 06:41):

polynomials have had problems with long elaboration in the past

view this post on Zulip Mario Carneiro (Nov 05 2018 at 06:41):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 06:45):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 06:48):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 06:48):

oh, thanks

view this post on Zulip Kenny Lau (Nov 05 2018 at 06:49):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 06:49):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 06:51):

but why does polynomial have long elaboration time?

view this post on Zulip Mario Carneiro (Nov 05 2018 at 06:59):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 07:00):

ah

view this post on Zulip Mario Carneiro (Nov 05 2018 at 07:01):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 07:04):

should I add two submodules together?

view this post on Zulip Kenny Lau (Nov 05 2018 at 07:11):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 07:12):

isn't this \sup?

view this post on Zulip Kenny Lau (Nov 05 2018 at 07:12):

oh

view this post on Zulip Kenny Lau (Nov 05 2018 at 07:12):

lol

view this post on Zulip Mario Carneiro (Nov 05 2018 at 07:13):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 09:12):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 09:25):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 09:25):

to what?

view this post on Zulip Mario Carneiro (Nov 05 2018 at 09:26):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 09:50):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 09:52):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 10:07):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 10:08):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 10:09):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:09):

Kenny and I are just chatting on Skype

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:10):

For Hilbert basis

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:10):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:11):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 10:12):

okay, it's broken tho

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:12):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:13):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:14):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:15):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 10:40):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 10:41):

it's probably guessing the wrong scalar ring here

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:42):

I thought it never had to guess anything nowadays?

view this post on Zulip Mario Carneiro (Nov 05 2018 at 10:42):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:42):

There's a _list_??

view this post on Zulip Johan Commelin (Nov 05 2018 at 10:42):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:42):

I never realised modules were so hard :-)

view this post on Zulip Kenny Lau (Nov 05 2018 at 10:44):

yeah that's 'coz you're a mathematician

view this post on Zulip Mario Carneiro (Nov 05 2018 at 10:54):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 10:59):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 13:18):

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

view this post on Zulip Kenny Lau (Nov 05 2018 at 13:18):

so... coeff is linear?

view this post on Zulip Mario Carneiro (Nov 05 2018 at 13:23):

it is now

view this post on Zulip Kenny Lau (Nov 05 2018 at 13:25):

thanks

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 13:25):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 13:25):

thanks too

view this post on Zulip Mario Carneiro (Nov 05 2018 at 13:28):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 13:28):

Otherwise you just have to introduce it locally every time

view this post on Zulip Mario Carneiro (Nov 05 2018 at 13:29):

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

view this post on Zulip Johan Commelin (Nov 05 2018 at 13:30):

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.

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 13:34):

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.

view this post on Zulip Johannes Hölzl (Nov 05 2018 at 13:46):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 13:48):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 13:49):

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

view this post on Zulip Johannes Hölzl (Nov 05 2018 at 15:17):

the module PR looks very good to me

view this post on Zulip Johan Commelin (Nov 05 2018 at 15:59):

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

view this post on Zulip Johannes Hölzl (Nov 05 2018 at 15:59):

COMMIT 1000

view this post on Zulip Neil Strickland (Feb 01 2019 at 11:18):

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.

view this post on Zulip Johan Commelin (Feb 01 2019 at 11:21):

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?

view this post on Zulip Johan Commelin (Feb 01 2019 at 11:21):

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

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:26):

... is this related to the previous discussion?

view this post on Zulip Neil Strickland (Feb 01 2019 at 11:30):

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.


Last updated: May 06 2021 at 22:13 UTC