ideal_map_of_isAffineHom — Mathlib

English

As in the previous result, but under an isomorphism condition IsAffineHom f, the same contraction formula holds for the affine open U.

Русский

Как и в предыдущем случае, при условии IsAffineHom f формула сокращения идеала на афинном открытом U остаётся той же.

LaTeX

$$$ (I.map f).ideal U = (I.ideal ⟨_, H⟩).comap (f.app U).hom $$$

Lean4

theorem ideal_map_of_isAffineHom (I : X.IdealSheafData) (f : X ⟶ Y) [IsAffineHom f] (U : Y.affineOpens) :
    (I.map f).ideal U = (I.ideal ⟨_, U.2.preimage f⟩).comap (f.app U).hom :=
  ideal_map I f U (U.2.preimage f)

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