English
If for each x, p x ↔ q (f x), then (Σ y : Subtype q, { x : α // f x = y }) ≃ Subtype p.
Русский
При условии, что ∀ x, p x ↔ q (f x), имеем эквивалентность между (Σ y : Subtype q, { x : α // f x = y }) и Subtype p.
LaTeX
$$$(\\Sigma y : Subtype q, { x : \\alpha // f x = y }) \\simeq \\text{Subtype } p$, given h: ∀ x, p x ↔ q (f x)$$
Lean4
/-- If for each `x` we have `p x ↔ q (f x)`, then `Σ y : {y // q y}, f ⁻¹' {y}` is equivalent
to `{x // p x}`. -/
def sigmaSubtypeFiberEquivSubtype {α β : Type*} (f : α → β) {p : α → Prop} {q : β → Prop} (h : ∀ x, p x ↔ q (f x)) :
(Σ y : Subtype q, { x : α // f x = y }) ≃ Subtype p :=
calc
(Σ y : Subtype q, { x : α // f x = y }) ≃
Σ y : Subtype q, { x : Subtype p // Subtype.mk (f x) ((h x).1 x.2) = y } :=
by {
apply sigmaCongrRight
intro y
apply Equiv.symm
refine (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight ?_)
intro x
exact ⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2), Subtype.eq h'⟩⟩
}
_ ≃ Subtype p := sigmaFiberEquiv fun x : Subtype p => (⟨f x, (h x).1 x.property⟩ : Subtype q)
