Documentation

Mathlib.Topology.Category.TopCat.Yoneda

Yoneda presheaves on topologically concrete categories #

This file develops some API for "topologically concrete" categories, defining universe polymorphic "Yoneda presheaves" on such categories.

@[simp]
theorem ContinuousMap.yonedaPresheaf_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C TopCat) (Y : Type w') [TopologicalSpace Y] :
∀ {X Y_1 : Cᵒᵖ} (f : X Y_1) (g : C((F.obj (Opposite.unop X)), Y)), (ContinuousMap.yonedaPresheaf F Y).map f g = g.comp (F.map f.unop)

A universe polymorphic "Yoneda presheaf" on C given by continuous maps into a topoological space Y.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem ContinuousMap.yonedaPresheaf'_map (Y : Type w') [TopologicalSpace Y] :
    ∀ {X Y_1 : TopCatᵒᵖ} (f : X Y_1) (g : C((Opposite.unop X), Y)), (ContinuousMap.yonedaPresheaf' Y).map f g = g.comp f.unop

    A universe polymorphic Yoneda presheaf on TopCat given by continuous maps into a topoological space Y.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      The universe polymorphic Yoneda presheaf on TopCat preserves finite products.

      Equations
      • One or more equations did not get rendered due to their size.