Documentation

Mathlib.Algebra.Category.CommAlgCat.Monoidal

The co-Cartesian monoidal category structure on commutative R-algebras #

This file provides the co-Cartesian-monoidal category structure on CommAlgCat R constructed explicitly using the tensor product.

source
๐Ÿ”ธ coverage
def CommAlgCat.binaryCofan {R : Type u} [CommRing R] (A B : CommAlgCat R) :
CategoryTheory.Limits.BinaryCofan A B

The explicit cocone with tensor products as the fibered coproduct in CommAlgCat.

Equations
    Instances For
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem CommAlgCat.binaryCofan_inl {R : Type u} [CommRing R] (A B : CommAlgCat R) :
      (A.binaryCofan B).inl = ofHom Algebra.TensorProduct.includeLeft
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem CommAlgCat.binaryCofan_inr {R : Type u} [CommRing R] (A B : CommAlgCat R) :
      (A.binaryCofan B).inr = ofHom Algebra.TensorProduct.includeRight
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem CommAlgCat.binaryCofan_pt {R : Type u} [CommRing R] (A B : CommAlgCat R) :
      (A.binaryCofan B).pt = of R (TensorProduct R โ†‘A โ†‘B)
      source
      ๐Ÿ”ธ coverage
      def CommAlgCat.binaryCofanIsColimit {R : Type u} [CommRing R] (A B : CommAlgCat R) :
      CategoryTheory.Limits.IsColimit (A.binaryCofan B)

      Verify that the pushout cocone is indeed the colimit.

      Equations
        Instances For
          source
          ๐Ÿ”ธ coverage
          def CommAlgCat.isInitialSelf {R : Type u} [CommRing R] :
          CategoryTheory.Limits.IsInitial (of R R)

          The initial object of CommAlgCat R is R as an algebra over itself.

          Equations
            Instances For
              source
              ๐Ÿ”ธ coverage
              instance CommAlgCat.instMonoidalCategory {R : Type u} [CommRing R] :
              CategoryTheory.MonoidalCategory (CommAlgCat R)
              Equations
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem CommAlgCat.coe_tensorUnit {R : Type u} [CommRing R] :
                โ†‘(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CommAlgCat R)) = R
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem CommAlgCat.coe_tensorObj {R : Type u} [CommRing R] (A B : CommAlgCat R) :
                โ†‘(CategoryTheory.MonoidalCategoryStruct.tensorObj A B) = TensorProduct R โ†‘A โ†‘B
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem CommAlgCat.tensorHom_hom {R : Type u} [CommRing R] {A B C D : CommAlgCat R} (f : A โŸถ C) (g : B โŸถ D) :
                Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = Algebra.TensorProduct.map (Hom.hom f) (Hom.hom g)
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem CommAlgCat.whiskerRight_hom {R : Type u} [CommRing R] {A B : CommAlgCat R} (C : CommAlgCat R) (f : A โŸถ B) :
                Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f C) = Algebra.TensorProduct.map (Hom.hom f) (AlgHom.id R โ†‘C)
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem CommAlgCat.whiskerLeft_hom {R : Type u} [CommRing R] {A B : CommAlgCat R} (C : CommAlgCat R) (f : A โŸถ B) :
                Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft C f) = Algebra.TensorProduct.map (AlgHom.id R โ†‘C) (Hom.hom f)
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem CommAlgCat.associator_hom_hom {R : Type u} [CommRing R] (A B C : CommAlgCat R) :
                Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator A B C).hom = โ†‘(Algebra.TensorProduct.assoc R R R โ†‘A โ†‘B โ†‘C)
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem CommAlgCat.associator_inv_hom {R : Type u} [CommRing R] (A B C : CommAlgCat R) :
                Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator A B C).inv = โ†‘(Algebra.TensorProduct.assoc R R R โ†‘A โ†‘B โ†‘C).symm
                source
                ๐Ÿ”ธ coverage
                instance CommAlgCat.instBraidedCategory {R : Type u} [CommRing R] :
                CategoryTheory.BraidedCategory (CommAlgCat R)
                Equations
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem CommAlgCat.braiding_hom_hom {R : Type u} [CommRing R] (A B : CommAlgCat R) :
                  Hom.hom (ฮฒ_ A B).hom = โ†‘(Algebra.TensorProduct.comm R โ†‘A โ†‘B)
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem CommAlgCat.braiding_inv_hom {R : Type u} [CommRing R] (A B : CommAlgCat R) :
                  Hom.hom (ฮฒ_ A B).inv = โ†‘(Algebra.TensorProduct.comm R โ†‘B โ†‘A)
                  source
                  ๐Ÿ“ coverage
                  theorem Quiver.Hom.unop_inj_iff {C : Type uโ‚} [Quiver C] {X Y : Cแต’แต–} {aโ‚ aโ‚‚ : X โŸถ Y} :
                  aโ‚ = aโ‚‚ โ†” aโ‚.unop = aโ‚‚.unop
                  source
                  ๐Ÿ”ธ coverage
                  instance CommAlgCat.instCartesianMonoidalCategoryOpposite {R : Type u} [CommRing R] :
                  CategoryTheory.CartesianMonoidalCategory (CommAlgCat R)แต’แต–
                  Equations
                    source
                    ๐Ÿ“ coverage
                    @[simp]
                    theorem CommAlgCat.fst_unop_hom {R : Type u} [CommRing R] (A B : (CommAlgCat R)แต’แต–) :
                    Hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst A B).unop = Algebra.TensorProduct.includeLeft
                    source
                    ๐Ÿ“ coverage
                    @[simp]
                    theorem CommAlgCat.snd_unop_hom {R : Type u} [CommRing R] (A B : (CommAlgCat R)แต’แต–) :
                    Hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.snd A B).unop = Algebra.TensorProduct.includeRight
                    source
                    ๐Ÿ“ coverage
                    @[simp]
                    theorem CommAlgCat.toUnit_unop_hom {R : Type u} [CommRing R] (A : (CommAlgCat R)แต’แต–) :
                    Hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A).unop = Algebra.ofId R โ†‘(Opposite.unop A)
                    source
                    ๐Ÿ“ coverage
                    @[simp]
                    theorem CommAlgCat.lift_unop_hom {R : Type u} [CommRing R] {A B C : (CommAlgCat R)แต’แต–} (f : C โŸถ A) (g : C โŸถ B) :
                    Hom.hom (CategoryTheory.CartesianMonoidalCategory.lift f g).unop = Algebra.TensorProduct.lift (Hom.hom f.unop) (Hom.hom g.unop) โ‹ฏ