instContainsIdentitiesScheme

Mathlib.AlgebraicGeometry.Morphisms.Integral

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsIntegralHom.instContainsIdentitiesScheme

English

The identity morphism on any scheme is integral.

Русский

Идентичность на любой схеме интегральна.

LaTeX

$$ContainsIdentities IsIntegralHom$$

Lean4

instance : ContainsIdentities @IsIntegralHom :=
  ⟨fun X ↦ ⟨fun _ _ ↦ by simpa using RingHom.isIntegral_of_surjective _ (Equiv.refl _).surjective⟩⟩

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

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

Разделы

Аффилиация

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