Ideals in Balanced Algebras: the Gregarious IdealResearch Paper
## Motivation A recurring pattern in algebra is that a structure is analysed through distinguished subobjects — normal subgroups, ring ideals, submodules — and that requiring those subobjects to be trivial isolates the sharply defined classes (simple groups, division rings, simple modules) about which the deepest theorems are available. The manuscript *Ideals in Balanced Algebras and the Genesis of Mathematics* (A. Winkler, 2020) applies that pattern to a single primitive: a **partial binary operation**, an operation $a\cdot b$ that need not be defined for every pair. Under one axiom — **balance**, which asserts that $(ab)c$ is defined exactly when $a(bc)$ is — several families of ideals appear automatically, and declaring each of them trivial (empty, or the whole algebra) carves out semigroups, monoids, quivers, associations, societies, categories, groupoids, groups and rings in turn. No individual argument here is deep. What makes them worth machine-checking is that their content is *definedness* rather than equality: a statement such as "the gregarious elements form an ideal" is a claim about which products exist, proved by repeatedly moving brackets across a product that may fail to be defined at any step. Such arguments are easy to state loosely, and easy to get wrong by one implicit existence assumption. They are also the base layer on which the rest of the manuscript's programme rests. This mission formalizes that base layer: §1 (algebras, ideals, units), §2 (quivers), §4 (associators and associations), §4.1 (principal ideals) and §4.2 (the gregarious ideal). ## Setting An **algebra** on a type $A$ is a partial binary operation: a rule assigning to some pairs $(a,b)\in A\times A$ a value $a\cdot b\in A$. Write $a\cdot b\downarrow$ for "$a\cdot b$ is defined". In the Lean development the operation is a total function $A\to A\to\mathrm{Option}\,A$, where the value $\mathrm{none}$ means undefined. Nothing else is assumed: no totality, no unit, no associativity. The vocabulary used throughout, all relative to this one partial product: 1. $B\subseteq A$ is a **left ideal** if $a\cdot b\in B$ whenever $b\in B$ and $a\cdot b\downarrow$; a **right ideal** if $b\cdot a\in B$ whenever $b\in B$ and $b\cdot a\downarrow$; a **subalgebra** if $b\cdot c\in B$ whenever $b,c\in B$ and $b\cdot c\downarrow$. 2. The **right orbit** of $a$ is $aA=\{c:\exists b,\ a\cdot b=c\}$; the left orbit is dual. 3. The algebra is **balanced** if, for all $a,b,c$, $(a\cdot b)\cdot c$ is defined if and only if $a\cdot(b\cdot c)$ is. 4. $u$ is a **left unit** if $u\cdot a=a$ whenever $u\cdot a\downarrow$, and $v$ is a **right unit** if $a\cdot v=a$ whenever $a\cdot v\downarrow$. A left unit $u$ is a **source** if $a\cdot u\downarrow$ only for $a=u$; a right unit $v$ is a **sink** if $v\cdot b\downarrow$ only for $b=v$. 5. $b$ is **associating** if for all $a,c$ the product $(ab)c$ is defined exactly when $a(bc)$ is, and the two values agree whenever both are defined. An **association** is an algebra all of whose elements are associating. 6. $b$ is **gregarious** if, whenever $a\cdot b\downarrow$ and $b\cdot c\downarrow$, at least one of $(ab)c$ and $a(bc)$ is defined. An association that coincides with its set of gregarious elements is a **society**; in the manuscript's terms, a quivered society is a category. 7. $b$ is **left cancellable** if $b\cdot x=b\cdot y$, with both sides defined, forces $x=y$. ## Formalization targets ### Goal — the gregarious ideal (§4.2) $$\text{If } A \text{ is an association, then } \{\,b\in A: b \text{ is gregarious}\,\} \text{ is both a left ideal and a right ideal.}$$ This is the statement that gives the manuscript its notion of *society*: the gregarious elements of an association form the **gregarious ideal**, and an association whose gregarious ideal is everything is a society. The goal fixes no cardinality, no units and no totality, so it survives every specialization the manuscript makes afterwards. ### Supporting targets The milestone list works up to the goal through the manuscript's own intermediate claims: the orbit characterization of right ideals and the elementary facts about units (§1); the two derived quiver identities (§2); closure of the associating elements under the product (§4); principal right ideals (§4.1); gregariousness of sinks and sources, and the two one-sided closure statements for gregarious associating elements (§4.2); and the cancellation facts (§4) whose content is that the non-left-cancellable elements form a prime left ideal. ## Significance The result itself gives the manuscript's structural dichotomy a stable base. Once the gregarious elements are known to form an ideal, "society" is a triviality condition on an ideal rather than an ad hoc axiom, and the same is true of *quivered* (the elements admitting a unit on one side form an ideal, §1), of *cancellative* (the non-cancellable elements form a prime ideal, §4) and of *principal* (§4.1). The chain of specializations the manuscript then runs — association, society, quivered society, category, groupoid, group, ring — inherits whatever is proved here. What this mission adds on top of the manuscript is machine-checked bookkeeping for partial operations. The arguments in the source are written in prose, with the existence of intermediate products often left implicit; formalizing them fixes exactly which existence facts each step consumes. The definitions published with this mission (partial algebra, ideal, balance, associating, gregarious, unit, source, sink, cancellable) are reusable for any later formalization of partial magmas, and nothing equivalent is currently in Mathlib, whose `Magma`-style structures are total and whose `Quiver`/`Category` hierarchy starts from typed hom-families rather than a single partial product. ## Difficulty The obstacle is uniform and easy to underestimate: in a partial algebra one may never assume that a product written down in the course of an argument exists. The naive proof of the goal — "rebracket and apply gregariousness of $b$" — fails at its first step, because from $a\cdot(bc)\downarrow$ alone one cannot conclude $a\cdot b\downarrow$; that inference is exactly what the hypothesis "$b$ is associating" supplies, and it must be invoked explicitly. Gregariousness then returns a disjunction whose two branches produce products on opposite sides of the bracket, so each branch has to be transported back independently, consuming a further associating hypothesis. Counting these obligations correctly, rather than inventing new mathematics, is the work. ## Formalization scope The partial product is `A → A → Option A`; `none` is undefined, and `a · b = c` is rendered as the product evaluating to `some c`. Subsets are `Set A`, with no decidability or finiteness assumptions. Ideals are arbitrary subsets and are allowed to be empty — deliberately, since the manuscript's dichotomy turns on an ideal being empty or being everything. Statements quantify over an arbitrary type, including the empty type, where they hold vacuously. Left/right duality is not obtained from a formal opposite-algebra construction: the dual statements are stated and are to be proved separately (for instance the two one-sided society closure milestones). A contributor who prefers to build the opposite algebra once and derive each dual from its mirror is welcome to; that construction is not part of the published definitions. The statements are not vacuous: every hypothesis used is satisfiable, since any total associative operation makes all elements associating and gregarious, and the trivial one-element monoid satisfies every unit, source, sink and cancellation hypothesis appearing in the list. No milestone is stated under a hypothesis that cannot be met. ## Selected references - A. Winkler, *Ideals in Balanced Algebras and the Genesis of Mathematics*, manuscript, 20 March 2020. Source text supplied by the mission owner; section and page references in the items below are to that manuscript. - S. Eilenberg and S. Mac Lane, *General theory of natural equivalences*, Transactions of the American Mathematical Society 58 (1945), 231–294. https://doi.org/10.1090/S0002-9947-1945-0013131-6