instIsIsoSubschemeιBotIdealSheafData

English

For any scheme X, the canonical inclusion of the bottom subscheme ⊥ into X is an isomorphism; i.e., the bottom subscheme is canonically identified with X.

Русский

Для любой схемы X каноническое вложение нижней подсхемы ⊥ в X является изоморфизмом; то есть нижняя подсхема естественным образом эквивалентна X.

LaTeX

$$$\\bot_X \\cong X$$$

Lean4

instance : IsIso (IdealSheafData.subschemeι ⊥ : _ ⟶ X) :=
  ⟨Scheme.Hom.toImage (𝟙 X) ≫ IdealSheafData.inclusion bot_le, by simp [← cancel_mono (IdealSheafData.subschemeι _)], by
    simp⟩

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