Documentation

Mathlib.Topology.Category.TopCat.Monoidal

The cartesian monoidal structure on TopCat #

We define the cartesian monoidal category structure on TopCat. We also introduce the unit interval as an object TopCat.I of TopCat.

source
@[implicit_reducible]
instance TopCat.instCartesianMonoidalCategory :
CategoryTheory.CartesianMonoidalCategory TopCat
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
instance TopCat.instBraidedCategory :
CategoryTheory.BraidedCategory TopCat
Equations
source
@[simp]
theorem TopCat.tensor_apply {W X Y Z : TopCat} (f : W ⟶ X) (g : Y ⟶ Z) (p : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj W Y)) :
(Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) p = ((CategoryTheory.ConcreteCategory.hom f) p.1, (CategoryTheory.ConcreteCategory.hom g) p.2)
source
@[simp]
theorem TopCat.whiskerLeft_apply (X : TopCat) {Y Z : TopCat} (f : Y ⟶ Z) (p : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)) p = (p.1, (CategoryTheory.ConcreteCategory.hom f) p.2)
source
@[simp]
theorem TopCat.whiskerRight_apply {Y Z : TopCat} (f : Y ⟶ Z) (X : TopCat) (p : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)) :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)) p = ((CategoryTheory.ConcreteCategory.hom f) p.1, p.2)
source
@[simp]
theorem TopCat.leftUnitor_hom_apply {X : TopCat} {x : ↑X} {p : PUnit.{u + 1}} :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) (p, x) = x
source
@[simp]
theorem TopCat.leftUnitor_inv_apply {X : TopCat} {x : ↑X} :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) x = (PUnit.unit, x)
source
@[simp]
theorem TopCat.rightUnitor_hom_apply {X : TopCat} {x : ↑X} {p : PUnit.{u + 1}} :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) (x, p) = x
source
@[simp]
theorem TopCat.rightUnitor_inv_apply {X : TopCat} {x : ↑X} :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) x = (x, PUnit.unit)
source
@[simp]
theorem TopCat.associator_hom_apply {X Y Z : TopCat} {x : ↑X} {y : ↑Y} {z : ↑Z} :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) ((x, y), z) = (x, y, z)
source
@[simp]
theorem TopCat.associator_inv_apply {X Y Z : TopCat} {x : ↑X} {y : ↑Y} {z : ↑Z} :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) (x, y, z) = ((x, y), z)
source
@[simp]
theorem TopCat.associator_hom_apply_1 {X Y Z : TopCat} {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)} :
((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) x).1 = x.1.1
source
@[simp]
theorem TopCat.associator_hom_apply_2_1 {X Y Z : TopCat} {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)} :
((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) x).2.1 = x.1.2
source
@[simp]
theorem TopCat.associator_hom_apply_2_2 {X Y Z : TopCat} {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)} :
((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) x).2.2 = x.2
source
@[simp]
theorem TopCat.associator_inv_apply_1_1 {X Y Z : TopCat} {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))} :
((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) x).1.1 = x.1
source
@[simp]
theorem TopCat.associator_inv_apply_1_2 {X Y Z : TopCat} {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))} :
((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) x).1.2 = x.2.1
source
@[simp]
theorem TopCat.associator_inv_apply_2 {X Y Z : TopCat} {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))} :
((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) x).2 = x.2.2
source
@[simp]
theorem TopCat.braiding_hom_apply {X Y : TopCat} {x : ↑X} {y : ↑Y} :
(CategoryTheory.ConcreteCategory.hom (β_ X Y).hom) (x, y) = (y, x)
source
@[simp]
theorem TopCat.braiding_inv_apply {X Y : TopCat} {x : ↑X} {y : ↑Y} :
(CategoryTheory.ConcreteCategory.hom (β_ X Y).inv) (y, x) = (x, y)
source
@[simp]
theorem TopCat.lift_apply {X Y Z : TopCat} {f : X ⟶ Y} {g : X ⟶ Z} {x : ↑X} :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CartesianMonoidalCategory.lift f g)) x = ((CategoryTheory.ConcreteCategory.hom f) x, (CategoryTheory.ConcreteCategory.hom g) x)
source
def TopCat.I :
TopCat

The unit interval, as an object of TopCat.

