quotientMapLeft_surjective
plain-language theorem explainer
Surjectivity of the projection from the composite recognition quotient onto the left component quotient follows from the existence of representatives in quotients. Researchers formalizing how paired measurements produce finer partitions of configuration space cite this to establish refinement. The argument constructs a preimage by applying the canonical projection to a representative of the target class.
Claim. Let $r_1$ and $r_2$ be recognizers on configuration space $C$. The natural projection from the quotient space induced by the composite recognizer $r_1 ⊗ r_2$ to the quotient space induced by $r_1$ is surjective.
background
Recognition geometry equips a configuration space $C$ with recognizers that induce equivalence relations via indistinguishability. The composite recognizer pairs outputs of $r_1$ and $r_2$, yielding a finer relation whose quotient admits natural projections to each factor quotient. The left projection is obtained by lifting the canonical map using the refinement property that the composite distinguishes at least as much as $r_1$ alone.
proof idea
The term proof takes an arbitrary class $q$ in the target quotient, extracts a representative configuration via the existence of representatives, and applies the canonical projection for the composite recognizer to that configuration; reflexivity verifies that the image recovers $q$.
why it matters
This supplies the left half of the refinement theorem, the central result of the composition module, which asserts that the composite quotient refines both component quotients via surjective maps. The module states that combining recognizers produces a finer view of configuration space, supporting the emergence of richer geometry from simpler measurements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.