fiberι_asFiber

Mathlib.AlgebraicGeometry.Fiber

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Hom.fiberι_asFiber

English

The inverse of Δ' is compatible with the base-change map: (W.map f)Δ'^{-1} = f(W.Δ'^{-1}).

Русский

Обратное к Δ' сохраняется при базисном переносе: (W.map f)Δ'^{-1} = f(W.Δ'^{-1}).

LaTeX

$$(W.map f).Δ'^{-1} = f(W.Δ'^{-1})$$

Lean4

@[simp]
theorem fiberι_asFiber (f : X.Hom Y) (x : X) : (f.fiberι _).base (f.asFiber x) = x :=
  f.fiberι_fiberHomeo_symm _ _

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

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

Разделы

Аффилиация

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