fiberHomeo_apply

Mathlib.AlgebraicGeometry.Fiber

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply

English

The base of the fiberι map at x recovers the original point x when viewed in X.

Русский

Базовый образ волокна fiberι над x возвращает исходную точку x в X.

LaTeX

$$(f.fiberι _).base (f.asFiber x) = x$$

Lean4

@[simp]
theorem fiberHomeo_apply (f : X.Hom Y) (y : Y) (x : f.fiber y) : (f.fiberHomeo y x).1 = (f.fiberι y).base x :=
  rfl

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

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

Разделы

Аффилиация

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