English
If π : Y → Z is a coequalizer of (f,g), and U ⊆ Y with f^{-1}(U) = g^{-1}(U), then π^{-1}(π[U]) = U.
Русский
Если π : Y → Z является копроэквалайзером пары (f,g), и U ⊆ Y удовлетворяет f^{-1}(U) = g^{-1}(U), то π^{-1}(π[U]) = U.
LaTeX
$$$$ π^{-1}(π''U) = U $$$$
Lean4
/-- If `π : Y ⟶ Z` is an coequalizer for `(f, g)`, and `U ⊆ Y` such that `f ⁻¹' U = g ⁻¹' U`,
then `π ⁻¹' (π '' U) = U`.
-/
theorem coequalizer_preimage_image_eq_of_preimage_eq (π : Y ⟶ Z) (e : f ≫ π = g ≫ π) (h : IsColimit (Cofork.ofπ π e))
(U : Set Y) (H : f ⁻¹' U = g ⁻¹' U) : π ⁻¹' (π '' U) = U :=
by
have lem : ∀ x y, Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U) :=
by
rintro _ _ ⟨x⟩
change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
rw [H]
have eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U := by aesop (add safe constructors _root_.Equivalence)
ext
constructor
· rw [← show _ = π from h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2 WalkingParallelPair.one]
rintro ⟨y, hy, e'⟩
dsimp at e'
replace e' :=
(mono_iff_injective (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp inferInstance e'
exact (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem (Quot.eqvGen_exact e'))).mp hy
· exact fun hx => ⟨_, hx, rfl⟩
