theorem
proved
term proof
universal_property
show as:
view Lean formalization →
formal statement (Lean)
133theorem universal_property {C E : Type*} [ConfigSpace C] [EventSpace E]
134 (r : Recognizer C E) :
135 -- The quotient map is surjective
136 Function.Surjective (recognitionQuotientMk r) ∧
137 -- The event map on quotient is injective
138 Function.Injective (quotientEventMap r) ∧
139 -- R factors through the quotient: R = R̄ ∘ π
140 (∀ c, r.R c = quotientEventMap r (recognitionQuotientMk r c)) := by
proof body
Term-mode proof.
141 refine ⟨?_, quotientEventMap_injective r, ?_⟩
142 · -- Surjectivity of π
143 intro q
144 obtain ⟨c, hc⟩ := Quotient.exists_rep q
145 use c
146 simp only [recognitionQuotientMk]
147 exact hc
148 · -- Factorization R = R̄ ∘ π
149 intro c
150 rfl
151
152/-- **Corollary**: The recognition quotient is the unique (up to isomorphism)
153 quotient satisfying: (1) R factors through it, (2) the factored map is injective.
154
155 This is a categorical universal property: C_R is the coequalizer of the
156 indistinguishability relation. Any other quotient with an injective factorization
157 must be isomorphic to C_R.
158
159 Full proof requires defining the category of quotients and proving C_R
160 is terminal in the appropriate subcategory. -/