English
Let r ≤ s be two equivalence relations on α. There is a canonical bijection between the sigma-type over Quotient s, where each fiber is a Quotient of the comap of r along Subtype.val, and the quotient by r. In symbols, (Σ q : Quotient s, Quotient (r.comap (Subtype.val))) ≃ Quotient r.
Русский
Пусть r ≤ s — две эквивалентности на α. Существует каноническая биекция между суммой по q ∈ Quotient s и соответствующими фрагментами Quotient(r.comap Subtype.val) и Quotient r.
LaTeX
$$$\\left( \\Sigma q:\\,\\Quotient s,\\; \\Quotient\\bigl( r.\\mathrm{comap}(\\mathrm{Subtype.val})\\bigr) \\right) \\simeq \\Quotient r.$$$
Lean4
/-- Given two equivalence relations with `r ≤ s`, a bijection between the sum of the quotients by
`r` on each equivalence class by `s` and the quotient by `r`. -/
def sigmaQuotientEquivOfLe {r s : Setoid α} (hle : r ≤ s) :
(Σ q : Quotient s, Quotient (r.comap (Subtype.val : Quotient.mk s ⁻¹' { q } → α))) ≃ Quotient r :=
.trans
(.symm <|
.sigmaCongrRight fun _ ↦
.subtypeQuotientEquivQuotientSubtype (s₁ := r) (s₂ := r.comap Subtype.val) _ _ (fun _ ↦ Iff.rfl) fun _ _ ↦
Iff.rfl)
(.sigmaFiberEquiv fun a ↦ a.lift (Quotient.mk s) fun _ _ h ↦ Quotient.sound <| hle h)
