ext_of_isAffine — Mathlib

English

If X is affine, two ideal sheaf data with equal underlying ideals agree as objects.

Русский

Если X аффина, совпадающие по базовой идее данные идеального слоя равны как объекты.

LaTeX

$$I = J$$

Lean4

theorem ext_of_isAffine [IsAffine X] {I J : IdealSheafData X}
    (H : I.ideal ⟨⊤, isAffineOpen_top X⟩ = J.ideal ⟨⊤, isAffineOpen_top X⟩) : I = J :=
  (le_of_isAffine H.le).antisymm (le_of_isAffine H.ge)

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