liftToQuotient
plain-language theorem explainer
The liftToQuotient definition supplies the induced map from the recognition quotient C_R to any type X for any function f : C → X that is constant on indistinguishable configurations. Researchers constructing observable invariants in recognition geometry cite it to descend maps to equivalence classes. The implementation is a direct one-line wrapper around Mathlib's Quotient.lift.
Claim. Let $r$ be a recognizer from configurations $C$ to events $E$. For any function $f : C → X$ and proof $hf$ that $f(c_1) = f(c_2)$ whenever $r(c_1) = r(c_2)$, the descended map $C_R → X$ satisfies $liftToQuotient(r, f, hf)([c]) = f(c)$ for the class $[c]$ in the quotient.
background
The recognition quotient $C_R$ is the quotient of configuration space $C$ by the indistinguishability relation, where two configurations are equivalent precisely when they yield the same event under recognizer $r$. Indistinguishable $r$ $c_1$ $c_2$ is defined as $r.R(c_1) = r.R(c_2)$, and RecognitionQuotient $r$ is Quotient of the corresponding setoid. This collapses configurations that produce identical observations, so maps on the quotient represent properties of observable classes only.
proof idea
The definition is a one-line wrapper that applies Quotient.lift to the supplied function $f$ and the hypothesis $hf$ that $f$ respects indistinguishability.
why it matters
This definition supplies the mechanism for well-defined maps on the recognition quotient. It is invoked by liftToQuotient_spec to confirm the projection identity and by quotient_status to record that the quotient and its event map together capture exactly the observable structure. The construction supports descent of invariants in the recognition geometry module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.