range_fst_of_isPullback — Mathlib

English

In a pullback square with fst : P ⟶ X, the image of fst equals the preimage under f of the image of g.

Русский

В квадрате pullback, сопоставленном fst : P → X, образ fst равен обратному образу under f от образ g.

LaTeX

$$$\text{range}(fst) = f^{-1}(\text{range}(g)).$$$

Lean4

theorem range_fst_of_isPullback (h : IsPullback fst snd f g) : Set.range fst = f ⁻¹' Set.range g :=
  by
  let e := h.isoPullback ≪≫ Types.pullbackIsoPullback f g
  have : fst = _root_.Prod.fst ∘ Subtype.val ∘ e.hom := by
    ext p
    suffices fst p = pullback.fst f g (h.isoPullback.hom p) by simpa
    rw [← types_comp_apply h.isoPullback.hom (pullback.fst f g), IsPullback.isoPullback_hom_fst]
  rw [this, Set.range_comp, Set.range_comp, Set.range_eq_univ.mpr (surjective_of_epi e.hom)]
  ext
  simp [eq_comm]

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