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
๐Ÿ”ธ coverage
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
    Instances For
      source
      ๐Ÿ“ coverage
      @[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)) :
      (yonedaPresheaf F Y).map f g = g.comp (TopCat.Hom.hom (F.map f.unop))
      source
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ”ธ coverage
      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
        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem ContinuousMap.yonedaPresheaf'_map (Y : Type w') [TopologicalSpace Y] {Xโœ Yโœ : TopCatแต’แต–} (f : Xโœ โŸถ Yโœ) (g : C(โ†‘(Opposite.unop Xโœ), Y)) :
          (yonedaPresheaf' Y).map f g = g.comp (CategoryTheory.ConcreteCategory.hom f.unop)
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem ContinuousMap.yonedaPresheaf'_obj (Y : Type w') [TopologicalSpace Y] (X : TopCatแต’แต–) :
          (yonedaPresheaf' Y).obj X = C(โ†‘(Opposite.unop X), Y)
          source
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          instance ContinuousMap.instPreservesFiniteProductsOppositeTopCatYonedaPresheaf' (Y : Type w') [TopologicalSpace Y] :
          CategoryTheory.Limits.PreservesFiniteProducts (yonedaPresheaf' Y)

          The universe polymorphic Yoneda presheaf on TopCat preserves finite products.