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.

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.

    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.

      Instances For
        source
        ๐Ÿ”ธ coverage
        @[implicit_reducible]
        instance CommAlgCat.instMonoidalCategory {R : Type u} [CommRing R] :
        CategoryTheory.MonoidalCategory (CommAlgCat R)
        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
        @[implicit_reducible]
        instance CommAlgCat.instBraidedCategory {R : Type u} [CommRing R] :
        CategoryTheory.BraidedCategory (CommAlgCat R)
        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
        @[implicit_reducible]
        instance CommAlgCat.instCartesianMonoidalCategoryOpposite {R : Type u} [CommRing R] :
        CategoryTheory.CartesianMonoidalCategory (CommAlgCat R)แต’แต–
        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) โ‹ฏ