map_eq_id

Mathlib.AlgebraicGeometry.GammaSpecAdjunction

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Spec.map_eq_id

English

For any f: Spec S ⟶ Spec R, Spec.map (Spec.preimage f) = f.

Русский

Для отображения f: Spec S ⟶ Spec R выполняется Spec.map (Spec.preimage f) = f.

LaTeX

$$Spec.map (Spec.preimage f) = f$$

Lean4

@[simp]
theorem map_eq_id {R : CommRingCat} {ϕ : R ⟶ R} : Spec.map ϕ = 𝟙 (Spec R) ↔ ϕ = 𝟙 R := by simp [← map_inj]

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

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

Разделы

Аффилиация

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