opensRange_pullback_fst_of_right — Mathlib

English

Let f: X → Z be an open immersion of schemes and g: Y → Z any morphism. Then the open range (opensRange) of the pullback projection fst: X ×_Z Y → Y equals the preimage under g of the open range of f; equivalently, the pullback along g preserves the open range via the natural projection.

Русский

Пусть f: X → Z — открытое вложение, и g: Y → Z — произвольный морфизм. Тогда открытое множество образа (opensRange) проекции fst: X ×_Z Y → Y совпадает с обратным образом под g от opensRange(f); эквивалентно, прямая вытяжка сохраняет открытое множество через проекцию.

LaTeX

$$$ (pullback.fst\; g\; f).opensRange = g^{-1}(f.opensRange) $$$

Lean4

theorem opensRange_pullback_fst_of_right : (pullback.fst g f).opensRange = g ⁻¹ᵁ f.opensRange :=
  Opens.ext (range_pullback_fst_of_right f g)

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