Theorems · Definition · algebraic geometry

AlgebraicGeometry.continuousMapPresheaf

(T : Type v) → [TopologicalSpace T] → CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ (Type (max v u))

The yoneda embedding of TopCat precomposed with the forgetful functor from Scheme. This is the presheaf U ↦ C(U, T). For universe reasons, we implement it by hand.

Defined in

Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpace