range_pullback_to_base_of_right — Mathlib

English

Similarly, with the roles of f and g swapped, the range of (pullback.fst g f ≫ g).base equals the intersection of the images of g.base and f.base in Z.

Русский

Аналогично, при перестановке ролей f и g, образ (pullback.fst g f ≫ g).base совпадает с пересечением образов g.base и f.base в Z.

LaTeX

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

Lean4

theorem range_pullback_to_base_of_right : Set.range (pullback.fst g f ≫ g).base = Set.range g.base ∩ Set.range f.base :=
  by
  rw [Scheme.comp_base, TopCat.coe_comp, Set.range_comp, range_pullback_fst_of_right, Opens.map_obj,
    Opens.carrier_eq_coe, Opens.coe_mk, Set.image_preimage_eq_inter_range, Set.inter_comm]

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