quotientMapLeft

formal source

 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
 132
 133theorem quotientMapRight_surjective (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 134    Function.Surjective (quotientMapRight r₁ r₂) := by
 135  intro q
 136  obtain ⟨c, rfl⟩ := Quotient.exists_rep q
 137  use recognitionQuotientMk (r₁ ⊗ r₂) c
 138  rfl
 139
 140/-! ## The Refinement Theorem -/
 141
 142/-- **Refinement Theorem**: The composite quotient refines both component quotients.
 143
 144    This is the fundamental theorem of recognition composition. It says that