range_fst — Mathlib

English

The range of the fst projection from the pullback equals the preimage in X of the range of g.base in S, capturing the base change geometry of the first projection.

Русский

Область определения fst-проекции из pullback совпадает с предобразом образа g.base в S по карте f.

LaTeX

$$$Set.range (pullback.fst f g).base = f.base^{-1}( Set.range g.base )$$$

Lean4

theorem range_fst : Set.range (pullback.fst f g).base = f.base ⁻¹' Set.range g.base :=
  by
  ext x
  refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩
  · rintro ⟨a, rfl⟩
    simp only [Set.mem_preimage, Set.mem_range, ← Scheme.comp_base_apply, pullback.condition]
    simp
  · obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' x y hy.symm)
    use a, ha.left

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