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 topoological 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✝) (g : C(↑(F.obj (Opposite.unop X✝)), Y)) :
    (ContinuousMap.yonedaPresheaf F Y).map f g = g.comp (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ᵒᵖ) :
    (ContinuousMap.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 topoological 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✝) (g : C(↑(Opposite.unop X✝), Y)) :
      (ContinuousMap.yonedaPresheaf' Y).map f g = g.comp f.unop
      source
      @[simp]
      theorem ContinuousMap.yonedaPresheaf'_obj (Y : Type w') [TopologicalSpace Y] (X : TopCatᵒᵖ) :
      (ContinuousMap.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] :
      ContinuousMap.yonedaPresheaf F Y = F.op.comp (ContinuousMap.yonedaPresheaf' Y)
      source
      theorem ContinuousMap.piComparison_fac (Y : Type w') [TopologicalSpace Y] {α : Type} (X : α → TopCat) :
      (CategoryTheory.Limits.piComparison (ContinuousMap.yonedaPresheaf' Y) fun (x : α) => Opposite.op (X x)) = CategoryTheory.CategoryStruct.comp ((ContinuousMap.yonedaPresheaf' Y).map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct X).inv (TopCat.sigmaIsoSigma X).inv.op)) (CategoryTheory.CategoryStruct.comp (equivEquivIso (ContinuousMap.sigmaEquiv Y fun (x : α) => ↑(X x))).inv (CategoryTheory.Limits.Types.productIso fun (i : α) => C(↑(X i), Y)).inv)
      source
      noncomputable instance ContinuousMap.instPreservesFiniteProductsOppositeTopCatYonedaPresheaf' (Y : Type w') [TopologicalSpace Y] :
      CategoryTheory.Limits.PreservesFiniteProducts (ContinuousMap.yonedaPresheaf' Y)

      The universe polymorphic Yoneda presheaf on TopCat preserves finite products.

      Equations
      • ⋯ = ⋯