Theorems · Theorem · algebraic geometry

AlgebraicGeometry.morphismRestrict_appLE

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

Defined in

Mathlib.AlgebraicGeometry.Restrict

Cited by

3 results in Mathlib

Foundations

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