Theorems · Theorem · algebraic geometry

AlgebraicGeometry.image_morphismRestrict_preimage

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : TopologicalSpace.Opens ↥↑U),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.base).obj U).ι).obj
      ((TopologicalSpace.Opens.map (f ∣_ U).base).obj V) =
    (TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)

Defined in

Mathlib.AlgebraicGeometry.Restrict

Cited by

20 results in Mathlib

Foundations

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