From fa982023055c6f6f65fdb3fd902472084ae74312 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 7 Jan 2025 13:30:44 -0500 Subject: [PATCH] def: quasigroups (#453) # Description This PR defines defines quasigroups, and proves some very basic properties about them. ## Checklist Before submitting a merge request, please check the items below: - [x] I've read [the contributing guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md). - [x] The imports of new modules have been sorted with `support/sort-imports.hs` (or `nix run --experimental-features nix-command -f . sort-imports`). - [x] All new code blocks have "agda" as their language. If your change affects many files without adding substantial content, and you don't want your name to appear on those pages (for example, treewide refactorings or reformattings), start the commit message and PR title with `chore:`. --- src/Algebra/Quasigroup.lagda.md | 899 ++++++++++++++++++ .../Quasigroup/Instances/Group.lagda.md | 169 ++++ .../Quasigroup/Instances/Initial.lagda.md | 80 ++ src/Cat/Diagram/Initial.lagda.md | 15 +- src/Cat/Displayed/Univalence/Thin.lagda.md | 2 +- 5 files changed, 1163 insertions(+), 2 deletions(-) create mode 100644 src/Algebra/Quasigroup.lagda.md create mode 100644 src/Algebra/Quasigroup/Instances/Group.lagda.md create mode 100644 src/Algebra/Quasigroup/Instances/Initial.lagda.md diff --git a/src/Algebra/Quasigroup.lagda.md b/src/Algebra/Quasigroup.lagda.md new file mode 100644 index 000000000..e3e2b46d0 --- /dev/null +++ b/src/Algebra/Quasigroup.lagda.md @@ -0,0 +1,899 @@ +--- +description: | + Quasigroups. +--- + + +```agda +module Algebra.Quasigroup where +``` + +# Quasigroups + +Traditionally, [[groups]] are defined as [[monoids]] where every element +has a ([necessarily unique]) inverse. However, there is another path to +the theory of groups that emphasizes division/subtraction over inverses. +This perspective is especially interesting when generalizing groups to +non-associative settings; axioms of the form $xx^{-1} = 1$ are rather +ill-behaved without associativity, as inverses are no longer necessarily +unique! + +[necessarily unique]: Algebra.Monoid.html#inverses + + + +## Right quasigroups + +For the sake of maximum generality, we will build up to the definition +of quasigroups in stages, starting with right quasigroups. + +:::{.definition #right-quasigroup} +Let $\star : A \to A \to A$ be a binary operator. $(A, \star)$ is a +**right quasigroup** if $(A, \star)$ is a [[magma]], and there is some +binary operator $/ : A \to A A$, subject to the following axioms: + +- For all $x, y : A$, $(y / x) \star x = y$ +- For all $x, y : A$, $(y \star x) / x = y$ +::: + +```agda +record is-right-quasigroup {ℓ} {A : Type ℓ} (_⋆_ : A → A → A) : Type ℓ where + no-eta-equality + field + _/_ : A → A → A + /-invl : ∀ x y → (x / y) ⋆ y ≡ x + /-invr : ∀ x y → (x ⋆ y) / y ≡ x + has-is-magma : is-magma _⋆_ + + open is-magma has-is-magma public +``` + +Intuitively, the $/ : A \to A \to A$ operation acts like a sort of +right-biased division. This is further cemented by noting that +the existence of such an operation implies that every $x : A$, the action +$- \star x : A \to A$ is an [[equivalence]]. + +```agda + ⋆-equivr : ∀ x → is-equiv (_⋆ x) + ⋆-equivr x .is-eqv y .centre = y / x , /-invl y x + ⋆-equivr x .is-eqv y .paths (l , lx=y) = + Σ-prop-path (λ l → has-is-set (l ⋆ x) y) $ + y / x ≡˘⟨ ap (_/ x) lx=y ⟩ + (l ⋆ x) / x ≡⟨ /-invr l x ⟩ + l ∎ +``` + +This in turn implies that $- / x : A \to A$ is an equivalence. + +```agda + /-equivr : ∀ x → is-equiv (_/ x) + /-equivr x = inverse-is-equiv (⋆-equivr x) +``` + +As easy corollaries, we get that multiplication and division in $A$ are +right-cancellative. + + +```agda + opaque + ⋆-cancelr : ∀ {x y} (z : A) → x ⋆ z ≡ y ⋆ z → x ≡ y + ⋆-cancelr z = Equiv.injective (_⋆ z , ⋆-equivr z) + + /-cancelr : ∀ {x y} (z : A) → x / z ≡ y / z → x ≡ y + /-cancelr z = Equiv.injective (_/ z , /-equivr z) +``` + +It turns out that $- \star x$ being an equivalence is a sufficient condition +for a $A$ to be a right quasigroup, provided that $A$ is a [[set]]. + +```agda +⋆-equivr→is-right-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-set A + → (∀ x → is-equiv (_⋆ x)) + → is-right-quasigroup _⋆_ +``` + +The proof is an exercise in unrolling definitions. If $- \star x$ is an +equivalence, then $(- \star y)^{-1}(x)$ serves as a perfectly valid +definition of $x / y$; both axioms follow directly from the +unit and counit of the equivalence. + +```agda +⋆-equivr→is-right-quasigroup {_⋆_ = _⋆_} A-set ⋆-eqv = + ⋆-right-quasi + where + open is-right-quasigroup + + module ⋆-eqv x = Equiv (_⋆ x , ⋆-eqv x) + + ⋆-right-quasi : is-right-quasigroup _⋆_ + ⋆-right-quasi ._/_ x y = ⋆-eqv.from y x + ⋆-right-quasi ./-invl x y = ⋆-eqv.ε y x + ⋆-right-quasi ./-invr x y = ⋆-eqv.η y x + ⋆-right-quasi .has-is-magma .is-magma.has-is-set = A-set +``` + +We can upgrade this correspondence to an equivalence, as we definitionally +get back the same division operation we started with after round-tripping. + +```agda +is-right-quasigroup≃⋆-equivr + : ∀ {_⋆_ : A → A → A} + → is-right-quasigroup _⋆_ ≃ (is-set A × (∀ x → is-equiv (_⋆ x))) +is-right-quasigroup≃⋆-equivr {_⋆_ = _⋆_} = + Iso→Equiv $ + ⟨ has-is-set , ⋆-equivr ⟩ , + iso (uncurry ⋆-equivr→is-right-quasigroup) + (λ _ → prop!) + (λ ⋆-right-quasi → + let open is-right-quasigroup ⋆-right-quasi in + Iso.injective eqv (refl ,ₚ prop!)) + where + open is-right-quasigroup + unquoteDecl eqv = declare-record-iso eqv (quote is-right-quasigroup) +``` + +Crucially, this means that the division operation $/ : A \to A \to A$ +is actually a [[property]] rather than structure, as both `is-equiv`{.Agda} and +`is-set`{.Agda} are propositions. + +```agda +is-right-quasigroup-is-prop + : ∀ {_⋆_ : A → A → A} + → is-prop (is-right-quasigroup _⋆_) +is-right-quasigroup-is-prop {A = A} = + Equiv→is-hlevel 1 is-right-quasigroup≃⋆-equivr (hlevel 1) +``` + + + +### Right quasigroup homomorphisms + +In the previous section, we proved that the existence of a right division +operation was actually a property of a magma, rather than structure. We shall now see +that right division is automatically preserved by magma homomorphisms. + +We start by defining the corresponding notion of structure for right +quasigroups. + +:::{.definition #right-quasigroup-structure} +A **right quasigroup structure** on a type $A$ is a binary operation +$\star : A \to A \to A$ such that $(A, \star)$ is a right quasigroup. +::: + +```agda +record Right-quasigroup-on {ℓ} (A : Type ℓ) : Type ℓ where + no-eta-equality + field + _⋆_ : A → A → A + has-is-right-quasigroup : is-right-quasigroup _⋆_ + + open is-right-quasigroup has-is-right-quasigroup public + +``` + +:::{.definition #right-quasigroup-homomorphism} +A **right quasigroup homomorphism** between two right quasigroups $A, B$ +is a function $f : A \to B$ such that $f (x \star y) = f x \star f y$. +::: + +```agda +record is-right-quasigroup-hom + {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + (f : A → B) + (S : Right-quasigroup-on A) (T : Right-quasigroup-on B) + : Type (ℓ ⊔ ℓ') + where + no-eta-equality + private + module A = Right-quasigroup-on S + module B = Right-quasigroup-on T + field + pres-⋆ : ∀ x y → f (x A.⋆ y) ≡ f x B.⋆ f y +``` + +Preservation of right division follows almost immediately from +right-cancellativity. + + +```agda + pres-/ : ∀ x y → f (x A./ y) ≡ f x B./ f y + pres-/ x y = + B.⋆-cancelr (f y) $ + f (x A./ y) B.⋆ f y ≡˘⟨ pres-⋆ (x A./ y) y ⟩ + f ((x A./ y) A.⋆ y) ≡⟨ ap f (A./-invl x y) ⟩ + f x ≡˘⟨ B./-invl (f x) (f y) ⟩ + (f x B./ f y) B.⋆ f y ∎ +``` + + + + + +Right quasigroups are algebraic structures, so they form a [[thin structure]] +over $\Sets$. + +```agda + Right-quasigroup-structure : ∀ ℓ → Thin-structure ℓ Right-quasigroup-on + Right-quasigroup-structure ℓ .is-hom f A B .∣_∣ = + is-right-quasigroup-hom f A B + Right-quasigroup-structure ℓ .is-hom f A B .is-tr = + is-right-quasigroup-hom-is-prop + Right-quasigroup-structure ℓ .id-is-hom .pres-⋆ x y = + refl + Right-quasigroup-structure ℓ .∘-is-hom f g f-hom g-hom .pres-⋆ x y = + ap f (g-hom .pres-⋆ x y) ∙ f-hom .pres-⋆ (g x) (g y) + Right-quasigroup-structure ℓ .id-hom-unique {A} {S} {T} p q = + Right-quasigroup-on-pathp (ext (p .pres-⋆)) + +``` + +This observation lets us neatly organize right quasigroups into a [[category]]. + +```agda +Right-quasigroups : ∀ ℓ → Precategory (lsuc ℓ) ℓ +Right-quasigroups ℓ = Structured-objects (Right-quasigroup-structure ℓ) + +module Right-quasigroups {ℓ} = Cat.Reasoning (Right-quasigroups ℓ) + +Right-quasigroup : (ℓ : Level) → Type (lsuc ℓ) +Right-quasigroup ℓ = Right-quasigroups.Ob {ℓ} +``` + + + + +## Left quasigroups + +We can dualise the definition of right quasigroups to arrive at the +notion of a **left quasigroup**. + +:::{.definition #left-quasigroup} +Let $\star : A \to A \to A$ be a binary operator. $(A, \star)$ is a +**left quasigroup** if $(A, \star)$ is a [[magma]], and there is some +binary operator $\backslash : A \to A \to A$, subject to the following axioms: + +- For all $x, y : A$, $x \star (x \backslash y) = y$ +- For all $x, y : A$, $x \backslash (x \star y) = y$ +::: + + +```agda +record is-left-quasigroup {ℓ} {A : Type ℓ} (_⋆_ : A → A → A) : Type ℓ where + no-eta-equality + field + _⧵_ : A → A → A + ⧵-invr : ∀ x y → x ⋆ (x ⧵ y) ≡ y + ⧵-invl : ∀ x y → x ⧵ (x ⋆ y) ≡ y + has-is-magma : is-magma _⋆_ + + open is-magma has-is-magma public +``` + +Intuitively, we should think of $x \backslash y$ as "$y$ divided by $x$" or +"$y$ over $x$". This is reinforced by the fact that for every $x : A$, the action +$x \star - : A \to A$ is an [[equivalence]]. + +```agda + ⋆-equivl : ∀ x → is-equiv (x ⋆_) + ⋆-equivl x .is-eqv y .centre = x ⧵ y , ⧵-invr x y + ⋆-equivl x .is-eqv y .paths (r , xr=y) = + Σ-prop-path (λ r → has-is-set (x ⋆ r) y) $ + x ⧵ y ≡˘⟨ ap (x ⧵_) xr=y ⟩ + x ⧵ (x ⋆ r) ≡⟨ ⧵-invl x r ⟩ + r ∎ + + ⧵-equivl : ∀ x → is-equiv (x ⧵_) + ⧵-equivl x = inverse-is-equiv (⋆-equivl x) +``` + +This implies that that multiplication and division in $A$ is left-cancellative. + +```agda + opaque + ⋆-cancell : ∀ (x : A) {y z} → x ⋆ y ≡ x ⋆ z → y ≡ z + ⋆-cancell x = Equiv.injective (x ⋆_ , ⋆-equivl x) + + ⧵-cancell : ∀ (x : A) {y z} → x ⧵ y ≡ x ⧵ z → y ≡ z + ⧵-cancell x = Equiv.injective (x ⧵_ , ⧵-equivl x) +``` + +Next, we shall show that left quasigroups are formally dual to right quasigroups. + +```agda +is-left-quasigroup≃op-is-right-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-left-quasigroup _⋆_ ≃ is-right-quasigroup (λ x y → y ⋆ x) +``` + +
+The proof of this fact is rather tedious, so we will omit the +details. + + +```agda +is-left-quasigroup→op-is-right-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-left-quasigroup _⋆_ → is-right-quasigroup (λ x y → y ⋆ x) + +is-right-quasigroup→op-is-left-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-right-quasigroup _⋆_ → is-left-quasigroup (λ x y → y ⋆ x) + +is-left-quasigroup→op-is-right-quasigroup {_⋆_ = _⋆_} A-quasi = A-op-quasi + where + open is-left-quasigroup A-quasi + open is-right-quasigroup + + A-op-quasi : is-right-quasigroup (λ x y → y ⋆ x) + A-op-quasi ._/_ x y = y ⧵ x + A-op-quasi ./-invr = flip ⧵-invl + A-op-quasi ./-invl = flip ⧵-invr + A-op-quasi .has-is-magma .is-magma.has-is-set = hlevel 2 + +is-right-quasigroup→op-is-left-quasigroup {_⋆_ = _⋆_} A-quasi = A-op-quasi + where + open is-right-quasigroup A-quasi + open is-left-quasigroup + + A-op-quasi : is-left-quasigroup (λ x y → y ⋆ x) + A-op-quasi ._⧵_ x y = y / x + A-op-quasi .⧵-invr = flip /-invl + A-op-quasi .⧵-invl = flip /-invr + A-op-quasi .has-is-magma .is-magma.has-is-set = hlevel 2 + +is-left-quasigroup≃op-is-right-quasigroup = + Iso→Equiv $ + is-left-quasigroup→op-is-right-quasigroup , + iso is-right-quasigroup→op-is-left-quasigroup + (λ _ → prop!) + (λ ⋆-left-quasi → + let open is-left-quasigroup ⋆-left-quasi in + Iso.injective eqv (refl ,ₚ prop!)) + where + private unquoteDecl eqv = declare-record-iso eqv (quote is-left-quasigroup) +``` +
+ + +This in turn means that being a left quasigroup is a property of a binary +operation. + +```agda +is-left-quasigroup-is-prop + : ∀ {_⋆_ : A → A → A} + → is-prop (is-left-quasigroup _⋆_) +is-left-quasigroup-is-prop {A = A} = + Equiv→is-hlevel 1 (is-left-quasigroup≃op-is-right-quasigroup) (hlevel 1) +``` + + + + + +### Left quasigroup homomorphisms + +We can continue dualizing to define a notion of homomorphism for +left quasigroups, though we shall be much more terse in our development. +Following the pattern of right quasigroups, we begin by defining +**left quasigroup structures**. + + +:::{.definition #left-quasigroup-structure} +A **left quasigroup structure** on a type $A$ is a binary operation +$\star : A \to A \to A$ such that $(A, \star)$ is a left quasigroup. +::: + +```agda +record Left-quasigroup-on {ℓ} (A : Type ℓ) : Type ℓ where + no-eta-equality + field + _⋆_ : A → A → A + has-is-left-quasigroup : is-left-quasigroup _⋆_ + + open is-left-quasigroup has-is-left-quasigroup public +``` + + +:::{.definition #left-quasigroup-homomorphism} +A **left quasigroup homomorphism** between two left quasigroups $A, B$ +is a function $f : A \to B$ such that $f (x \star y) = f x \star f y$. +::: + +```agda +record is-left-quasigroup-hom + {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + (f : A → B) + (S : Left-quasigroup-on A) (T : Left-quasigroup-on B) + : Type (ℓ ⊔ ℓ') + where + no-eta-equality + private + module A = Left-quasigroup-on S + module B = Left-quasigroup-on T + field + pres-⋆ : ∀ x y → f (x A.⋆ y) ≡ f x B.⋆ f y +``` + +Dual to right quasigroups, preservation of left division follows from +left-cancellativity. + +```agda + pres-⧵ : ∀ x y → f (x A.⧵ y) ≡ f x B.⧵ f y + pres-⧵ x y = + B.⋆-cancell (f x) $ + f x B.⋆ f (x A.⧵ y) ≡˘⟨ pres-⋆ x (x A.⧵ y) ⟩ + f (x A.⋆ (x A.⧵ y)) ≡⟨ ap f (A.⧵-invr x y) ⟩ + f y ≡˘⟨ B.⧵-invr (f x) (f y) ⟩ + f x B.⋆ (f x B.⧵ f y) ∎ +``` + + + +Left quasigroups are algebraic structures, so they form a [[thin structure]] +over $\Sets$. + + + +```agda + Left-quasigroup-structure : ∀ ℓ → Thin-structure ℓ Left-quasigroup-on + Left-quasigroup-structure ℓ .is-hom f A B .∣_∣ = + is-left-quasigroup-hom f A B + Left-quasigroup-structure ℓ .is-hom f A B .is-tr = + is-left-quasigroup-hom-is-prop + Left-quasigroup-structure ℓ .id-is-hom .pres-⋆ x y = + refl + Left-quasigroup-structure ℓ .∘-is-hom f g f-hom g-hom .pres-⋆ x y = + ap f (g-hom .pres-⋆ x y) ∙ f-hom .pres-⋆ (g x) (g y) + Left-quasigroup-structure ℓ .id-hom-unique p q = + Left-quasigroup-on-pathp (ext (p .pres-⋆)) +``` + +This observation lets us assemble left quasigroups into a [[category]]. + +```agda +Left-quasigroups : ∀ ℓ → Precategory (lsuc ℓ) ℓ +Left-quasigroups ℓ = Structured-objects (Left-quasigroup-structure ℓ) + +module Left-quasigroups {ℓ} = Cat.Reasoning (Left-quasigroups ℓ) + +Left-quasigroup : (ℓ : Level) → Type (lsuc ℓ) +Left-quasigroup ℓ = Left-quasigroups.Ob {ℓ} +``` + + + + +## Quasigroups + +:::{.definition #quasigroup} +A type $A$ equipped with a binary operation $\star : A \to A \to A$ is +a **quasigroup** if it is a [[left quasigroup]] and a [[right quasigroup]]. +::: + + +```agda +record is-quasigroup {ℓ} {A : Type ℓ} (_⋆_ : A → A → A) : Type ℓ where + no-eta-equality + field + has-is-left-quasigroup : is-left-quasigroup _⋆_ + has-is-right-quasigroup : is-right-quasigroup _⋆_ +``` + + + +Quasigroups obey the **latin square property**: for every $x, y : A$, +there exists a unique pair $l, r : A$ such that $l \star x = y$ and $x \star r = y$. + +```agda + ⋆-latin : ∀ x y → is-contr (Σ[ l ∈ A ] Σ[ r ∈ A ] (l ⋆ x ≡ y × x ⋆ r ≡ y)) +``` + +The proof is an exercise in equivalence yoga: by definition, a quasigroup +is both a left and right quasigroup, so multiplication on the left and right +is an equivalence, so the types $\Sigma (l : A) l \star x = y$ and +$\Sigma (r : A) r \star x = y$ are both contractible. Moreover, +$(\Sigma (l : A) l \star x = y) \times (\Sigma (r : A) r \star x = y)$ is +equivalent to $\Sigma (l : A) \Sigma (r : A) (l \star x = y \times x \star r = y)$, +so the latter must also be contractible. + +```agda + ⋆-latin x y = + Equiv→is-hlevel 0 + latin-eqv + (×-is-hlevel 0 (⋆-equivr x .is-eqv y) (⋆-equivl x .is-eqv y)) + where + latin-eqv + : (Σ[ l ∈ A ] Σ[ r ∈ A ] (l ⋆ x ≡ y × x ⋆ r ≡ y)) + ≃ ((Σ[ l ∈ A ] l ⋆ x ≡ y) × (Σ[ r ∈ A ] x ⋆ r ≡ y)) + latin-eqv = + Σ[ l ∈ A ] Σ[ r ∈ A ] (l ⋆ x ≡ y × x ⋆ r ≡ y) ≃⟨ Σ-ap id≃ (λ l → Σ-swap₂) ⟩ + Σ[ l ∈ A ] (l ⋆ x ≡ y × (Σ[ r ∈ A ] (x ⋆ r) ≡ y)) ≃⟨ Σ-assoc ⟩ + (Σ[ l ∈ A ] l ⋆ x ≡ y) × (Σ[ r ∈ A ] x ⋆ r ≡ y) ≃∎ +``` + +We also have the following pair of useful identities that relate +left and right division. + +```agda + /-⧵-cancelr : ∀ x y → x / (y ⧵ x) ≡ y + /-⧵-cancelr x y = + x / (y ⧵ x) ≡˘⟨ ap (_/ (y ⧵ x)) (⧵-invr y x) ⟩ + (y ⋆ (y ⧵ x)) / (y ⧵ x) ≡⟨ /-invr y (y ⧵ x) ⟩ + y ∎ + + /-⧵-cancell : ∀ x y → (x / y) ⧵ x ≡ y + /-⧵-cancell x y = + (x / y) ⧵ x ≡˘⟨ ap ((x / y) ⧵_) (/-invl x y) ⟩ + (x / y) ⧵ ((x / y) ⋆ y) ≡⟨ ⧵-invl (x / y) y ⟩ + y ∎ +``` + + + +### Quasigroup homomorphisms + +:::{.definition #quasigroup-structure} +A **quasigroup structure** on a type $A$ is a binary operation +$\star : A \to A \to A$ such that $(A, \star)$ is a quasigroup. +::: + +```agda +record Quasigroup-on {ℓ} (A : Type ℓ) : Type ℓ where + no-eta-equality + field + _⋆_ : A → A → A + has-is-quasigroup : is-quasigroup _⋆_ + + open is-quasigroup has-is-quasigroup public +``` + + + +:::{.definition #quasigroup-homomorphism} +A **quasigroup homomorphism** between two quasigroups $A, B$ +is a function $f : A \to B$ such that $f (x \star y) = f x \star f y$. +::: + + +```agda +record is-quasigroup-hom + {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + (f : A → B) + (S : Quasigroup-on A) (T : Quasigroup-on B) + : Type (ℓ ⊔ ℓ') + where + no-eta-equality + private + module A = Quasigroup-on S + module B = Quasigroup-on T + field + pres-⋆ : ∀ x y → f (x A.⋆ y) ≡ f x B.⋆ f y +``` + + + + + + + +Quasigroups and quasigroup homomorphisms form a [[thin structure]]. + +```agda + Quasigroup-structure : ∀ ℓ → Thin-structure ℓ Quasigroup-on +``` + +
+ + + +```agda + Quasigroup-structure ℓ .is-hom f A B .∣_∣ = + is-quasigroup-hom f A B + Quasigroup-structure ℓ .is-hom f A B .is-tr = + is-quasigroup-hom-is-prop + Quasigroup-structure ℓ .id-is-hom .pres-⋆ x y = + refl + Quasigroup-structure ℓ .∘-is-hom f g f-hom g-hom .pres-⋆ x y = + ap f (g-hom .pres-⋆ x y) ∙ f-hom .pres-⋆ (g x) (g y) + Quasigroup-structure ℓ .id-hom-unique p q = + Quasigroup-on-pathp (ext (p .pres-⋆)) +``` +
+ +This gives us a tidy way to construct the category of quasigroups. + +```agda +Quasigroups : ∀ ℓ → Precategory (lsuc ℓ) ℓ +Quasigroups ℓ = Structured-objects (Quasigroup-structure ℓ) + +module Quasigroups {ℓ} = Cat.Reasoning (Quasigroups ℓ) + +Quasigroup : (ℓ : Level) → Type (lsuc ℓ) +Quasigroup ℓ = Quasigroups.Ob {ℓ} +``` + + + +## Constructing quasigroups + +The interfaces for `is-quasigroup`{.Agda} and `Quasigroup-on`{.Agda} are +deeply nested and contain some duplication, so we introduce some helper +functions for constructing them. + +```agda +record make-quasigroup {ℓ} (A : Type ℓ) : Type ℓ where + field + quasigroup-is-set : is-set A + _⋆_ : A → A → A + _⧵_ : A → A → A + _/_ : A → A → A + + /-invl : ∀ x y → (x / y) ⋆ y ≡ x + /-invr : ∀ x y → (x ⋆ y) / y ≡ x + ⧵-invr : ∀ x y → x ⋆ (x ⧵ y) ≡ y + ⧵-invl : ∀ x y → x ⧵ (x ⋆ y) ≡ y +``` + + diff --git a/src/Algebra/Quasigroup/Instances/Group.lagda.md b/src/Algebra/Quasigroup/Instances/Group.lagda.md new file mode 100644 index 000000000..2b157e6d9 --- /dev/null +++ b/src/Algebra/Quasigroup/Instances/Group.lagda.md @@ -0,0 +1,169 @@ +--- +description: | + Groups and quasigroups +--- + +```agda +module Algebra.Quasigroup.Instances.Group where +``` + +# Groups and quasigroups + + + +Every [[group]] is a [[quasigroup]], as multiplication in a group is +an equivalence. + +```agda +is-group→is-left-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-group _⋆_ + → is-left-quasigroup _⋆_ +is-group→is-left-quasigroup {_⋆_ = _⋆_} ⋆-group = + ⋆-equivl→is-left-quasigroup (hlevel 2) ⋆-equivl + where open is-group ⋆-group + +is-group→is-right-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-group _⋆_ + → is-right-quasigroup _⋆_ +is-group→is-right-quasigroup {_⋆_ = _⋆_} ⋆-group = + ⋆-equivr→is-right-quasigroup (hlevel 2) ⋆-equivr + where open is-group ⋆-group + +is-group→is-quasigroup + : ∀ {_⋆_ : A → A → A} + → is-group _⋆_ + → is-quasigroup _⋆_ +is-group→is-quasigroup {_⋆_ = _⋆_} ⋆-group .is-quasigroup.has-is-left-quasigroup = + is-group→is-left-quasigroup ⋆-group +is-group→is-quasigroup {_⋆_ = _⋆_} ⋆-group .is-quasigroup.has-is-right-quasigroup = + is-group→is-right-quasigroup ⋆-group +``` + +## Associative quasigroups as groups + +Conversely, if a quasigroup $(A, \star)$ is merely inhabited and associative, +then it is a group. + +```agda +associative+is-quasigroup→is-group + : ∀ {_⋆_ : A → A → A} + → ∥ A ∥ + → (∀ x y z → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z) + → is-quasigroup _⋆_ + → is-group _⋆_ +``` + +We start by observing that `is-group` is an h-prop, so it suffices to +consider the case where $A$ is inhabited. + +```agda +associative+is-quasigroup→is-group {A = A} {_⋆_ = _⋆_} ∥a∥ ⋆-assoc ⋆-quasi = + rec! (λ a → to-is-group (⋆-group a)) ∥a∥ +``` + + + +Next, a useful technical lemma: if $a \star x = b \star y$, then +$x \backslash a = b / y$. + +```agda + ⧵-/-comm + : ∀ {a b x y} + → x ⋆ b ≡ a ⋆ y + → x ⧵ a ≡ b / y +``` + +The proof is an elegant bit of algebra. Recall that in a quasigroup, +$\star$ is left and right cancellative, so it suffices to show that: + +$$(x \star (x \backslash a)) \star y = (x \star (b / y)) \star y$$ + +Next, $(x \star (x \backslash a)) \star y = a \star y$, and $a \star y = x \star b$, +so it remains to show that $x \star b = (x \star (b / y)) \star y$. Crucially, +$\star$ is associative, so: + +$$ +(x \star (b / y)) \star y = x \star ((b / y) \star y) = x \star b +$$ + +which completes the proof. + +```agda + ⧵-/-comm {a} {b} {x} {y} comm = + ⋆-cancell x $ ⋆-cancelr y $ + (x ⋆ (x ⧵ a)) ⋆ y ≡⟨ ap (_⋆ y) (⧵-invr x a) ⟩ + a ⋆ y ≡˘⟨ comm ⟩ + x ⋆ b ≡˘⟨ ap (x ⋆_) (/-invl b y) ⟩ + x ⋆ ((b / y) ⋆ y) ≡⟨ ⋆-assoc x (b / y) y ⟩ + (x ⋆ (b / y)) ⋆ y ∎ +``` + +With that out of the way, we shall show that + +$$(A, \star, (a \backslash a), (\lambda x. (a \backslash a) / x))$$ + +forms a group for any $a : A$. + +```agda + ⋆-group : A → make-group A + ⋆-group a .group-is-set = hlevel 2 + ⋆-group a .unit = a ⧵ a + ⋆-group a .mul x y = x ⋆ y + ⋆-group a .inv x = (a ⧵ a) / x +``` + +Associativity is one of our hypotheses, so all that remains is left +inverses and left identities. Next, note that + +$$ +(a \backslash a), (\lambda x. (a \backslash a) / x)) \star x = (a \backslash a) +$$ + +is just one of the quasigroup axioms. Finally, our lemma gives us +$a \backslash a = x / x$, so we have: + +$$ +(a \backslash a) \star x = (x / x) \star x = x +$$ + +which completes the proof. + +```agda + ⋆-group a .assoc x y z = + ⋆-assoc x y z + ⋆-group a .invl x = + /-invl (a ⧵ a) x + ⋆-group a .idl x = + (a ⧵ a) ⋆ x ≡⟨ ap (_⋆ x) (⧵-/-comm refl) ⟩ + (x / x) ⋆ x ≡⟨ /-invl x x ⟩ + x ∎ +``` + +Taking a step back, this result demonstrates that associative quasigroups +behave like potentially empty groups. diff --git a/src/Algebra/Quasigroup/Instances/Initial.lagda.md b/src/Algebra/Quasigroup/Instances/Initial.lagda.md new file mode 100644 index 000000000..ad84c437a --- /dev/null +++ b/src/Algebra/Quasigroup/Instances/Initial.lagda.md @@ -0,0 +1,80 @@ +--- +description: | + The initial quasigroup. +--- + + +```agda +module Algebra.Quasigroup.Instances.Initial where +``` + +# The initial quasigroup {defines="initial-quasigroup empty-quasigroup"} + +The empty type trivially forms a [[quasigroup]]. + + + +```agda +Empty-quasigroup : ∀ {ℓ} → Quasigroup ℓ +Empty-quasigroup = to-quasigroup ⊥-quasigroup where + open make-quasigroup + + ⊥-quasigroup : make-quasigroup (Lift _ ⊥) + ⊥-quasigroup .quasigroup-is-set = hlevel 2 + ⊥-quasigroup ._⋆_ () + ⊥-quasigroup ._⧵_ () + ⊥-quasigroup ._/_ () + ⊥-quasigroup ./-invl () + ⊥-quasigroup ./-invr () + ⊥-quasigroup .⧵-invr () + ⊥-quasigroup .⧵-invl () +``` + +Moreover, the empty quasigroup is an [[initial object]] in the category +of quasigroups, as there is a unique function out of the empty type. + +```agda +Empty-quasigroup-is-initial : is-initial (Quasigroups ℓ) Empty-quasigroup +Empty-quasigroup-is-initial A .centre .hom () +Empty-quasigroup-is-initial A .centre .preserves .is-quasigroup-hom.pres-⋆ () +Empty-quasigroup-is-initial A .paths f = ext λ () + +Initial-quasigroup : Initial (Quasigroups ℓ) +Initial-quasigroup .Initial.bot = Empty-quasigroup +Initial-quasigroup .Initial.has⊥ = Empty-quasigroup-is-initial +``` + +In fact, the empty quasigroup is a [[strict initial object]]. + +```agda +Initial-quasigroup-is-strict + : is-strict-initial (Quasigroups ℓ) Initial-quasigroup +Initial-quasigroup-is-strict = + make-is-strict-initial (Quasigroups _) Initial-quasigroup $ λ A f → ext λ a → + absurd (Lift.lower (f # a)) +``` + + diff --git a/src/Cat/Diagram/Initial.lagda.md b/src/Cat/Diagram/Initial.lagda.md index 12256894d..db090ac2c 100644 --- a/src/Cat/Diagram/Initial.lagda.md +++ b/src/Cat/Diagram/Initial.lagda.md @@ -93,7 +93,7 @@ a proposition: (x1 .has⊥ ob) (x2 .has⊥ ob) i ``` -## Strictness +## Strictness {defines="strict-initial-object"} An initial object is said to be *[strict]* if every morphism into it is an *iso*morphism. This is a categorical generalization of the fact that if one can write a function $X \to \bot$ then $X$ must itself be empty. @@ -121,6 +121,19 @@ Strictness is a property of, not structure on, an initial object. is-strict-initial-is-prop i = hlevel 1 ``` +As maps out of initial objects are unique, it suffices to show that +every map $\text{!`} \circ f = id$ for every $f : X \to \bot$ to establish that $\bot$ is a +strict initial object. + +```agda + make-is-strict-initial + : (i : Initial) + → (∀ x → (f : Hom x (i .bot)) → (¡ i) ∘ f ≡ id) + → is-strict-initial i + make-is-strict-initial i p x f = + make-invertible (¡ i) (¡-unique₂ i (f ∘ ¡ i) id) (p x f) +``` + -# Thinly displayed structures +# Thinly displayed structures {defines=thin-structure} The HoTT Book's version of the structure identity principle can be seen as a very early example of [[displayed category]] theory. Their