universal_property
plain-language theorem explainer
Recognition Geometry's universal property theorem asserts that for any recognizer the recognition quotient map is surjective, the induced event map is injective, and the recognizer factors through the quotient. Researchers establishing canonicity of the quotient construction cite it to justify that the recognition quotient is the finest such structure. The proof is a direct term-mode construction that invokes a representative existence lemma for surjectivity, applies the supporting injectivity lemma, and uses reflexivity for factorization.
Claim. Let $C$ be a configuration space and $E$ an event space. For any recognizer $r$ from $C$ to $E$, the recognition quotient map is surjective, the quotient event map is injective, and $r$ equals the composition of the quotient event map with the recognition quotient map.
background
A configuration space carries an empty configuration, a commutative join operation, a consistency predicate, and an independence relation, per the ConfigSpace class definition. An event space supplies the codomain for recognizers. The module states the three pillars of Recognition Geometry, with the first asserting that the recognition quotient captures exactly the observable distinctions via the equivalence that two configurations are identified precisely when the recognizer assigns them the same event value.
proof idea
The proof is a term-mode refinement of a triple. Surjectivity follows by obtaining a representative configuration from any quotient element via the existence lemma for quotients and verifying the mapping definition. Injectivity of the quotient event map is supplied directly by the lemma quotientEventMap_injective. The factorization identity holds by reflexivity.
why it matters
This theorem realizes the universal property of the recognition quotient as the canonical coequalizer of the indistinguishability relation. It feeds the quotient_uniqueness corollary, which extracts surjectivity and injectivity to conclude uniqueness up to isomorphism. In the framework it underpins the pillar that the quotient determines observables and aligns with the fundamental theorem equating quotient classes to equal recognition values. It touches the open question of fully developing the category of quotients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.