map_injective

Mathlib.AlgebraicGeometry.GammaSpecAdjunction

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

English

Spec.map on morphisms is injective: if Spec.map φ = Spec.map ψ then φ = ψ.

Русский

Spec.map на отображениях инъективен: если Spec.map φ = Spec.map ψ, то φ = ψ.

LaTeX

$$∀ {R S : CommRingCat}, Function.Injective (Spec.map : (R ⟶ S) → _)$$

Lean4

theorem map_injective {R S : CommRingCat} : Function.Injective (Spec.map : (R ⟶ S) → _) := fun _ _ ↦ Spec.map_inj.mp

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

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

Разделы

Аффилиация

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