-
Notifications
You must be signed in to change notification settings - Fork 251
Open
Description
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 initial+terminal algebras #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 typeI
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
Setoid
s? etc. plus: level issues?) - related matters: quotients, plus short/long exact sequences to characterise things?
- what else?
Taneb