Equations
Instances For
    source
    instance TopCat.instLocallyCompactSpaceCarrierI :
    LocallyCompactSpace ↑I
    source
    def TopCat.I.homeomorph :
    ↑I ≃ₜ ↑unitInterval

    The unit interval TopCat.I is homeomorphic to unitInterval.

    Equations
    Instances For
      source
      theorem TopCat.I.ext {x y : ↑I} (h : homeomorph x = homeomorph y) :
      x = y
      source
      theorem TopCat.I.ext_iff {x y : ↑I} :
      x = y ↔ homeomorph x = homeomorph y
      source
      def TopCat.I.symm :
      I ⟶ I

      The symmetrization map TopCat.I ⟶ TopCat.I.

      Equations
      Instances For
        source
        @[simp]
        theorem TopCat.I.homeomorph_symm (x : ↑I) :
        homeomorph ((CategoryTheory.ConcreteCategory.hom symm) x) = unitInterval.symm (homeomorph x)
        source
        @[implicit_reducible]
        instance TopCat.I.instOfNatCarrierOfNatNat :
        OfNat (↑I) 0
        Equations
        source
        @[implicit_reducible]
        instance TopCat.I.instOfNatCarrierOfNatNat_1 :
        OfNat (↑I) 1
        Equations
        source
        @[simp]
        theorem TopCat.I.homeomorph_zero :
        homeomorph 0 = 0
        source
        @[simp]
        theorem TopCat.I.homeomorph_one :
        homeomorph 1 = 1
        source
        @[simp]
        theorem TopCat.I.symm_one :
        (CategoryTheory.ConcreteCategory.hom symm) 1 = 0
        source
        @[simp]
        theorem TopCat.I.symm_zero :
        (CategoryTheory.ConcreteCategory.hom symm) 0 = 1
        source
        noncomputable def TopCat.ι₀ {X : TopCat} :
        X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X I

        The inclusion X ⟶ X ⊗ I given by 0 : I for X : TopCat.

        Equations
        Instances For
          source
          @[simp]
          theorem TopCat.ι₀_comp {X Y : TopCat} (f : X ⟶ Y) :
          CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.MonoidalCategoryStruct.whiskerRight f I) = CategoryTheory.CategoryStruct.comp f ι₀
          source
          @[simp]
          theorem TopCat.ι₀_comp_assoc {X Y : TopCat} (f : X ⟶ Y) {Z : TopCat} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y I ⟶ Z) :
          CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f I) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ι₀ h)
          source
          @[simp]
          theorem TopCat.ι₀_fst (X : TopCat) :
          CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.SemiCartesianMonoidalCategory.fst X I) = CategoryTheory.CategoryStruct.id X
          source
          @[simp]
          theorem TopCat.ι₀_fst_assoc (X : TopCat) {Z : TopCat} (h : X ⟶ Z) :
          CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X I) h) = h
          source
          @[simp]
          theorem TopCat.ι₀_snd (X : TopCat) :
          CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.SemiCartesianMonoidalCategory.snd X I) = const 0
          source
          @[simp]
          theorem TopCat.ι₀_snd_assoc (X : TopCat) {Z : TopCat} (h : I ⟶ Z) :
          CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X I) h) = CategoryTheory.CategoryStruct.comp (const 0) h
          source
          @[simp]
          theorem TopCat.ι₀_apply {X : TopCat} (x : ↑X) :
          (CategoryTheory.ConcreteCategory.hom ι₀) x = (x, 0)
          source
          noncomputable def TopCat.ι₁ {X : TopCat} :
          X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X I

          The inclusion X ⟶ X ⊗ I given by 1 : I for X : TopCat.

          Equations
          Instances For
            source
            @[simp]
            theorem TopCat.ι₁_comp {X Y : TopCat} (f : X ⟶ Y) :
            CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.MonoidalCategoryStruct.whiskerRight f I) = CategoryTheory.CategoryStruct.comp f ι₁
            source
            @[simp]
            theorem TopCat.ι₁_comp_assoc {X Y : TopCat} (f : X ⟶ Y) {Z : TopCat} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y I ⟶ Z) :
            CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f I) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ι₁ h)
            source
            @[simp]
            theorem TopCat.ι₁_fst (X : TopCat) :
            CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.SemiCartesianMonoidalCategory.fst X I) = CategoryTheory.CategoryStruct.id X
            source
            @[simp]
            theorem TopCat.ι₁_fst_assoc (X : TopCat) {Z : TopCat} (h : X ⟶ Z) :
            CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X I) h) = h
            source
            @[simp]
            theorem TopCat.ι₁_snd (X : TopCat) :
            CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.SemiCartesianMonoidalCategory.snd X I) = const 1
            source
            @[simp]
            theorem TopCat.ι₁_snd_assoc (X : TopCat) {Z : TopCat} (h : I ⟶ Z) :
            CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X I) h) = CategoryTheory.CategoryStruct.comp (const 1) h
            source
            @[simp]
            theorem TopCat.ι₁_apply {X : TopCat} (x : ↑X) :
            (CategoryTheory.ConcreteCategory.hom ι₁) x = (x, 1)