comap_id'

Mathlib.AlgebraicGeometry.StructureSheaf

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.StructureSheaf.comap_id'

← MathLib Explorer

English

If U = V, the comap along the identity is the identity.

Русский

Если U = V, комап по тождественному отображению равен тождественному отображению.

LaTeX

$$$comap f U V hUV = eqToHom( ... )$$$

Lean4

@[simp]
theorem comap_id' (U : Opens (PrimeSpectrum.Top R)) :
    (comap (RingHom.id R) U U fun p hpU => by rwa [PrimeSpectrum.comap_id]) = RingHom.id _ := by rw [comap_id rfl]; rfl

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

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

Разделы

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

Аффилиация

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