Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsAffineOpen.comap_primeIdealOf_appLE

∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↥X} (U : Y.Opens) (hU : AlgebraicGeometry.IsAffineOpen U)
  (V : X.Opens) (hV : AlgebraicGeometry.IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U)
  (hx : x ∈ V),
  PrimeSpectrum.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V hVU)) (hV.primeIdealOf ⟨x, hx⟩) =
    hU.primeIdealOf ⟨f x, ⋯⟩

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

1 results in Mathlib

Foundations

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