instιScheme

Mathlib.AlgebraicGeometry.Morphisms.Immersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsImmersion.instιScheme

← MathLib Explorer

English

The equalizer immersion equalizer.ι f g is immersion for any pair of morphisms f,g.

Русский

Нормирование равнителя равносильно вложению равнителя, равном f и g.

LaTeX

$$$\\text{IsImmersion}(\\text{equalizer.ι}(f,g))$$$

Lean4

instance (f g : X ⟶ Y) : IsImmersion (equalizer.ι f g) :=
  MorphismProperty.of_isPullback (P := @IsImmersion) (isPullback_equalizer_prod f g).flip inferInstance

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

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

Разделы

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

Аффилиация

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