lude

Algebra.slop.md (31208B)

---

 # Long Discussion
 
 ## Summary
 
 ### 1. Initial objects
 - **Ring → ℤ**, via n ↦ n·1. The initial object is always the free algebra on no generators.
 - **Rng → 0**, the zero ring, which is also terminal. Rng maps ℤ → R correspond to idempotents of R.
 - **Rig → ℕ.** Absorption doesn't matter here, since 0·0 = 0 is derivable in unital rigs.
 - **Rg:** 0 with absorption. Without absorption the initial object is {0, 0², …} ≅ ({1, 2, …}, max, +).
 - **Rig without 0 → ℕ₊**, and ∅ if 1 is dropped too.
 - **Non-associative rings → ℤ** (0 if non-unital). **Near-rings → ℤ** if unital, else 0.
 - **Commutative versions** have the same initial objects.
 - **Derivable laws in rings:** additive commutativity (expand (1+1)(a+b) two ways) and absorption (by cancellation).
 
 ### 2. Literals under RebindableSyntax
 - **Integer literals:**
   - `fromNatural :: Natural -> a` lives on `Semiring`, since ℕ is the initial rig. Its default uses binary splitting.
   - `fromZ` lives on `Ring`.
   - The hook is `fromInteger = fromNatural . P.fromInteger`, where `P.fromInteger` is base's `Num` method at `Natural`; instances are global.
 - **Negative literals** go through `negate`, which needs `Ring`.
   - Keep NegativeLiterals and LexicalNegation off; they would produce `fromInteger (-n)`.
   - Detect them with Template Haskell's `isExtEnabled` in a splice, or with a GHC plugin, plus a runtime error as a safety net.
 - **Laws:** these maps are homomorphisms, which makes them unique; overriding them is only for speed.
 - **Caveat:** in idempotent semirings (Bool, min-plus, max-plus), every positive literal equals `one`.
 - **Decimal literals:**
   - `fromQ` lives on a ℚ-algebra class (every nonzero integer invertible; ℚ is initial). The condition is not "characteristic 0".
   - `Double` overrides it with `P.fromRational` to avoid double rounding.
   - A semiring version is possible via ℚ≥0.
   - Skip a methodless `CharZero`. Positive characteristic, if needed, gets an associated type-level `Characteristic` with `KnownNat` (useful for Frobenius).
 
 ### 3. Terminology
 - There's no standard adjective for "is a ring". The nearest are rig or bimonoidal category; "ringoid" means an Ab-enriched category; "ringed" is already taken.
 - Rename endofunctor algebras to F-algebras and F-coalgebras, freeing "algebra" for associative algebras. Avoid "R-ring".
 
 ### 4. Scope of the hierarchy
 - **Add:**
   - division rings and fields;
   - Euclidean (`quotRem`/`divMod`, `gcd`, `lcm`, over rigs);
   - monus;
   - signed/ordered classes (`abs`/`signum` kept out of `Ring`);
   - `Module` over a rig, with an associated `Scalar`;
   - associative algebras (methodless, with `fromScalar r = r *^ one`);
   - `Action m x`;
   - torsors/affine spaces with `Diff x`.
 - **Maybe:** semifields, lattices/Boolean algebras, star semirings.
 - **Skip:** rng, rg, near-rings, non-associative rings, magmas, quasigroups, PID/UFD (`GcdDomain` optional). Integral domain later came back as `Domain`.
 - **Modules** have the same axioms over rigs, rings and fields.
   - Over rigs, 0·m = 0 must be stated; over rings, negatives are forced.
   - Vector space is a constraint synonym. Non-commutative scalars give left vs. right modules.
 - **Algebras** need commutative scalars. Law: r*^(ab) = (r*^a)b = a(r*^b).
   - Instances: complex numbers, polynomials, power series, matrices, quaternions, dual numbers, functions, monoid/group algebras.
   - Skip Lie algebras, octonions, non-unital algebras.
 - **Monoids and actions** in a monoidal category:
   - (Set, ×): monoids and actions.
   - (CMon, ⊗): rigs and semimodules.
   - (Ab, ⊗): rings and modules.
   - (Vect, ⊗): algebras and representations.
   - (Endofunctors, ∘): monads and their algebras.
   
   A monoid is a one-object category, and an action is a functor out of it.
 
 ### 5. Division, `NonZero`, `Units`
 - **`Divisive`** (`recip`, `/`, `^^`) is shared by `MulGroup` and `DivisionSemiring`, a group with zero. Laws are guarded. `recip zero` is unspecified; Lean's meadow convention `recip 0 = 0` is the alternative.
 - **`NonZero a`** is a newtype with a hidden constructor, nominal role and smart constructor. Its accessor is not a record field, because record-update syntax would let clients forge a zero.
   - It's a monoid iff `a` is a domain, a group iff `a` is a group with zero, and an additive semigroup iff `a` is zero-sum-free (`NonZero Natural` = ℕ₊). `negate` preserves it in rings.
   - `Int`/`Word` aren't domains, and `Double` breaks the invariant.
   - Use it for divisors, Euclidean norms, `leadingCoeff` and mixed division, with partial wrappers for literal divisors (there are no `NonZero` literals).
 - **Units:**
   - They're defined for any monoid: M^× is the largest submonoid that's a group. It's right adjoint to groups ↪ monoids; the -oid analogue is the core of a category.
   - Examples: ℤ → ±1; ℕ → 1; k[x] → nonzero constants; invertible matrices; ℤ/n → coprime residues; `Int` → the odd numbers. `AddUnits` is the additive version.
   - In a group with zero, `Units ≅ NonZero`; keep both types anyway.
   - Model: a single-field `newtype Units a`, plus a class `HasUnits` with `toUnit` (returning an unboxed sum) and `invertUnit`. `Units a` is then an `IsMulGroup`, and instances compose (matrices via the determinant).
   - Don't store the inverse; in your rep-polymorphic setting that would need an unlifted tuple. Name it `Units`, not `Unit`.
 - **No class for testing equality with `one`.**
 
 ### 6. Representation polymorphism
 - **The rule:** no variable or argument may have a representation-polymorphic type. Function types are always lifted, so `coerce` between functions works generically.
 - **`NonZero` under it:**
   - It becomes `NonZero :: TYPE r -> TYPE r` via UnliftedNewtypes.
   - `onNonZero = coerce`, and `getNonZero = onNonZero id` works over each fixed representation.
   - Instances coerce function-typed methods.
 - **What has to be per-instance:**
   - Anything that inspects values, such as the zero test.
   - Default method bodies, which can't bind values either.
 - **Other consequences:**
   - `Maybe` holds only lifted types, so decisions return unboxed sums.
   - base's `Eq`/`Ord` get standalone instances at `a :: Type`.
 
 ### 7. Equality and decidability
 - **No `Eq` superclass** on algebraic classes. It would exclude function types, and structural `Eq` on symbolic types would falsify the laws; `Double` isn't lawful anyway. `Num` lost `Eq`/`Show` in GHC 7.4.
   - Document each instance's intended equality. Skip `Setoid`; property tests carry their own constraints.
 - **The zero test isn't algebraic** (ℚ and computable reals are both fields).
   - It says zero is an *isolated point*, equivalently `a ≅ 1 + NonZero a`, which is `nonZero`'s type.
   - It equals decidable equality given subtraction or monus, and is weaker otherwise (ℕ∞).
   - A division semiring with a zero test is a *discrete division rig*, R = {0} ⊔ R^×. The alternative reads "nonzero" as apartness (Heyting).
   - Mathlib's `withZeroUnitsEquiv` needs exactly a decidable zero.
   - It lives in `IsZeroIsolated`, beside equality, with the splitting as its law. `IsDiscreteDivisionSemiring` is a synonym.
   - The addition-free precondition for `NonZero a` being a group is `GroupWithZero`, which needs its own `zero` class, as Lean has `Zero`.
 - **Lean's approach:**
   - `Decidable p` is a proof-carrying Bool; `DecidableEq`/`Pred`/`Rel` are abbreviations for families of it.
   - Lawless `BEq` and `Ord` get law mixins: `PartialEquivBEq`, `ReflBEq`, `EquivBEq`, `LawfulBEq`, `LawfulHashable`, `TransOrd`, `LawfulEqOrd`.
   - Mathlib adds classical `DecidableEq` for ℝ and `Set`.
 - **Recommendations:**
   - Decisions return evidence, as splittings into refinement types (detachable subsets); `Bool` versions are secondary.
   - Split equality into a lawless `==` plus an equivalence mixin and a lawful (substitutive) mixin.
     - IEEE `==` is only a partial equivalence.
     - For `Double` in containers, use a strict-equality newtype, like Scala's `StrictEquiv`.
   - Treat ordering the same way.
   - Give no instance where equality is undecidable; at most offer one-sided evidence tests.
   - Precedents: base's `TestEquality`, singletons' `Decision`.
 
 ### 8. Commutativity and operators
 - **Non-commutative addition** is allowed, as in Lean, though Lean's main payoff (`to_additive`) has no Haskell analogue.
 - **Commutativity** gets one class, `IsAddCommSemigroup`, plus synonyms `IsAddCommMonoid` and `IsAddCommGroup`.
 - **Aliases:** an operator takes the constraint of the method it aliases, so `(+)` needs `IsAddSemigroup`.
 - **Consequences:**
   - Code that relies on commutativity must state it.
   - `Semiring` and `Module` superclasses use the `Comm` versions.
 
 ### 9. Ordered structures
 - **Pattern:** an ordered X is an X-object in the ordered counterpart of the category X is presented in.
   - (Set, ×) becomes (Pos, ×).
   - (Ab, ⊗) becomes (OAb, ⊗), whose nonnegative cone is generated by products of nonnegatives. OAb is closed, its internal hom contains all homomorphisms with the monotone ones nonnegative, and preorders are used throughout.
   - Properties, like having inverses, stay properties.
 - **Resulting definitions:**
   - Ordered monoid: a monoid in Pos.
   - Ordered group: a monoid in Pos that's a group. A group object in Pos is discrete.
   - Ordered ring: a monoid in OAb. A rig object in Pos that's a ring is discrete.
   - Ordered modules and algebras: likewise, in OAb.
   - Ordered rigs: use Mathlib's definition (monotone multiplication by nonnegatives, 0 ≤ 1), so ordered rings are ordered rigs.
 - **Laws:**
   - Structure maps are monotone, or positive bimorphisms.
   - Antitone laws are theorems about derived operations (negation, `recip`, subtraction, division) and belong on the ordered-structure mixin. Field `recip` is antitone only within each sign.
   - Strict and reflecting variants exist. Mathlib calls them `AddLeftMono`, `AddLeftStrictMono`, `AddLeftReflectLE`; its older "contravariant" means *reflecting*.
 - **Mixins** are per operation (Mathlib's 2025 unbundling): additive monotonicity; multiplicative monotonicity (not for rings); ordered semiring, plus a strict version. An ordered ring's multiplicative monoid is not an ordered monoid.
 - **Canonical orders** (ℕ, ℝ≥0, multisets) are where monus lives, as an adjoint (`OrderedSub`).
 - **Trichotomy** needs only a linear order and a zero (`SignType.sign`). In ordered groups, sign and `compare` are interdefinable.
   - `Positive a` is closed under + in ordered monoids and under * in strictly ordered semirings; in ℕ it equals `NonZero`.
 - **Earlier drafts:** a fuzzy "variance recipe" and a polarity formulation came first. The pattern above supersedes them.
 
 ### 10. "Is a group", categorically
 - Being a group is a property, so groups form a full subcategory.
 - **U-group:** an inverse exists in D after applying a product-preserving U: C → D.
 - **Shear map:** an isomorphism gives a group object; mono plus epi (a bijection) gives an ordered group.
 - **Units counit** of V ⊣ Inv: an isomorphism gives a group object (discrete); an epimorphism gives an ordered group.
 - The gap exists because Pos isn't balanced. Top shows the same split: topological vs. paratopological groups (the Sorgenfrey line). Ordered groups are paratopological in the up-set topology.
 - Group completion inside Pos collapses comparable elements: ordered ℤ completes to the trivial group.
 - `negate` is the witness of the property, with no monotonicity law.
 
 ### 11. Naming scheme (final version)
 - **Constraints:** never contradict convention, and make monoid-like structures the unmarked default.
 - **Roots:** `Monoid`; `Rig` (commutative additive monoid, multiplicative monoid, distributive, absorbing 0).
 - **Removing a default:** `NonUnital`, `NonAssoc`.
 - **Adding a feature:** `Comm`, `Idem`, `Inv` (division, so loops and quasigroups fit), `Neg` (additive inverses), `Div` (nonzero reciprocals), `WithZero`.
 - **Constructors:** `…oid`, `…Action`, `…Algebra`. A leading `Add`/`Mul` names the operation.
 - **Order:** `[Add|Mul][Comm][Idem][NonAssoc][NonUnital][Neg][Div][Inv]Root[WithZero][oid|Action|Algebra]`.
 - **Translations:**
   - group = `InvMonoid`; semigroup = `NonUnitalMonoid`; magma = `NonAssocNonUnitalMonoid`.
   - loop = `NonAssocInvMonoid`; quasigroup = `NonAssocNonUnitalInvMonoid`.
   - band and semilattice use `Idem`; group with zero = `DivMonoidWithZero`.
   - category = `Monoidoid`; semicategory = `NonUnitalMonoidoid`; groupoid = `InvMonoidoid`.
   - rg = `NonUnitalRig`; rng = `NonUnitalNegRig`; ring = `NegRig`.
   - division semiring = `DivRig`; semifield = `CommDivRig`; division ring = `NegDivRig`; field = `CommNegDivRig`.
   - ringoid = `NegRigoid`.
   - semimodule, module, vector space = `RigAction`, `NegRigAction`, `CommNegDivRigAction`.
   - semialgebra = `CommRigAlgebra`; algebra = `CommNegRigAlgebra`.
 - **Notes:**
   - Conventional names can stay as aliases.
   - Collapsed combinations: `NonUnitalInvMonoid` needs no name, and a module's negatives are forced.
   - The first draft (`Semi` = "no division", making `SemiGroup` mean monoid) was rejected.
 
 ### 12. Structures with several operations
 - **Absorption:**
   - It's the empty-sum case of distributivity: monoid homomorphisms must be told to preserve 0. That's also why rng maps can send 1 to idempotents.
   - Beck's distributive law: a product of sums is a sum of products, so an empty factor gives the empty sum.
   - Near-rings have absorption on their distributive side only.
   - Without it, the identity matrix and the polynomial 1 aren't units, and sparse representations are unsound.
   - In `Rig`, state `mul a zero = zero = mul zero a`; in `NegRig` it's a theorem.
 - **Cayley pattern:** rigs are subrigs of End(commutative monoid), and each axiom reflects that.
   - Addition must be commutative for pointwise sums of endomorphisms to be endomorphisms.
   - The same template: monoids = End(set), groups = Aut(set), rings = End(Ab), near-rings = functions on a group, modules = homomorphisms into End.
 - **Kinds of compatibility:**
   - distributivity (tensor);
   - interchange, which by Eckmann–Hilton forces equal, commutative operations;
   - lattice absorption (one order);
   - compatibility with extra structure.
 - **Why require compatibility:**
   - normal forms (the free rig is ℕ⟨X⟩);
   - homomorphic evaluation;
   - generic algorithms, such as dynamic programming over semirings.
 - **Non-commutative addition:**
   - It's not a monoid in (Mon, ×), which gives commutative monoids.
   - Two-sided distributivity works only without cancellation (example: {0, 1, t}); some literature says "additively commutative semiring" when assuming it.
   - The natural notion is the one-sided near-semiring (seminearring). Its Cayley model is functions on a monoid; examples are ordinals and `Alternative`/`MonadPlus`.
   - Keep additive commutativity in `Rig`.
 
 ### 13. Monoids in monoidal categories, precisely
 - **Notation:** base (V, ⊗, I, σ). Mon(V, ⊗) and CMon(V, ⊗) name the product explicitly: Mon(Ab, ×) ≃ Ab, but Mon(Ab, ⊗_ℤ) = rings.
 - **Examples:**
   - Mon(Set, ×): monoids. Mon(Pos, ×): ordered monoids. Mon(Top, ×): topological monoids.
   - Mon(Ab, ⊗_ℤ): rings. Mon(CMon, ⊛): rigs. Mon(Vect, ⊗_k): algebras.
   - Mon(End(C), ∘): monads.
 - **Free objects:** lists ∐X^⊗n and bags ∐X^⊗n/Σₙ.
 - **Products on C = Mon(V, ⊗) or CMon(V, ⊗):**
   - ⊗ᶜ, componentwise (needs σ). It's × for cartesian V, and the coproduct on CMon.
   - ⊔, the coproduct (free product), whose unit is the initial monoid.
   - ⊛, bilinear. It needs a commutative theory over a cartesian closed V with colimits. It's a quotient of the free model on M × N, and its unit is the free model on one generator.
   - On CMon: × = ⊗ᶜ = ⊔ (a biproduct), and ⊛ is the tensor of commutative monoids. On Ab, ⊛ = ⊗_ℤ.
 - **Their monoids:**
   - Mon(Mon(V, ⊗), ⊗ᶜ) ≃ CMon(V, ⊗) by Eckmann–Hilton.
   - Mon(C, ⊔) ≃ C.
   - Mon(Mod_T, ⊛) gives:
     - sets → monoids;
     - pointed sets → monoids with zero;
     - commutative monoids → rigs;
     - abelian groups → rings;
     - join-semilattices with 0 → idempotent semirings;
     - sup-lattices → quantales;
     - R-modules → R-algebras.
   - Commutative monoids for ⊛ give the commutative versions. Over Pos, ⊛ gives rig objects in Pos; ordered rings came from the cone tensor instead.
 - **Why monoids get no ⊛:** it needs a commutative theory. For monoids, interchange is the same as commutativity; the list monad isn't commutative, while the bag monad is.
 - **One-sided:** on End(C), composition ∘ distributes over the pointwise product ×. Near-semiring objects there are `MonadPlus`.
 
 ## Algebraic structures mentioned
 
 - **One operation:** magma, unital magma, quasigroup, loop, semigroup, monoid, group, abelian group, band, (bounded) semilattice, monoid with zero, group with zero, adjoined zero, units and additive units, zero-sum-free monoid, canonically ordered monoid, monus, semigroup/monoid/group actions, torsor, affine space.
 - **Two operations:**
   - Rings and rigs: ring, rng, rig/semiring, rg/hemiring, rig without zero, commutative ring/rig, non-associative ring, near-ring (zero-symmetric), near-semiring/seminearring, additively non-commutative semiring.
   - Domains: domain/integral domain, GCD domain, PID, UFD, Euclidean domain.
   - Division structures: division ring, field, division semiring, semifield/division rig, discrete and Heyting division rigs, meadow.
   - Characteristic: ℚ-algebra, characteristic zero and positive characteristic, finite field, ℤ/n.
   - Idempotent and order-like: idempotent, tropical (min-plus, max-plus) and Boolean semirings, star semiring, quantale, lattice, Boolean algebra, residuated lattice, join-semilattice with 0, sup-lattice.
 - **Module-like:** left/right module, semimodule, vector space, representation, associative algebra, semialgebra, R-algebra, monoid/group algebra, Lie algebra, octonions.
 - **Ordered and topological:** preordered, ordered, linearly ordered and strictly ordered versions of semigroups, monoids, groups (bi- and left-ordered), abelian groups, semirings, rings, fields, modules, vector spaces and algebras; positive cones; group objects in Pos; topological monoids; topological and paratopological groups.
 - **Categorical:** monoid, commutative monoid and group objects; category (monoidoid); semicategory; groupoid; core; ringoid; rigoid; rig (bimonoidal) category; monads; near-semiring objects (`Alternative`, `MonadPlus`); F-algebras and coalgebras; algebras for a monad; commutative theories and monads (bag vs. list); pointed sets with smash product; ringed spaces.
 - **Examples:** ℕ, ℕ₊, ℕ∞, ℤ, ℚ, ℚ≥0, ℝ, ℝ≥0, ℂ, ordinals, polynomials, power series, matrices, quaternions, dual numbers, pointwise functions, computable reals, `Int`/`Word` (ℤ/2ⁿ), `Double`, `Bool`, permutations, valuation targets, multisets, sets, End(M), the {0, 1, t} rig, the Sorgenfrey line.
 
 # Algebraic Structures/Abstractions Useful in FP
 
 **Rule of thumb:** algebra pays off in FP when it gives you one of three things:
 - laws you can program against, which license folds, parallelism, incrementality, rewrites and property tests;
 - homomorphisms and free/quotient constructions;
 - order and fixpoint theory.
 
 Classification theory almost never pays off.
 
 **Cosets and ideals:** rarely used as such. What transfers is the general notion behind them: congruences and quotients (cosets are congruence classes; normal subgroups and ideals are kernels), plus orbits. Concrete cosets are elements of ℤ/n and syndrome decoding of linear codes. Ring ideals matter through quotient rings (§5). Order ideals (down-sets) matter in lattices and CRDTs (§7). Semigroup ideals show up as absorbing elements (§1).
 
 ### 1. Extra laws on the basics
 - **Commutativity** → order-independent reduction: `HashMap`/bag folds that respect equality, and parallel partial results combined in completion order. Commutative effects can be reordered or batched (Haxl), and give exchangeability in probabilistic programs (Staton).
 - **Idempotence** (bands; plus commutativity = **semilattices**) → merging that tolerates duplicates and retries: state-based CRDTs, LVars, Datalog/Datafun, `Min`/`Max`, `First`/`Last`.
 - **Absorbing elements** → early exit from folds (`Any True`, `All False`, `0`); `empty <*> x = empty` → pruning in search.
 - **Cancellative, GCD and monus monoids** (`monoid-subclasses`) → `stripPrefix`/`isPrefixOf` for any monoid, parsers over any monoidal input (picoparsec), and multiset/`Natural` subtraction.
 - **Involutions/anti-homomorphisms** → `Dual . reverse` is a monoid iso `[a] → Dual [a]`; dagger and inverse categories model reversible and quantum languages.
 - **Near-semirings** → the actual laws of `Alternative`/`MonadPlus` (Rivas–Jaskelioff–Schrijvers).
 - **Closed (star) semirings, Kleene algebra (with tests)** → one matrix-closure algorithm gives shortest/widest paths, reachability, path counting and automaton→regex, just by swapping the semiring (Dolan, *Fun with Semirings*). Also: regex derivatives, semiring parsing (Goodman), provenance semirings, KAT/NetKAT verification.
 - **Graded monoids/rings** → `(++) :: Vec n a → Vec m a → Vec (n+m) a`; graded monads; units of measure (a ring graded by the dimension group).
 - **Preordered monoids/semirings** → effect systems via graded monads with subeffecting (Katsumata); usage multiplicities in QTT/Idris 2 ({0,1,ω}), Linear Haskell and Granule.
 - **Caveat:** IEEE `+`/`*` are only commutative magmas, so parallel float sums aren't reproducible and `Double` instances are only approximately lawful.
 
 ### 2. Universal algebra (biggest payoff after the basics)
 - **Homomorphisms** → `foldMap f` is the unique monoid hom out of the free monoid. Homs parallelize (third homomorphism theorem, Gibbons) and justify fusion and GHC `RULES`. Monad morphisms give the laws for `lift` and `hoist`. `Traversable`'s naturality law quantifies over applicative homs.
 - **Free algebras** → the Boom hierarchy: free magma = leaf trees; add associativity = `NonEmpty`; add a unit = lists; add commutativity = bags; add idempotence = finite sets.
   - Free group = reduced words.
   - ℕ[X] = the universal provenance semiring.
   - Free monads, applicatives and categories, with effect handlers = homs out of them (Plotkin–Pretnar).
 - **Initial algebras / final coalgebras** → ADTs and folds (recursion schemes); codata, streams and bisimulation.
 - **Presentations / equational theories** → algebraic effects = operations + equations (Plotkin–Power); Knuth–Bendix and rewriting; unification modulo AC/AG (F# units-of-measure inference, Maude, Tamarin).
 - **Birkhoff's HSP theorem** → equational laws survive products, subalgebras and quotients. So tuple and pointwise (`a -> b`) instances are lawful for free, and invariant-preserving newtypes inherit laws. Non-equational axioms don't survive:
   - Fields aren't a variety: there is no free field, and pointwise `Fractional (a,b)` is unlawful because `(1,0)` has no inverse.
   - Cancellativity isn't preserved by quotients.
   - This is why `Group` makes `invert` an operation.
 - **Subalgebras** → a smart-constructor invariant is sound iff it is closed under every exported operation.
 - **Congruences and quotients** → `Eq` on an abstract type must be a congruence for its API. Also: quotient types (Lean `Quot`, cubical HITs, setoids), and e-graphs, which are incremental congruence closure. The 1st isomorphism theorem says you can represent A/ker f by im f, which is how normal forms work (sorted lists or `Map a Int` for bags, reduced words for free groups).
 - **Cayley's theorem** → difference lists (`Endo`), `Codensity` for monads (Rivas–Jaskelioff), CPS. All three reassociate for asymptotic speedups.
 - **Semidirect products** → pair a value with the transformation acting on it: diagrams (Yorgey, *Monoids: Theme and Variations*); rolling hashes and CRCs combine as affine maps x ↦ x·Bⁿ + h.
 
 ### 3. Actions, torsors, automata
 - **Monoid actions** → update monads (Ahman–Uustalu); change actions/structures for incremental computation and semi-naïve Datalog (Alvarez-Picallo et al.; Cai et al.).
 - **Actions by homomorphisms** → lazy-propagation segment trees.
 - **Torsors / affine spaces** → points typed apart from differences: `UTCTime`/`NominalDiffTime`, pointer/offset (`vector-space`, `acts`).
 - **Transition monoids** → running a DFA is a hom into endofunctions on its states, which gives parallel/incremental lexing (Hillis–Steele; finger-tree measures).
 - **The bicyclic monoid** ⟨p,q ∣ pq=1⟩ → parallel bracket matching (Levien's "stack monoid").
 - **Orbits, stabilizers, Burnside** → quotient containers such as unordered pairs, bags and cycles (Abbott–Altenkirch–Ghani–McBride); species (Yorgey); symmetry reduction in search and model checking.
 - **Actions of monoidal categories** → profunctor optics are Tambara modules.
 
 ### 4. Groups and their "-oids"
 - **Inverses** → range queries from prefix sums or Fenwick trees need inverses; segment trees need only a monoid. Also subtract-on-evict sliding windows, and undo.
 - **(Free) abelian groups** → Z-sets in DBSP and differential dataflow (incremental view maintenance with ± weights); units of measure (Kennedy).
 - **Cyclic groups** → wraparound indices, ring buffers (`Finite n`, `Mod m`).
 - **Symmetric groups** → permutations as invertible first-class data, axis transposes, species.
 - **Semigroupoids, categories, groupoids** (typed semigroups, monoids and groups) → the `semigroupoids` package; patches (Darcs; homotopical patch theory); HoTT identity types; isos.
 - **Inverse semigroups** (partial bijections) → partial isomorphisms for invertible parser/printers (Rendel–Ostermann); reversible computing.
 - **Trace (partially commutative) monoids** → Mazurkiewicz traces and partial-order reduction; scoped-label rows (Leijen; Koka effect rows).
 
 ### 5. Rings and ideals
 - **Quotient rings in daily use:**
   - ℤ/2ⁿ is wrapping `Word`/`Int`: a lawful ring, unlike `Double`. Odd numbers are units, which gives bijective hash mixers (SplitMix) and exact division by constants.
   - ℤ/n with CRT and Fermat/Euler (Lagrange in the unit group) → modular types, multi-modular/NTT arithmetic, hashing.
   - 𝔽₂[x]/(p) = GF(2ⁿ) → CRC (reduction is a ring hom, which gives `crc32_combine` and parallel CRC), Rabin fingerprints, Reed–Solomon, AES. The quotient is a field iff (p) is maximal iff p is irreducible.
   - ℝ[ε]/(ε²) = dual numbers → forward-mode AD; ℝ[ε]/(εᵏ⁺¹) → Taylor-mode AD.
 - **Euclidean/GCD domains** → `semirings`' `GcdDomain`/`Euclidean`; generic extended gcd; canonical `Ratio`.
 - **Fields of fractions** → `Ratio a`, rational functions.
 - **Polynomial, power-series and monoid (semi)rings** → lazy power series (McIlroy). Convolution over a monoid unifies polynomials, languages and weighted automata (Elliott, *Generalized Convolution*).
 - **Noetherianity / ACC** → termination arguments: Kleene iteration terminates under ACC (otherwise you need widening), and Dickson/Hilbert make Buchberger's algorithm terminate.
 
 ### 6. Modules & linear algebra
 - **Free semimodule monad** (finite S-weighted sums) → one monad with many semantics, depending on S:
   - 𝔹 → nondeterminism
   - ℕ → multisets
   - ℝ≥0 → probability (distributions are free convex algebras)
   - tropical → optimization
   - ℂ → quantum amplitudes
 - **Matrices over semirings** → graph algorithms as linear algebra (GraphBLAS); weighted automata.
 - **Duals and transposes** → reverse-mode AD is transposed linearization (JAX, *You Only Linearize Once*; Elliott, *Simple Essence of AD*).
 - **𝔽₂-linear algebra** → XOR bases, linear codes.
 - **Tensor products, inner products, spectral theory, canonical forms, exterior/Clifford algebras** → numerics, ML and graphics only. Tensor products do serve as the model for monoidal products (§8).
 
 ### 7. Order theory
 - **Complete lattices + Knaster–Tarski/Kleene** → semantics of recursion, dataflow analysis, Datalog, grammar analyses (nullable/FIRST).
 - **CPOs/domains** → semantics of laziness, ⊥ and general recursion.
 - **Galois connections** → abstract interpretation; calculating `floor`, integer division and integer sqrt (Backhouse; Mu–Oliveira).
 - **Distributive lattices, Birkhoff representation, down-sets** → causal histories and version vectors; join-irreducible decompositions for optimal delta-CRDT sync (Enes et al.).
 - **Boolean algebras** → bitsets, predicates, BDDs; set-theoretic types (CDuce, Elixir).
 - **Heyting algebras** → the intuitionistic logic of types.
 - **Security lattices** → information-flow control (LIO, MAC).
 - **Well-founded orders, WQOs, ordinals** → termination checking; homeomorphic embedding (Kruskal) as supercompilation's termination test.
 - **Quantales** → quantitative/metric semantics (niche).
 
 ### 8. Categorified algebra (where all of the above resurfaces)
 - **Monoid objects:**
   - `Monoid` under ×
   - `Applicative` under Day convolution
   - `Monad` under composition
   - `Category`/`Arrow` in profunctors
   - `Alternative` as a monoid on `f a`
   - `Divisible`/`Decidable` as the contravariant versions
 - **Comonoids** → trivial in Hask, explicit under linearity (`linear-base`'s `Dupable`/`Consumable`).
 - **Eilenberg–Moore algebras** → monoids are list-monad algebras, convex sets are distribution-monad algebras; effect handlers.
 - **The rig of types up to iso** → "algebraic" data types, refactoring by algebra, zippers as derivatives and dissections (McBride); the reversible language Π as rig-groupoid isos (James–Sabry; Carette–Sabry).
 - **Distributive laws** (Beck) → when monads compose; `traverse`.
 - **Adjunctions** → free ⊣ forgetful underlies every "free X" above; `State` comes from currying.
 
 ### 9. Little or no use
 These have little or no use:
 - Sylow theory, p-groups and the class equation
 - simple, solvable and nilpotent groups; composition series
 - the 2nd and 3rd isomorphism theorems
 - structure theorems for abelian groups and PID-modules; Jordan and rational canonical forms
 - field extensions and Galois theory
 - representation theory and Lie theory
 - homological algebra, most commutative algebra, algebraic geometry
 - subdirect representation, quasigroups
 - Green's relations and Krohn–Rhodes; Hopf algebras
 
 **Why:** these classify or decompose structures rather than supplying laws to program against, so they license no generic algorithm, data structure or rewrite.
 
 **Domain-specific exceptions:**
 - characters of finite abelian groups → FFT, NTT, Walsh–Hadamard
 - quaternions and SO(3) → graphics and robotics
 - Schreier–Sims → symmetry breaking (nauty)
 - Hermite and Smith normal forms → polyhedral compilation
 - Gröbner bases → computer algebra, nonlinear SMT, invariant generation
 
 I can turn this into a Doc if you want an editable catalogue.