composite_cell_subset_left

formal source

  98             composite_indistinguishable_iff]
  99
 100/-- Composite resolution cells are subsets of either component cell -/
 101theorem composite_cell_subset_left (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
 102    ResolutionCell (r₁ ⊗ r₂) c ⊆ ResolutionCell r₁ c := by
 103  rw [composite_resolutionCell]
 104  exact Set.inter_subset_left
 105
 106theorem composite_cell_subset_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
 107    ResolutionCell (r₁ ⊗ r₂) c ⊆ ResolutionCell r₂ c := by
 108  rw [composite_resolutionCell]
 109  exact Set.inter_subset_right
 110
 111/-! ## Quotient Maps -/
 112
 113/-- There is a natural map from the composite quotient to the r₁ quotient -/
 114def quotientMapLeft (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 115    RecognitionQuotient (r₁ ⊗ r₂) → RecognitionQuotient r₁ :=
 116  Quotient.lift (recognitionQuotientMk r₁) (fun c₁ c₂ h =>
 117    (quotientMk_eq_iff r₁).mpr (composite_refines_left r₁ r₂ h))
 118
 119/-- There is a natural map from the composite quotient to the r₂ quotient -/
 120def quotientMapRight (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 121    RecognitionQuotient (r₁ ⊗ r₂) → RecognitionQuotient r₂ :=
 122  Quotient.lift (recognitionQuotientMk r₂) (fun c₁ c₂ h =>
 123    (quotientMk_eq_iff r₂).mpr (composite_refines_right r₁ r₂ h))
 124
 125/-- The quotient maps are surjective -/
 126theorem quotientMapLeft_surjective (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 127    Function.Surjective (quotientMapLeft r₁ r₂) := by
 128  intro q
 129  obtain ⟨c, rfl⟩ := Quotient.exists_rep q
 130  use recognitionQuotientMk (r₁ ⊗ r₂) c
 131  rfl