UniMath
Actions of monoids, groups, and rings
Summary:
- I define
hasinv, etc. as propositions expressing "this element has an (left/right) inverse under this binary operation". This is more granular than saying "this operation is (left/right) invertible". We might want to rephrase the latter definitions in terms of the former, but I wanted to get feedback before making those changes. - I define the submonoid of elements with inverses, and show that it is actually a group.
- I define the endomorphism monoid, automorphism group, and endomorphism ring (in an additive category), and define monoid (group) actions and ring actions as homomorphisms into these.
This PR might need a little reorganization (including the first bullet point above). Let me know where things should go!
I made a git error which caused the Travis build to be canceled. I'm going to close and re-open this to get another build started.
@benediktahrens Thanks for taking a look! Do you have feedback on whether I should rephrase islinv, isrinv, isrinvertible, etc. in terms of haslinv and the others I add in this PR?
My thinking is that isrinv,islinv, and isinv should be rephrased in terms of isrinvel, islinvel and isinvel, but I don't know about isinvertible, which is expressed in terms of a weak equivalence instead of paths (is that because the weak equivalence is more useful in some situations?).
On 12/06/2017 02:40 AM, Langston Barrett wrote:
@benediktahrens https://github.com/benediktahrens Thanks for taking a look! Do you have feedback on whether I should rephrase |islinv|, |isrinv|, |isrinvertible|, etc. in terms of |haslinv| and the others I add in this PR?
My thinking is that |isrinv|,|islinv|, and |isinv| should be rephrased in terms of |isrinvel|, |islinvel| and |isinvel|, but I don't know about |isinvertible|, which is expressed in terms of a weak equivalence instead of paths (is that because the weak equivalence is more useful in some situations?).
Reformulating isinvertible in terms of haslinv etc is a bad idea,
for the following reason:
The definition of hexists involves propositional truncation, which
impedes computation.
The truncation is necessary because a left (or right) inverse is not
unique in general.
However, a two-sided inverse is unique when it exists, so there is no need for a truncation to turn that into a proposition.
It is hence better to define two-sided inverses not using haslinv.
Does that make sense?
The PR does not currently compile, see, e.g., https://travis-ci.org/UniMath/UniMath/jobs/312201293 . Could you fix these errors, please?
@benediktahrens That does make sense, thank you for explaining. To summarize, I understand you to be saying: when something is not unique (e.g. a left/right inverse), we should use hexists, whereas when something is unique (e.g. a two-sided inverse), we should just use total2. Is that correct?
Also: I am still left wondering whether or not to rephrase isrinv,islinv, and isinv in terms of islinvel, isrinvel, and isinvel. I guess more generally, what would you like to see changed for this PR to be mergeable?
@benediktahrens Actually, I just realized that making hasinv into a sigma-type makes this whole construction fail. Then we can't define the subtype invertible_elements of a monoid, because having an inverse is no longer an hProp.
On 12/07/2017 08:18 PM, Langston Barrett wrote:
@benediktahrens Actually, I just realized that making
hasinvinto a sigma-type makes this whole construction fail. Then we can't define the subtypeinvertible_elementsof a monoid, because having an inverse is no longer anhProp.
I might be misunderstanding you, but:
in a monoid, you can show that for a given element, its inverse is unique.
That means that in a monoid, is_invertible a for some element a, is
a proposition. However, that requires a tiny proof - it is not obvious
from the definition.
But, the type of left-sided inverses of a fixed element is not unique. This is why one needs a truncation to obtain a proposition.
I think I understand better now what the issue is. I hadn't looked at the code properly.
There is the following definition:
Definition invertible_elements : hsubtype X :=
fun x => (hasinv x,, isaprophasinv x).
That definition is ok when X is a set or a type more generally.
But, when X is a monoid, then a different definition is better. Namely, in some sort of pseudocode:
Definition invertible_elements (X : monoid) : X -> UU :=
fun x => total2 (fun y => x * y = 1 \times y * x = 1).
Lemma isaprop_invertible_elements X (x : X) : isaprop (invertible_elements X x)
Proof.
< insert the well-known proof that in a monoid, an inverse is unique >
Qed.
Definition invertible_elements_hsubtype (X : monoid) : hsubtype X :=
fun x => <pair of the two above>
The advantage of this will be that the inverse is not under a truncation.
This looks good to me, modulo the changes already suggested above.
One minor comment: highly compressed identifiers like islinvel are difficult to parse, let alone to remember them for later use, or to find them as a user searching for the concept of “left inverse”, “left invertible” in the library. I would strongly prefer something like is_linv_el to this, and mildly prefer the even more verbose is_left_inverse_element. But a lot of existing identifiers in the library are similarly compressed, so I understand others may prefer keeping consistent with them.
Maintainers @benediktahrens , @DanGrayson : is there any standard guideline/preference on this, for new contributed code? Or are contributors equally free to use whatever conventions they like (and bikeshedding over it discouraged in reviews)?
@peterlefanulumsdaine See #687 and the issue Dan links to from there. I completely agree that such compressed names are not optimal, but any consistency would be preferable to none.
This is an important issue of style, for which we need a uniform solution, and it goes back to choices Vladimir made in 2010. He loved even such identifiers as coconustot.
@siddharthist : could you update this PR, please? There is currently a merge conflict in CT/.package/files.
I suggest we merge this PR and you think about naming conventions afterwards.
I've updated this and made it conform to the style guide, it should be ready for review.
We actually might want to define these in further generality: first define the categories corresponding to each monoid, group, and ring, and then define actions as functors. The reason is equivariant maps. The naive definition would look like the following:
Definition equivariant_map_mon {C : category} {M : monoid} {X Y : ob C}
(f : monaction M X) (g : monaction M Y) : UU :=
∑ h : X --> Y, h ∘ f = g ∘ h.
However, since h is a morphism in C, it can't be composed with f and g, which are functions, i.e. morphisms in type_precat. I don't immediately see a way around this issue, other than generalizing.
I've now proved an equivalence between monoids and categories with contractible object types, which allowed me to define actions as functors and equivariant maps as natural transformations.
I haven't established the same correspondence for groups and rings.
I've also fixed the merge conflict with master. Now, it really should be ready for review!
COQC UniMath/CategoryTheory/Actions.v
File "./UniMath/CategoryTheory/Actions.v", line 230, characters 55-58:
Error: The reference rng was not found in the current environment.
Command exited with non-zero status 1
0.39user 0.09system 0:00.49elapsed 99%CPU (0avgtext+0avgdata 356784maxresident)k
0inputs+64outputs (0major+11270minor)pagefaults 0swaps
build/CoqMakefile.make:645: recipe for target 'UniMath/CategoryTheory/Actions.vo' failed
make[1]: *** [UniMath/CategoryTheory/Actions.vo] Error 1
make[1]: Leaving directory '/UniMath'
Okay, it is finally building! I've expanded the results just a little more: I've proved the equivalence between functors between one-object categories and monoid homomorphisms.
@DanGrayson : you had asked for changes here. Have they been addressed?
I noticed that Domains_and_Fields defines a lot of similar ideas about elements with inverses. I've now upstreamed proofs of all the lemmas there to BinaryOperations, and a note that they just need to be replaced.
See https://travis-ci.org/UniMath/UniMath/jobs/456369958#L1661 for one compilation failure. It has to do with the addition of the symmetric associativity law to categories, I assume.
File "./UniMath/CategoryTheory/Categories.v", line 213, characters 12-40:
Error:
In environment
obj : UU
mor : obj → obj → UU
homsets : ∏ a b : obj, isaset (mor a b)
identity : ∏ i : obj, mor i i
compose : ∏ i j k : obj, mor i j → mor j k → mor i k
right : ∏ (i j : obj) (f : mor i j), compose i i j (identity i) f = f
left : ∏ (i j : obj) (f : mor i j), compose i j j f (identity j) = f
associativity :
∏ (a b c d : obj) (f : mor a b) (g : mor b c) (h : mor c d),
compose a b d f (compose b c d g h) = compose a c d (compose a b c f g) h
associativity' :
∏ (a b c d : obj) (f : mor a b) (g : mor b c) (h : mor c d),
compose a c d (compose a b c f g) h = compose a b d f (compose b c d g h)
The term "(right,, left),, associativity" has type
"∑
_ : (∏
(a
b : precategory_data_pair
I’ve updated this very old PR to build again (at least locally — hopefully the CI will agree). It has a lot of good material; almost all changes requested in reviews have been addressed, and as far as I can see, none of this material is obsoleted or duplicated by more recent contributions.
The one outstanding requested change is the “TODO” noting that there’s a treatment of inverses in Algebra.Domain_and_Fields that overlaps with the one in Algebra.BinaryOperations, which should certainly be unified. (The duplication is already present before this PR.) However, refactoring that will interact with a fair bit of material downstream (including another large PR in prep by a student of mine) so to avoid entanglement between large PR’s, I suggest leaving that refactor for a separate single-purpose PR, and merging this PR roughly as-is? I will open an issue for this point.
@peterlefanulumsdaine : Thanks for working on this! I have merged current master into this PR. I am in principle happy with merging this PR, in particular since it mostly adds code.