range_pullback_to_base_of_left — Mathlib

English

Let f: X → Z be an open immersion and g: Y → Z. The image (range) of the base map of the composite pullback.fst f g ≫ f equals the intersection of the images of f.base and g.base in Z.

Русский

Пусть f: X → Z — открытое вложение и g: Y → Z. Образ базовой карты композиции pullback.fst f g ≫ f равен пересечению образов f.base и g.base внутри Z.

LaTeX

$$$\\operatorname{range}((pullback.fst\ \, f\\ g\\ ≫ f).base) = \\operatorname{range}(f.base) \\cap \\operatorname{range}(g.base)$$$

Lean4

theorem range_pullback_to_base_of_left : Set.range (pullback.fst f g ≫ f).base = Set.range f.base ∩ Set.range g.base :=
  by
  rw [pullback.condition, Scheme.comp_base, TopCat.coe_comp, Set.range_comp, range_pullback_snd_of_left,
    Opens.carrier_eq_coe, Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range, Opens.carrier_eq_coe,
    Scheme.Hom.coe_opensRange]

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