instIsZariskiLocalAtSource

Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.SurjectiveOnStalks.instIsZariskiLocalAtSource

← MathLib Explorer

English

Similarly, SurjectiveOnStalks is Zariski-local at the source.

Русский

Аналогично, SurjectiveOnStalks локально по зарику на источнике.

LaTeX

$$IsZariskiLocalAtSource SurjectiveOnStalks$$

Lean4

instance : IsZariskiLocalAtSource @SurjectiveOnStalks :=
  eq_stalkwise ▸ stalkwise_isZariskiLocalAtSource_of_respectsIso RingHom.surjective_respectsIso

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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