commit fac468b1a468da013d460b8b7d8ce1cbb47545e4
parent 89e6d8e2f0a2a924da32230a201e5f6238ddbe36
Author: Robert Russell <robert@rr3.xyz>
Date: Thu, 24 Sep 2026 09:30:25 -0700
Todo: add slop Claude transcript
Diffstat:
| A | Todo/Algebra.slop.md | | | 234 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
1 file changed, 234 insertions(+), 0 deletions(-)
diff --git a/Todo/Algebra.slop.md b/Todo/Algebra.slop.md
@@ -0,0 +1,234 @@
+## 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.
