mathlib3 documentation

algebraic_geometry.presheafed_space

Presheafed spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Introduces the category of topological spaces equipped with a presheaf (taking values in an arbitrary target category C.)

We further describe how to apply functors and natural transformations to the values of the presheaves.

@[simp]
theorem algebraic_geometry.PresheafedSpace.mk_coe {C : Type u} [category_theory.category C] (carrier : Top) (presheaf : Top.presheaf C carrier) :
{carrier := carrier, presheaf := presheaf} = carrier

The constant presheaf on X with value Z.

Equations

A morphism between presheafed spaces X and Y consists of a continuous map f between the underlying topological spaces, and a (notice contravariant!) map from the presheaf on Y to the pushforward of the presheaf on X via f.

Instances for algebraic_geometry.PresheafedSpace.hom
theorem algebraic_geometry.PresheafedSpace.hext {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} (α β : X.hom Y) (w : α.base = β.base) (h : α.c == β.c) :
α = β

The identity morphism of a PresheafedSpace.

Equations

Composition of morphisms of PresheafedSpaces.

Equations
@[protected, instance]

The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map from the presheaf on the target to the pushforward of the presheaf on the source.

Equations
@[simp]

Sometimes rewriting with comp_c_app doesn't work because of dependent type issues. In that case, erw comp_c_app_assoc might make progress. The lemma comp_c_app_assoc is also better suited for rewrites in the opposite direction.

An isomorphism of PresheafedSpaces is a homeomorphism of the underlying space, and a natural transformation between the sheaves.

Equations

The restriction of a presheafed space along an open embedding into the space.

Equations

The map from the restriction of a presheafed space.

Equations
Instances for algebraic_geometry.PresheafedSpace.of_restrict

The map to the restriction of a presheafed space along the canonical inclusion from the top subspace.

Equations

The isomorphism from the restriction to the top subspace.

Equations

We can apply a functor F : C ⥤ D to the values of the presheaf in any PresheafedSpace C, giving a functor PresheafedSpace C ⥤ PresheafedSpace D

Equations

A natural transformation induces a natural transformation between the map_presheaf functors.

Equations