RecognitionChart

formal source

  54    a map φ : U → ℝⁿ such that:
  55    1. φ is injective on resolution cells (indistinguishable configs map to same point)
  56    2. φ is "continuous" in the sense that small changes in config give small changes in φ -/
  57structure RecognitionChart (L : LocalConfigSpace C) (r : Recognizer C E) (n : ℕ) where
  58  /-- The domain: a neighborhood in the local structure -/
  59  domain : Set C
  60  /-- The domain is a valid neighborhood of some point -/
  61  domain_is_nbhd : ∃ c, domain ∈ L.N c
  62  /-- The coordinate map -/
  63  toFun : domain → Fin n → ℝ
  64  /-- Indistinguishable configurations map to the same coordinates -/
  65  respects_indistinguishable : ∀ c₁ c₂ : domain,
  66    Indistinguishable r c₁.val c₂.val → toFun c₁ = toFun c₂
  67  /-- The map is injective on resolution classes -/
  68  injective_on_classes : ∀ c₁ c₂ : domain,
  69    toFun c₁ = toFun c₂ → Indistinguishable r c₁.val c₂.val
  70
  71/-! ## Chart Properties -/
  72
  73variable {n : ℕ} (L : LocalConfigSpace C) (r : Recognizer C E)
  74
  75/-- A chart maps equivalent configurations to the same coordinates -/
  76theorem chart_respects_equiv (φ : RecognitionChart L r n) (c₁ c₂ : φ.domain)
  77    (h : Indistinguishable r c₁.val c₂.val) :
  78    φ.toFun c₁ = φ.toFun c₂ :=
  79  φ.respects_indistinguishable c₁ c₂ h
  80
  81/-- A chart induces a well-defined map on the local quotient -/
  82noncomputable def chartOnQuotient (φ : RecognitionChart L r n) :
  83    {q : RecognitionQuotient r // ∃ c ∈ φ.domain, recognitionQuotientMk r c = q} →
  84    (Fin n → ℝ) :=
  85  fun ⟨_, hq⟩ =>
  86    let c := hq.choose
  87    let hc : c ∈ φ.domain ∧ recognitionQuotientMk r c = _ := hq.choose_spec