projectSet

formal source

  98/-! ## Quotient of Local Structure -/
  99
 100/-- The projection of a set U ⊆ C to the quotient -/
 101def projectSet (U : Set C) : Set (RecognitionQuotient r) :=
 102  {q | ∃ c ∈ U, recognitionQuotientMk r c = q}
 103
 104/-- The induced neighborhood structure on the quotient -/
 105def quotientNeighborhoods (L : LocalConfigSpace C) :
 106    RecognitionQuotient r → Set (Set (RecognitionQuotient r)) :=
 107  fun q => {V | ∃ c : C, recognitionQuotientMk r c = q ∧ ∃ U ∈ L.N c, projectSet r U ⊆ V}
 108
 109/-! ## Summary Theorem -/
 110
 111/-- Summary: The recognition quotient captures exactly the observable structure -/
 112theorem recognition_quotient_summary :
 113    Function.Surjective (recognitionQuotientMk r) ∧
 114    Function.Injective (quotientEventMap r) := by
 115  constructor
 116  · intro q
 117    obtain ⟨c, rfl⟩ := Quotient.exists_rep q
 118    exact ⟨c, rfl⟩
 119  · exact quotientEventMap_injective r
 120
 121/-! ## Module Status -/
 122
 123def quotient_status : String :=
 124  "✓ RecognitionQuotient defined (C_R = C/~)\n" ++
 125  "✓ Canonical projection π : C → C_R\n" ++
 126  "✓ quotientMk_eq_iff: same class ↔ indistinguishable\n" ++
 127  "✓ quotientEventMap: R̄ : C_R → E\n" ++
 128  "✓ quotientEventMap_injective: R̄ is injective\n" ++
 129  "✓ quotient_equiv_image: C_R ≃ Im(R)\n" ++
 130  "✓ liftToQuotient: lifting functions\n" ++
 131  "✓ quotientNeighborhoods: induced locality\n" ++