quotientMk_respects_event

formal source

  41  Quotient.eq (r := indistinguishableSetoid r)
  42
  43/-- The projection respects the recognizer: same class → same event -/
  44theorem quotientMk_respects_event {c₁ c₂ : C}
  45    (h : recognitionQuotientMk r c₁ = recognitionQuotientMk r c₂) :
  46    r.R c₁ = r.R c₂ :=
  47  (quotientMk_eq_iff r).mp h
  48
  49/-- The quotient is nonempty if C is -/
  50instance [ConfigSpace C] : Nonempty (RecognitionQuotient r) :=
  51  ⟨recognitionQuotientMk r (ConfigSpace.witness C)⟩
  52
  53/-! ## Event Map on Quotient -/
  54
  55/-- The event map factors through the quotient: R = R̄ ∘ π -/
  56def quotientEventMap : RecognitionQuotient r → E :=
  57  Quotient.lift r.R (fun _ _ h => h)
  58
  59/-- The quotient event map makes the diagram commute -/
  60theorem quotientEventMap_spec (c : C) :
  61    quotientEventMap r (recognitionQuotientMk r c) = r.R c := rfl
  62
  63/-- The quotient event map is injective -/
  64theorem quotientEventMap_injective :
  65    Function.Injective (quotientEventMap r) := by
  66  intro q₁ q₂ h
  67  obtain ⟨c₁, hc₁⟩ := Quotient.exists_rep q₁
  68  obtain ⟨c₂, hc₂⟩ := Quotient.exists_rep q₂
  69  simp only [← hc₁, ← hc₂] at h ⊢
  70  -- h : quotientEventMap r ⟦c₁⟧ = quotientEventMap r ⟦c₂⟧
  71  -- which means r.R c₁ = r.R c₂
  72  apply Quotient.sound
  73  exact h
  74