instIsPreimmersionFiberι

Mathlib.AlgebraicGeometry.Fiber

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsPreimmersionFiberι

English

The scheme-theoretic fiber of f at y is homeomorphic to the preimage f^{-1}({y}).

Русский

Схемоподобное волокно f над y гомеоморфно к множеству f^{-1}({y}).

LaTeX

$$f.fiber y ≃ₜ f.base ⁻¹' { y }$$

Lean4

instance (f : X ⟶ Y) (y : Y) : IsPreimmersion (f.fiberι y) :=
  MorphismProperty.pullback_fst _ _ inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru