Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion

∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f]
  (U : ↑X.affineOpens),
  (I.comap f).ideal U =
    Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appIso f ↑U).inv)
      (I.ideal ⟨(AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ↑U, ⋯⟩)

Defined in

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Cited by

1 results in Mathlib

Foundations

Depth 214 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.IsOpenImmersion