Sheaf of continuous maps associated to topological space

Given a topological space T, we consider the presheaf on Scheme given by U ↦ C(U, T) and show that it is a Zariski sheaf (TODO: show that it is a fpqc sheaf). When T is discrete, this is the constant sheaf associated to T (TODO).

Main declarations

• AlgebraicGeometry.continuousMapPresheaf: The sheaf U ↦ C(U, T) for a topological space T.
• AlgebraicGeometry.continuousMapPresheafAb: For a topological abelian group A, this is continuousMapPresheaf A viewed as a sheaf of abelian groups.

TODOs

• Show that continuousMapPresheaf is a sheaf for the fpqc topology (@chrisflav).

def AlgebraicGeometry.continuousMapPresheaf (T : Type v) [TopologicalSpace T] : CategoryTheory.Functor 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.

@[simp]

theorem AlgebraicGeometry.continuousMapPresheaf_obj (T : Type v) [TopologicalSpace T] (U : Schemeᵒᵖ) : (continuousMapPresheaf T).obj U = C(↥(Opposite.unop U), T)

@[simp]

theorem AlgebraicGeometry.continuousMapPresheaf_map (T : Type v) [TopologicalSpace T] {U V : Schemeᵒᵖ} (f : U ⟶ V) (g : C(↥(Opposite.unop U), T)) : (continuousMapPresheaf T).map f g = g.comp (TopCat.Hom.hom f.unop.base)

def AlgebraicGeometry.continuousMapPresheafIsoUlift (T : Type v) [TopologicalSpace T] : continuousMapPresheaf T ≅ Scheme.forgetToTop.op.comp (TopCat.uliftFunctor.op.comp (CategoryTheory.yoneda.obj (TopCat.of (ULift.{u_1, v} T))))

continuousMapPresheaf is isomorphic to the composition of the forgetful functor to TopCat and the yoneda embedding.

theorem AlgebraicGeometry.isSheaf_zariskiTopology_continuousMapPresheaf (T : Type v) [TopologicalSpace T] : CategoryTheory.Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

theorem AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheaf (T : Type v) [TopologicalSpace T] : CategoryTheory.Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheaf T)

def AlgebraicGeometry.continuousMapPresheafEquivOfTotallyDisconnectedSpace (T : Type v) [TopologicalSpace T] [TotallyDisconnectedSpace T] (U : Scheme) : (continuousMapPresheaf T).obj (Opposite.op U) ≃ C(ConnectedComponents ↥U, T)

continuousMapPresheaf is U ↦ C(ConnectedComponents U, T) if T is totally disconnected.

def AlgebraicGeometry.continuousMapPresheafAb (A : Type v) [TopologicalSpace A] [AddCommGroup A] [IsTopologicalAddGroup A] : CategoryTheory.Functor Schemeᵒᵖ Ab

continuousMapPresheaf as a presheaf of abelian groups associated to a topological abelian group.

def AlgebraicGeometry.continuousMapPresheafAbForgetIso (A : Type v) [TopologicalSpace A] [AddCommGroup A] [IsTopologicalAddGroup A] : (continuousMapPresheafAb A).comp (CategoryTheory.forget Ab) ≅ continuousMapPresheaf A

continuousMapPresheafAb viewed as a type valued sheaf is isomorphic to `continuousMapPresheaf.

theorem AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheafAb (A : Type v) [TopologicalSpace A] [AddCommGroup A] [IsTopologicalAddGroup A] : CategoryTheory.Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheafAb A)