inv_appTop

Mathlib.AlgebraicGeometry.Scheme

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

English

The appTop component of the inverse morphism equals the inverse of the appTop component of f.

Русский

Компонента appTop обратного отображения равна обратному отображению от компоненты appTop отображения f.

LaTeX

$$$ (f^{-1})_{\mathrm{appTop}} = (f_{\mathrm{appTop}})^{-1}. $$$

Lean4

theorem inv_appTop {X Y : Scheme} (f : X ⟶ Y) [IsIso f] : (inv f).appTop = inv (f.appTop) := by simp

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

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

Разделы

Аффилиация

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