Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion

∀ {X Y U V : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (f' : U ⟶ V) (iU : U ⟶ X) (iV : V ⟶ Y)
  [inst : AlgebraicGeometry.IsOpenImmersion iV] [AlgebraicGeometry.QuasiCompact f],
  CategoryTheory.IsPullback f' iU iV f →
    ∀ (W : ↑V.affineOpens),
      (AlgebraicGeometry.Scheme.Hom.ker f').ideal W =
        Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appIso iV ↑W).inv)
          ((AlgebraicGeometry.Scheme.Hom.ker f).ideal ⟨(AlgebraicGeometry.Scheme.Hom.opensFunctor iV).obj ↑W, ⋯⟩)

Defined in

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsOpenImmersionAlgebraicGeometry.QuasiCompact