Substructures and quotients in the `Algebra.*` hierarchy

[jamesmckinna]

The recent discussion in issue #1888 concerning the correct definition of Module drew my attention to the (almost?) complete (?) lack of any treatment of algebraic substructures, and the corresponding notions of 'things-which-give-rise-to-quotients':

• [ ] submonoid of a monoid;
• [ ] (normal) subgroup of a group;
• [ ] (left- and right-) ideal of a (non-commutative) ring;
• [ ] others? (eg do we care about submagmas? subsemirings etc.)

together with the associated 'free' things, viz.

• [ ] the submonoid generated by a subset;
• [ ] the subgroup generated by ...;
• [ ] the ideal generated by...;
• [ ] the terminal ('zero'?) (sub)object as the free thing on the empty type of generators...; EDITED apologies for my ignorance of Algebra.Construct.Zero which does define these (but none of the associated homomorphisms); see also PR #1902
• [ ] etc.

So this is (the beginnings of) a shopping list for the above, and some proposals for how to represent them.

A left- (resp. right-) ideal of a Ring R with Carrier given by A should be given by:

• a left- (resp. right-) R-module, with carrier type I for representing the subset in question;
• an injective map h : I -> A which is a left- (resp. right-) R-module homomorphism

TODO:

• work out the details! (eg: injective map or monomorphism? are they same for Setoids? etc. plus: level issues?)
• related matters: quotients, plus short/long exact sequences to characterise things?
• what else?

[JacquesCarette]

On the 'what else', Yasmine Sharoda's PhD Thesis has a nice list of things that are well-enough understood that our original plan was to generate them all. Eventually our code generated fewer of these (in Agda and in Lean). She mined a lot of universal algebra texts to find the most common constructions we should be looking at.

There's a lot of work to be still to be done to actually come up with a good shopping list, and even more work to find good definitions to actually use. The naive definitions in undergraduate textbooks tend to be flawed, and indeed one needs to look at category theory to find stable patterns (as already listed: terminal objects, initial objects, free objects -- but there are lots of very useful variations).

Being systematic 'by hand' would involve thousands of person-hours of work, and an unclear payoff. Having said that, clearly some of those constructions should be in stdlib. I'm not even quite sure how to approximate a decent middle ground!

[jamesmckinna]

Jacques, many thanks again for these pointers; this work deserves to be better known.

[jamesmckinna]

@JacquesCarette , replying to your comment on #1898 here (because the reply at least belongs here, i think):

where do you get that

is something well worth unpacking... ;-) if only towards the TODOs above...

I reasoned as follows ("we will study those things which, from time to time, arise as topics of interest"):

• the notion of 'subset' is suspect, constructively, esp. considered in (level-raising) Pred form; the predicative Fam/enumerated form as a function h : I -> A is (?) better behaved, and moreover cleanly separates, as a type, the 'elements' of the subset I;
• the derived notion of 'membership' is then nicely captured by a ∈ₕ I = ∃[ i ∈ I ] a ≈ h i;
• injectivity of h is then a way of enforcing "yes, it is a subset", in the usual 'subset = mono' arrow-theoretic style, but might in fact be optional (?);
• when considering 'least ... such that...', but also the simpler algebra such as intersections etc. you then get the additional wiggle-room to choose the representing type, given some underlying function from I into A which picks out the generators, together with the image of those generators:
  • for submagmas, take non-empty lists of I, with generators injected via singleton lists; the binary operation is _++_; _≈_ is pointwise equality;
  • for submonoids, take lists of I, with h [] = 0 (in fact: h is the unique fold over _*_), ditto. for generators; ditto the operation and book equality;
  • for commutative monoids, the same as above, but with _≈_ given by permutation;
  • for ideals, lists of (A × I), with injection of generators given by [(1# , i)] (the A component is there to absorb closure under multiplication in A);
  • etc.

Once/If you accept such definitions, then the injection from I to A, in the case of ideals, needs to be (all, and only) the canonical homomorphism of A-modules extending h on generators (the proof that the generating types above do indeed admit the correct algebraic operations is part of the work that would need doing anyway, and amounts to the 'undergraduate textbook' exercises of the form "show that a subset such that ... forms an ideal" etc.)

Now, I think I would have been thinking along those lines even before the work on frex, but I'm more and more convinced (cf. the reengineering of Tactic.RingSolver etc.) by that work, that the ability to choose a distinct representation of (the underlying type of) a subset of an algebra (or related gadgets such as frexes) is crucial to making computationally, cognitively, and even mathematically, efficient definitions.

[jamesmckinna]

[moved from #1898] But your link to 'rings = monoid objects in (Ab , _⊗_ , I)' makes me wonder if the definition I gave above is in fact necessary and sufficient (I hope so!).

As for sieves, I'll wait until we have a decent account of Setoid-based rings, ideals and modules, before attempting any formalisation of EGA or SGA ;-)

But for sure, local rings (and Nagata's construction) are baby steps on the way to such things...

[jamesmckinna]

So, your comment about

a solid source we could rely on...

I think I would answer with Atiyah and MacDonald, Commutative Algebra (Addison-Wesley-Longman, 1969), Chapter 2 on "Modules":

• p.17 example 1, "an ideal a of A is an A-module";
• p.22 "Exact Sequences", equations (1), (2), (3) characterising injective, surjective, and quotient-by-ideal-included-in-A module homomorphisms by the associated (short) exact sequences.

So, perhaps by what may seem somewhat baroque revisionism, motivated by the above (to my mind) representational gain, my thinking is to 'turn a property into a definition'...

... my experience being, that this is something we habitually do in the course of the general programme of the explicitation of mathematics in theorem provers. Perhaps, even, of doing mathematics in general.

[JacquesCarette]

So I was going to reply, unhelpfully, that a textbook written in the classical style, even if by spectacular scholars, might not give quite the right definition -- mathematicians tend to expose things post-inlining of many definitions instead of generically. Then I remembered that right here in my office, I have a wonderful textbook "Post-Modern Algebra", where they redo Algebra from the point of view of our modern understanding instead of the usual socio-historical point of view.

It proceeds by defining the concept of a 'sink' for a semigroup as being a subset that is closed by multiplication under all elements of the semigroup. i.e. K is a sink in semigroup S if forall k:K s:S, ks : K and sk : K. Then a non-unital subring K of a ring S is an ideal if it is a sink in the semigroup (induced by) S.

In that book, modules are not introduced until a couple of sections later.

[jamesmckinna]

Interesting reference. Will try to follow-up when I (next) have time to read! Meanwhile, I'd be happy on a first PR to commit content on ideals and submodules, and 'work backwards' to the weaker structures later (assuming that's even a plausible way of working with the existing towers of abstractions.

Regarding the technical details of ideals and submodules, some pen-and-paper sketching suggests to me that the Fam-approach applies equally to either (or both), with the advantages I sketched regarding choice of representing/indexing type I; at least as far as (direct) sums (ideals; submodules) and (direct) products (submodules) go; intersections of ideals/submodules seems to require to use the appropriate subset type underlying the carrier of the algebra as indexing type, with projection as enumerator h. In each case, there is the multiplicative closure condition to check, but it seems to go through without difficulty. So perhaps exact sequences can wait for another time... ;-)

[JacquesCarette]

This reminds me that I really have to get the whole Fam v Pow approach sunk into my brain much more deeply. Right now, this requires active thinking, while it ought to be available to me at a much deeper level.

[jamesmckinna]

Another one to punt until after v2.0, I think ;-)