`RecognitionQuotient`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Quotient
domain: RecogGeom
line: 26 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogGeom.Quotient on GitHub at line 26.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  23/-! ## Recognition Quotient -/
  24
  25/-- The recognition quotient C_R = C/~ where ~ is indistinguishability. -/
  26def RecognitionQuotient {C E : Type*} (r : Recognizer C E) :=
  27  Quotient (indistinguishableSetoid r)
  28
  29/-- The canonical projection π : C → C_R -/
  30def recognitionQuotientMk {C E : Type*} (r : Recognizer C E) (c : C) :
  31    RecognitionQuotient r :=
  32  Quotient.mk (indistinguishableSetoid r) c
  33
  34/-! ## Quotient Properties -/
  35
  36variable {C E : Type*} (r : Recognizer C E)
  37
  38/-- Two configurations have the same quotient class iff indistinguishable -/
  39theorem quotientMk_eq_iff {c₁ c₂ : C} :
  40    recognitionQuotientMk r c₁ = recognitionQuotientMk r c₂ ↔ c₁ ~[r] c₂ :=
  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 :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.