quotientEventMap_injective

formal source

  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
  75/-- The quotient is isomorphic to the image of R -/
  76noncomputable def quotient_equiv_image :
  77    RecognitionQuotient r ≃ Set.range r.R :=
  78  Equiv.ofBijective
  79    (fun q => ⟨quotientEventMap r q,
  80      Quotient.inductionOn q (fun c => ⟨c, rfl⟩)⟩)
  81    ⟨fun q₁ q₂ h => by
  82      simp only [Subtype.mk.injEq] at h
  83      exact quotientEventMap_injective r h,
  84     fun ⟨e, c, hc⟩ => ⟨recognitionQuotientMk r c, by simp [quotientEventMap_spec, hc]⟩⟩
  85
  86/-! ## Lifting Functions to Quotient -/
  87
  88/-- A function f : C → X descends to the quotient if it respects indistinguishability -/
  89def liftToQuotient {X : Type*} (f : C → X)
  90    (hf : ∀ c₁ c₂, Indistinguishable r c₁ c₂ → f c₁ = f c₂) :
  91    RecognitionQuotient r → X :=
  92  Quotient.lift f hf
  93
  94theorem liftToQuotient_spec {X : Type*} (f : C → X)