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.

source
def ContinuousMap.yonedaPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C TopCat) (Y : Type w') [TopologicalSpace Y] :
CategoryTheory.Functor Cᵒᵖ (Type (max w w'))

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) :
    (yonedaPresheaf F Y).map f = TypeCat.ofHom fun (g : C(↑(F.obj (Opposite.unop X✝)), Y)) => g.comp (TopCat.Hom.hom (F.map f.unop))
    source
    @[simp]
    theorem ContinuousMap.yonedaPresheaf_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C TopCat) (Y : Type w') [TopologicalSpace Y] (X : Cᵒᵖ) :
    (yonedaPresheaf F Y).obj X = C(↑(F.obj (Opposite.unop X)), Y)
    source
    def ContinuousMap.yonedaPresheaf' (Y : Type w') [TopologicalSpace Y] :
    CategoryTheory.Functor TopCatᵒᵖ (Type (max w w'))

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem ContinuousMap.yonedaPresheaf'_map (Y : Type w') [TopologicalSpace Y] {X✝ Y✝ : TopCatᵒᵖ} (f : X✝ ⟶ Y✝) :
      (yonedaPresheaf' Y).map f = TypeCat.ofHom fun (g : C(↑(Opposite.unop X✝), Y)) => g.comp (CategoryTheory.ConcreteCategory.hom f.unop)
      source
      @[simp]
      theorem ContinuousMap.yonedaPresheaf'_obj (Y : Type w') [TopologicalSpace Y] (X : TopCatᵒᵖ) :
      (yonedaPresheaf' Y).obj X = C(↑(Opposite.unop X), Y)
      source
      theorem ContinuousMap.comp_yonedaPresheaf' {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C TopCat) (Y : Type w') [TopologicalSpace Y] :
      yonedaPresheaf F Y = F.op.comp (yonedaPresheaf' Y)
      source
      theorem ContinuousMap.piComparison_fac (Y : Type w') [TopologicalSpace Y] {α : Type} (X : α → TopCat) :
      (CategoryTheory.Limits.piComparison (yonedaPresheaf' Y) fun (x : α) => Opposite.op (X x)) = CategoryTheory.CategoryStruct.comp ((yonedaPresheaf' Y).map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct X).inv (TopCat.sigmaIsoSigma X).inv.op)) (CategoryTheory.CategoryStruct.comp (equivEquivIso (sigmaEquiv Y fun (x : α) => ↑(X x))).inv (CategoryTheory.Limits.Types.productIso fun (i : α) => C(↑(X i), Y)).inv)
      source
      instance ContinuousMap.instPreservesFiniteProductsOppositeTopCatYonedaPresheaf' (Y : Type w') [TopologicalSpace Y] :
      CategoryTheory.Limits.PreservesFiniteProducts (yonedaPresheaf' Y)

      The universe polymorphic Yoneda presheaf on TopCat preserves finite products.