pullback_snd_range — Mathlib

English

The range of the snd projection from the pullback equals the set of pairs (x,y) with f(x) = g(y).

Русский

Образ snd-проекции пределa равен множеству пар (x,y) таких, что f(x) = g(y).

LaTeX

$$$ \operatorname{range}( \mathrm{pullback.snd} f g ) = \{ y : Y \mid \exists x : X, f x = g y \} $$$

Lean4

theorem pullback_snd_range {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) :
    Set.range (pullback.snd f g) = {y : Y | ∃ x : X, f x = g y} :=
  by
  ext y
  constructor
  · rintro ⟨x, rfl⟩
    use pullback.fst f g x
    exact CategoryTheory.congr_fun pullback.condition x
  · rintro ⟨x, eq⟩
    use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩
    rw [pullbackIsoProdSubtype_inv_snd_apply]

Похожие утверждения