Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.restrict_presheaf_map

∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (V W : (TopologicalSpace.Opens ↥(X.restrict h))ᵒᵖ) (i : V ⟶ W),
  (X.restrict h).presheaf.map i = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

Defined in

Mathlib.AlgebraicGeometry.OpenImmersion

Cited by

0 results in Mathlib

Foundations

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