quotientMapRight

formal source

 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
 145    combining recognizers gives us a "finer" view of configuration space.
 146    The composite quotient C_{R₁₂} maps onto both C_{R₁} and C_{R₂}.
 147
 148    Mathematically: there exist surjective maps
 149      π₁ : C_{R₁₂} → C_{R₁}
 150      π₂ : C_{R₁₂} → C_{R₂}