le_of_isAffine — Mathlib

English

If X is affine, inclusion of ideals at the affine level implies a global order relation on ideal sheaf data.

Русский

Если X аффина, включение идеалов на аффинном уровне имплицирует глобальный порядок для данных идеальных слоев.

LaTeX

$$H : I.ideal ⟨⊤, isAffineOpen_top X⟩ ≤ J.ideal ⟨⊤, isAffineOpen_top X⟩ → I ≤ J$$

Lean4

theorem le_of_isAffine [IsAffine X] {I J : IdealSheafData X}
    (H : I.ideal ⟨⊤, isAffineOpen_top X⟩ ≤ J.ideal ⟨⊤, isAffineOpen_top X⟩) : I ≤ J :=
  by
  intro U
  rw [← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) I (le_top (a := U.1)), ←
    map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) J (le_top (a := U.1))]
  exact Ideal.map_mono H

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