ℤ as a Form — Initial Ring and Grothendieck group of ℕ. More...

#include <functional>
#include <type_traits>
import dedekind.algebra:group;
import dedekind.sets;
import dedekind.category;

Include dependency graph for initial_ring.cppm:

Concepts
concept	dedekind::algebra::IsInitialRing
	`R` is the initial object in `Ring` — for every ring `S` there exists a unique ring homomorphism `R` `→` `S`.
concept	dedekind::algebra::IsGrothendieckGroup
	`G` is the Grothendieck group of the commutative monoid `M` — the free abelian group on `M`, equivalently the left adjoint of the forgetful functor `Ab` `→` `CMon` applied at `M`.

Variables
template<typename R>
constexpr bool	dedekind::algebra::is_initial_ring_v = false
	Opt-in trait: `R` is the initial object in the category of (commutative, unital) rings.
template<typename G, typename M>
constexpr bool	dedekind::algebra::is_grothendieck_group_v = false
	Opt-in trait: `G` is the Grothendieck group of the commutative monoid `M`.
template<>
constexpr bool	dedekind::algebra::is_initial_ring_v< SignedCardinality > = true
template<>
constexpr bool	dedekind::algebra::is_grothendieck_group_v< SignedCardinality, Cardinality >

Detailed Description

ℤ as a Form — Initial Ring and Grothendieck group of ℕ.

@partition :initial_ring

Copyright: 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

initial_ring__Two_Universal_Properties_For_ℤ

The categorical identity of ℤ has two textbook universal- property readings, both load-bearing for the project:

Initial object in Ring. For every (commutative, unital) ring R there exists a unique ring homomorphism χ_R : ℤ → R, sending 1_ℤ ↦ 1_R and determined uniquely by ring-axiom preservation. Reified as IsInitialRing<R>.
Grothendieck group of ℕ. ℤ is the free abelian group on the commutative monoid (ℕ, +, 0) — the left adjoint of the forgetful functor Ab → CMon applied at ℕ. Universal property: for every abelian group G and monoid homomorphism φ : ℕ → G, there exists a unique group homomorphism φ̂ : ℤ → G extending φ. Reified as IsGrothendieckGroup<G, M>.

initial_ring__Why_Reify_Both

The two readings are mathematically equivalent up to canonical isomorphism, but they sit in different categories ( Ring vs Ab) and bind to different operational consumers in the project:

The initial-object reading is what justifies χ_{Modular<n>} as a unique ring homomorphism (the mod-n reduction).
The Grothendieck reading is what the closure-forcing operator Cardinality - Cardinality → SignedCardinality (PR #433) realises operationally.

Reifying both as separate concepts gives the practitioner formal, type-checked documentation that SignedCardinality inhabits both Forms; downstream generic code can bind to whichever universal property is relevant for its argument.

initial_ring__Honesty_Obligation

Existence and uniqueness of the canonical homomorphisms remain the engineer's honesty obligation. C++ concepts cannot quantify universally over the target ring (in IsInitialRing) or the target abelian group (in IsGrothendieckGroup). What the type system pins is the structural shape — the carrier is a ring / abelian group of the appropriate kind, plus the opt-in trait that names it as the universal one. Witnesses on SignedCardinality exercise the universal property at one concrete target each (Modular<n> for the initial-ring side; Cardinality for the Grothendieck side) — the static_asserts pin the shape, the test suite pins the operational behaviour.

initial_ring__Architecture

Three-layer chain mirroring the NNO story (PR #447):

IsInitialRing → SignedCardinality → ℤ IsGrothendieckGroup<·, Cardinality> → SignedCardinality → ℤ

The first chain anchors the ring-side universal property; the second anchors the abelian-group-side universal property. Both land on the same carrier.

initial_ring__Bridge_to_Limit

IsInitialRing instantiates the same universal-property pattern that :limit's IsInitialObject<Zero> instantiates, just at a different categorical level — initial in the Ring category rather than initial in Set. The two readings live at different levels (forgetful functor U : Ring → Set does not preserve initial: ℤ is initial in Ring but its underlying set is not Zero = std::nullptr_t). A non-vacuous structural witness of this bridge requires reifying IsTerminalRing for the trivial / zero ring (whose carrier is One = std::monostate from :limit) — filed as a sibling concern; the static_assert here would be premature without the dual concept. See :f_algebra for the analogous bridge at the F-Alg category level.

Note: "Adjoint functors arise everywhere." — Saunders Mac Lane.

Variable Documentation

◆ is_grothendieck_group_v

template<typename G, typename M>

bool dedekind::algebra::is_grothendieck_group_v = false

inlineconstexprexport

Opt-in trait: G is the Grothendieck group of the commutative monoid M.

Default: false. Specialised to true on the canonical pair (SignedCardinality, Cardinality), registered downstream where both carrier types are visible.

Universal-property content (existence + uniqueness of the extension φ̂ : G → A for every abelian group A and monoid homomorphism φ : M → A) is the engineer's honesty obligation.

◆ is_grothendieck_group_v< SignedCardinality, Cardinality >

template<>

bool dedekind::algebra::is_grothendieck_group_v< SignedCardinality, Cardinality >

inlineconstexpr

Initial value:

=

true

◆ is_initial_ring_v

template<typename R>

bool dedekind::algebra::is_initial_ring_v = false

inlineconstexprexport

Opt-in trait: R is the initial object in the category of (commutative, unital) rings.

Default: false. Specialised to true on the canonical exact-ℤ carrier ( SignedCardinality, registered downstream where the carrier type is visible).

Universal-property content (existence + uniqueness of the canonical ring homomorphism χ_R : R → S for every ring S) is the engineer's honesty obligation. This trait is the type-system anchor: a carrier opts in, and downstream concept checks fire.

Concepts

Variables