range_fiberι — Mathlib

English

For a morphism f: X → Y and a point y ∈ Y, the image of the base map of the fiber over y is exactly the preimage of y under the base map.

Русский

Пусть f: X → Y. Образ базовой карты волокна над y равен множеству точек, которые над y в X.

LaTeX

$$Set.range (f.fiberι y).base = f.base^{-1}({ y })$$

Lean4

theorem range_fiberι (f : X.Hom Y) (y : Y) : Set.range (f.fiberι y).base = f.base ⁻¹' { y } := by
  simp [fiber, fiberι, Scheme.Pullback.range_fst, Scheme.range_fromSpecResidueField]

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