id_toShHom'

Mathlib.Geometry.RingedSpace.LocallyRingedSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.LocallyRingedSpace.id_toShHom'

Lean4

/-- A variant of `id_toShHom'` that works with `𝟙 X` instead of `id X`. -/
@[simp]
theorem id_toShHom' (X : LocallyRingedSpace.{u}) : Hom.toShHom (𝟙 X) = 𝟙 X.toSheafedSpace :=
  rfl

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

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

Разделы

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

Аффилиация

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