isoOfEq_rfl

Mathlib.AlgebraicGeometry.Restrict

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

← MathLib Explorer

English

For any open U, the isomorphism X.isoOfEq(refl U) is the identity on U.

Русский

Для любого открытого U изоморфизм X.isoOfEq(refl U) является тождественным на U.

LaTeX

$$X.isoOfEq(\\text{refl } U) = Iso.refl _$$

Lean4

@[simp]
theorem isoOfEq_rfl (X : Scheme.{u}) (U : X.Opens) : X.isoOfEq (refl U) = Iso.refl _ :=
  by
  ext1
  rw [← cancel_mono U.ι, Scheme.isoOfEq_hom_ι, Iso.refl_hom, Category.id_comp]

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

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

Разделы

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

Аффилиация

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