Learn · Algebra
Axeyum for algebraists
Axeyum has a checked structure hierarchy and concrete algebraic instances, with quotient-based algebra as a clear next frontier.
a103b3db3 Measured Source Axeyum fact ledger and implementation documentation After reading this guide, you should be able to
Learning objectives
- Identify the parts of Axeyum that are relevant to algebra.
- Distinguish implemented results from the current research frontier.
- Open a lesson or artifact that provides the underlying definitions and evidence.
Current state
How much abstract algebra is available over the constructed carriers?
The kernel library defines structures from magmas through fields and supplies concrete operations and laws for natural numbers, integers, rationals, constructed reals, and complex numbers. It also contains finite modular groups and symmetric groups on finite functions.
The kernel implements Quot, Quot.mk, Quot.lift, and Quot.ind, but it does not declare Quot.sound. This supports elimination from quotient representatives without making related representatives equal. The distinction is visible in the trusted surface instead of being hidden in a library convention.
Why it matters
What the current work makes possible
- The same kernel checks both the abstract laws and their concrete carrier instances.
- Complex numbers are built as a pair setoid over constructed reals with an empty footprint.
- The limited quotient interface provides a precise test case for the foundations of quotient algebra.
Results to inspect
Open the evidence
What comes next
Extend the present base
The next layer is quotient groups, ideals, polynomial rings as algebraic structures, modules, field extensions, group actions, and Galois theory.
Progress starts with a deliberate decision about equality for quotient objects. A setoid-based route and a stronger quotient primitive have different proof and trust costs, and Axeyum can record those costs explicitly.
Where to begin