ideal_le_iff — Mathlib

English

For affine open U in X, I ≤ J in the ring of sections Γ(X,U) if and only if for every x ∈ X and h with x ∈ U, the germ maps satisfy I.map(⋯) ≤ J.map(⋯).

Русский

Для аффинного открытого U: I ≤ J тогда и только тогда, когда для каждого x ∈ X и h, соответствующие гёрм отображения удовлетворяют I.map(⋯) ≤ J.map(⋯).

LaTeX

$$$I \le J \iff \forall x\in X,\forall h\in U, I.map( X.presheaf.germ U x h).hom \le J.map( X.presheaf.germ U x h).hom$$$

Lean4

theorem ideal_le_iff {I J : Ideal Γ(X, U)} :
    I ≤ J ↔ ∀ (x : X) (h : x ∈ U), I.map (X.presheaf.germ U x h).hom ≤ J.map (X.presheaf.germ U x h).hom :=
  ⟨fun h _ _ ↦ Ideal.map_mono h, fun H _ hs ↦ hU.mem_ideal_iff.mpr fun x hx ↦ H x hx (Ideal.mem_map_of_mem _ hs)⟩

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