Quasigroups #1330
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| # Quasigroups | ||
|
|
||
| ```agda | ||
| module quasigroups where | ||
|
|
||
| open import quasigroups.loops public | ||
| open import quasigroups.quasigroups public | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,220 @@ | ||
| # Loops | ||
|
|
||
| ```agda | ||
| module quasigroups.loops where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import foundation.action-on-identifications-functions | ||
| open import foundation.conjunction | ||
| open import foundation.dependent-pair-types | ||
| open import foundation.equality-dependent-pair-types | ||
| open import foundation.identity-types | ||
| open import foundation.propositions | ||
| open import foundation.sets | ||
| open import foundation.transport-along-identifications | ||
| open import foundation.universe-levels | ||
|
|
||
| open import foundation-core.cartesian-product-types | ||
| open import foundation-core.contractible-types | ||
| open import foundation-core.dependent-identifications | ||
| open import foundation-core.subtypes | ||
|
|
||
| open import quasigroups.quasigroups | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| {{#concept "Loops" Agda=Loop}} are [quasigroups](quasigroups.quasigroups.md) | ||
| with a designated identity element, that is, `e : type-Quasigroup Q` such that | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| for any `x : type-Quasigroup Q`: | ||
|
|
||
| ```text | ||
| e * x ＝ x | ||
| x * e ＝ x | ||
| ``` | ||
|
|
||
| Note: we will see that units, when they exist, are unique, and so being a loop | ||
| is actually a property of a quasigroup rather than structure. | ||
|
|
||
| ## Definitions | ||
|
|
||
| ### Left units in quasigroups | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| ```agda | ||
| module _ | ||
| {l : Level} (Q : Quasigroup l) | ||
| where | ||
|
|
||
| private | ||
| _*_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q | ||
| _*_ = mul-Quasigroup Q | ||
|
|
||
| _l/_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q | ||
| _l/_ = left-div-Quasigroup Q | ||
|
|
||
| _r/_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q | ||
| _r/_ = right-div-Quasigroup Q | ||
|
There was a problem hiding this comment. Private definitions are against our conventions. But... since we're discussing changes to our syntax conventions currently, maybe I can use you as a test dummy? I have an idea for how we might go about having operators like these in the library |
||
|
|
||
| is-left-unit-Quasigroup : (e : type-Quasigroup Q) → UU l | ||
| is-left-unit-Quasigroup e = (x : type-Quasigroup Q) → e * x ＝ x | ||
|
|
||
| is-prop-is-left-unit-Quasigroup : | ||
| (e : type-Quasigroup Q) → is-prop (is-left-unit-Quasigroup e) | ||
| is-prop-is-left-unit-Quasigroup e = | ||
| is-prop-Π (λ x → is-set-Quasigroup Q (e * x) x) | ||
|
|
||
| is-left-unit-Quasigroup-Prop : (e : type-Quasigroup Q) → Prop l | ||
| is-left-unit-Quasigroup-Prop e = | ||
| is-left-unit-Quasigroup e , is-prop-is-left-unit-Quasigroup e | ||
|
|
||
| has-left-unit-Quasigroup : UU l | ||
| has-left-unit-Quasigroup = | ||
| Σ (type-Quasigroup Q) λ e → is-left-unit-Quasigroup e | ||
|
|
||
| term-has-left-unit-Quasigroup : has-left-unit-Quasigroup → type-Quasigroup Q | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| term-has-left-unit-Quasigroup (e , _) = e | ||
|
|
||
| left-units-agree-Quasigroup : | ||
| (e f : has-left-unit-Quasigroup) → term-has-left-unit-Quasigroup e | ||
| ＝ term-has-left-unit-Quasigroup f | ||
| left-units-agree-Quasigroup (e , e-left-unit) (f , f-left-unit) = | ||
| equational-reasoning | ||
| e ＝ (e * f) r/ f | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| by is-right-cancellative-right-div-Quasigroup Q f e | ||
| ＝ f r/ f | ||
| by ap (λ x → x r/ f) (e-left-unit f) | ||
| ＝ (f * f) r/ f | ||
| by ap (λ x → x r/ f) (inv (f-left-unit f)) | ||
| ＝ f | ||
| by inv (is-right-cancellative-right-div-Quasigroup Q f f) | ||
|
|
||
| is-prop-has-left-unit-Quasigroup : is-prop has-left-unit-Quasigroup | ||
| pr1 (is-prop-has-left-unit-Quasigroup e f) = | ||
| eq-type-subtype is-left-unit-Quasigroup-Prop | ||
| (left-units-agree-Quasigroup e f) | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| pr2 (is-prop-has-left-unit-Quasigroup e f) p = | ||
| is-set-has-uip (is-set-type-subtype is-left-unit-Quasigroup-Prop | ||
| (is-set-Quasigroup Q)) e f (pr1 (is-prop-has-left-unit-Quasigroup e f)) p | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| ``` | ||
|
|
||
| ### Right units in quasigroups | ||
|
|
||
| ```agda | ||
| is-right-unit-Quasigroup : (e : type-Quasigroup Q) → UU l | ||
| is-right-unit-Quasigroup e = (x : type-Quasigroup Q) → x * e ＝ x | ||
|
|
||
| is-prop-is-right-unit-Quasigroup : | ||
| (e : type-Quasigroup Q) → is-prop (is-right-unit-Quasigroup e) | ||
| is-prop-is-right-unit-Quasigroup e = | ||
| is-prop-Π (λ x → is-set-Quasigroup Q (x * e) x) | ||
|
|
||
| is-right-unit-Quasigroup-Prop : (e : type-Quasigroup Q) → Prop l | ||
| is-right-unit-Quasigroup-Prop e = | ||
| is-right-unit-Quasigroup e , is-prop-is-right-unit-Quasigroup e | ||
|
|
||
| has-right-unit-Quasigroup : UU l | ||
| has-right-unit-Quasigroup = | ||
| Σ (type-Quasigroup Q) λ e → is-right-unit-Quasigroup e | ||
|
|
||
| term-has-right-unit-Quasigroup : has-right-unit-Quasigroup → type-Quasigroup Q | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| term-has-right-unit-Quasigroup (e , _) = e | ||
|
|
||
| right-units-agree-Quasigroup : | ||
| (e f : has-right-unit-Quasigroup) → term-has-right-unit-Quasigroup e | ||
| ＝ term-has-right-unit-Quasigroup f | ||
| right-units-agree-Quasigroup (e , e-right-unit) (f , f-right-unit) = | ||
| equational-reasoning | ||
| e ＝ f l/ (f * e) | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| by is-right-cancellative-left-div-Quasigroup Q f e | ||
| ＝ f l/ f | ||
| by ap (λ x → f l/ x) (e-right-unit f) | ||
| ＝ f l/ (f * f) | ||
| by inv ((ap (λ x → f l/ x) (f-right-unit f))) | ||
| ＝ f | ||
| by inv (is-right-cancellative-left-div-Quasigroup Q f f) | ||
|
|
||
| is-prop-has-right-unit-Quasigroup : is-prop has-right-unit-Quasigroup | ||
| pr1 (is-prop-has-right-unit-Quasigroup e f) = | ||
| eq-type-subtype is-right-unit-Quasigroup-Prop | ||
| (right-units-agree-Quasigroup e f) | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| pr2 (is-prop-has-right-unit-Quasigroup e f) p = | ||
| is-set-has-uip (is-set-type-subtype is-right-unit-Quasigroup-Prop | ||
| (is-set-Quasigroup Q)) e f (pr1 (is-prop-has-right-unit-Quasigroup e f)) p | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| ``` | ||
|
|
||
| ### Units in quasigroups | ||
|
|
||
| A **unit**, as usual, is both a left and right unit. In fact, if `Q` has both a | ||
| left unit `e` and a right unit `f`, then already we have `e ＝ f`, and thus the | ||
| type of units is equivalent to the type of pairs of left and right units. | ||
|
|
||
| ```agda | ||
| has-unit-Quasigroup : UU l | ||
| has-unit-Quasigroup = | ||
| Σ (type-Quasigroup Q) | ||
| λ e → is-left-unit-Quasigroup e × is-right-unit-Quasigroup e | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| unit-has-unit-Quasigroup : has-unit-Quasigroup → type-Quasigroup Q | ||
| unit-has-unit-Quasigroup (e , _) = e | ||
|
|
||
| has-unit-has-left-unit-Quasigroup : | ||
| has-unit-Quasigroup → has-left-unit-Quasigroup | ||
| has-unit-has-left-unit-Quasigroup (e , e-left-unit , _) = e , e-left-unit | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| has-unit-has-right-unit-Quasigroup : | ||
| has-unit-Quasigroup → has-right-unit-Quasigroup | ||
| has-unit-has-right-unit-Quasigroup (e , _ , e-right-unit) = e , e-right-unit | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| has-unit-has-left-and-right-units-Quasigroup : | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| has-unit-Quasigroup → has-left-unit-Quasigroup × has-right-unit-Quasigroup | ||
| has-unit-has-left-and-right-units-Quasigroup e = | ||
| (has-unit-has-left-unit-Quasigroup e) , | ||
| (has-unit-has-right-unit-Quasigroup e) | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| left-and-right-units-agree-Quasigroup : | ||
| (e : has-left-unit-Quasigroup) → (f : has-right-unit-Quasigroup) → | ||
| term-has-left-unit-Quasigroup e ＝ term-has-right-unit-Quasigroup f | ||
| left-and-right-units-agree-Quasigroup (e , e-left-unit) (f , f-right-unit) = | ||
| equational-reasoning | ||
| e ＝ (e * f) r/ f | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| by is-right-cancellative-right-div-Quasigroup Q f e | ||
| ＝ f r/ f | ||
| by ap (λ x → x r/ f) (e-left-unit f) | ||
| ＝ (f * f) r/ f | ||
| by inv (ap (λ x → x r/ f) (f-right-unit f)) | ||
| ＝ f | ||
| by inv (is-right-cancellative-right-div-Quasigroup Q f f) | ||
|
|
||
| has-left-and-right-units-is-left-unit-is-right-unit : | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| (e : has-left-unit-Quasigroup) → has-right-unit-Quasigroup → | ||
| is-right-unit-Quasigroup (term-has-left-unit-Quasigroup e) | ||
| has-left-and-right-units-is-left-unit-is-right-unit e f x = | ||
| inv-tr is-right-unit-Quasigroup (left-and-right-units-agree-Quasigroup e f) | ||
| (pr2 f) x | ||
|
|
||
| has-left-and-right-units-has-unit-Quasigroup : | ||
djspacewhale marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| has-left-unit-Quasigroup → has-right-unit-Quasigroup → has-unit-Quasigroup | ||
| pr1 (has-left-and-right-units-has-unit-Quasigroup (e , _) _) = e | ||
| pr1 (pr2 (has-left-and-right-units-has-unit-Quasigroup (e , e-left-unit) _)) = | ||
| e-left-unit | ||
| pr2 (pr2 (has-left-and-right-units-has-unit-Quasigroup e f)) = | ||
| has-left-and-right-units-is-left-unit-is-right-unit e f | ||
| ``` | ||
|
|
||
| ### Loops | ||
|
|
||
| Note now that having a designated unit is a property of a quasigroup, and thus | ||
| we may make the easier definition. | ||
|
|
||
| ```agda | ||
| Loop : (l : Level) → UU (lsuc l) | ||
| Loop l = Σ (Quasigroup l) (λ Q → has-unit-Quasigroup Q) | ||
|
|
||
| quasigroup-Loop : {l : Level} (Q : Loop l) → Quasigroup l | ||
| quasigroup-Loop (Q , _) = Q | ||
| ``` | ||
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The justification for creating a new namespace for quasigroups is unclear to me. Why do you not wish to put this in
group-theory? Notice that we also have semigroups and monoids ingroup-theory. I must admit I'm not familiar with the theory of quasigroups, is the nature of the theory very different fromgroup-theory? Given its name, I would guess not, and then it might be appropriate to have it ingroup-theory.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Truthfully I'm approaching this formalization of quasigroups as a way to learn about them, so I'm not an expert on the broad theory. Including them in the
group-theorynamespace could make sense - groups are simply unital associative quasigroups, anyways - but the applications seem rather different; say, finite quasigroups classically correspond to latin squares, and their representation theory is much subtler.I don't want to step on toes too aggressively being a new contributor but the current namespace convention is a tad frustrating for me. Finding definitions is easier using the website and its search bar, but searching monolithic namespaces by hand is not as elegant as, say, using a hierarchy of namespaces a la cubical. I did think about creating a subnamespace
group-theory/quasigroupsbut as this convention does not exist currently I held off. Has this (re)organization been discussed before?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@djspacewhale, that is totally fine. I don't think you are stepping on anyone's toes, and your contribution is most welcome! Learning and formalizing at the same time is a great strategy to really get to the bottom of a subject, I use that strategy too. To that end, would you be willing to cite standard references for you definitions, such as
Pflugfelder. Quasigroups and Loops: Introduction?
We have a
references.bibfile in the root folder and there are guidelines about how to include a bibliography at the end of a file. The situation could be improved by now, but it used to be the case that the definition of quasigroups and semigroups was wrong on wikipedia, so it is important to follow a standard reference.I also think developing quasigroups in the group theory folder could make sense, because some definitions and results about quasigroups will be more general and it would be a natural setting for comparing the two developments. On the other hand, I do understand why you initially chose to create a setup in a separate namespace: The nonassociative case is actually quite different and the
group-theoryname space is quite large, containing many different concepts.We are aware of the organizational conventions of the cubical library, and other libraries as well, and we have deliberately chosen our current library organization. I personally find other library organizations a bit chaotic, and the one-concept-per-file principle is the cleanest in my view. It is also good to keep in mind that the choices for a library organization are tied to the purpose of the library: In cubical the goal is to facilitate formalization related to current research, which agda-unimath also hopes to facilitate, but agda-unimath has an important secondary purpose, which is to develop an informative resource where ultimately the library webpage could serve as a nlab-style website where you can find precise definitions and infomation about how concepts are interrelated. From that point of view, an organization with
concept.baseandconcept.propertiesmodules whereconcept.propertiesbecomes a dumping place for all sorts of properties is not helping us at all, and what would be inconcept.basein cubical could often be spread out over several pages in agda-unimath, each its own concept.I hope this explanation helps!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I actually don't have a reference text and have been formalizing roughly what's on Wikipedia and the nlab, cross-referenced with arxiv papers that arise in searches. I'll look for that text though. It's of course not the morally healthiest approach, and I'm no longer a student so sourcing texts may be a bit harder, but I'll find a better primary source!
I also appreciate agda-unimath's goal of being a readable informative source and this knowledge-for-the-people element is one reason I chose to contribute here rather than, say, cubical (long-term I'm also interested in modal type theory and applications to synthetic math, a project that appears at technical odds with cubical). My thought was less around, say, having one
groups.basedefining everything to do with groups, but more around using subfolders to consolidate "subareas" of knowledge, say, putting abelian stuff ingroup-theory/abelian-groups/and so on. That said, I'll respect how the library is currently organized, and Fredrik's notes about separating e.g. left/right quasigroups into their own files is a good note for following the one-concept-per-file principle that I'll incorporate.