chartOnQuotient

formal source

  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
  88    φ.toFun ⟨c, hc.1⟩
  89
  90/-- The chart on quotient is well-defined (independent of representative) -/
  91theorem chartOnQuotient_well_defined (φ : RecognitionChart L r n)
  92    (q : RecognitionQuotient r)
  93    (c₁ c₂ : C) (h₁ : c₁ ∈ φ.domain) (h₂ : c₂ ∈ φ.domain)
  94    (hq₁ : recognitionQuotientMk r c₁ = q) (hq₂ : recognitionQuotientMk r c₂ = q) :
  95    φ.toFun ⟨c₁, h₁⟩ = φ.toFun ⟨c₂, h₂⟩ := by
  96  have h : Indistinguishable r c₁ c₂ := by
  97    rw [← quotientMk_eq_iff r]
  98    rw [hq₁, hq₂]
  99  exact φ.respects_indistinguishable ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ h
 100
 101/-! ## Chart Compatibility -/
 102
 103/-- Two charts are compatible if they agree on their overlap -/
 104def ChartCompatible (φ₁ φ₂ : RecognitionChart L r n) : Prop :=
 105  ∀ c : C, ∀ (h₁ : c ∈ φ₁.domain) (h₂ : c ∈ φ₂.domain),
 106    φ₁.toFun ⟨c, h₁⟩ = φ₂.toFun ⟨c, h₂⟩
 107
 108/-- Chart compatibility is reflexive -/
 109theorem chartCompatible_refl (φ : RecognitionChart L r n) :
 110    ChartCompatible L r φ φ := by
 111  intro c h₁ h₂
 112  -- h₁ and h₂ are both proofs that c ∈ φ.domain, so they must give same result