Documentation

Mathlib.Algebra.Category.CommAlgCat.Monoidal

The cocartesian monoidal category structure on commutative R-algebras #

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

source
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
      @[simp]
      theorem CommAlgCat.binaryCofan_inl {R : Type u} [CommRing R] (A B : CommAlgCat R) :
      (A.binaryCofan B).inl = ofHom Algebra.TensorProduct.includeLeft
      source
      @[simp]
      theorem CommAlgCat.binaryCofan_inr {R : Type u} [CommRing R] (A B : CommAlgCat R) :
      (A.binaryCofan B).inr = ofHom Algebra.TensorProduct.includeRight
      source
      @[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
      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
          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
              instance CommAlgCat.instMonoidalCategory {R : Type u} [CommRing R] :
              CategoryTheory.MonoidalCategory (CommAlgCat R)
              Equations
                source
                @[simp]
                theorem CommAlgCat.coe_tensorUnit {R : Type u} [CommRing R] :
                ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CommAlgCat R)) = R
                source
                @[simp]
                theorem CommAlgCat.coe_tensorObj {R : Type u} [CommRing R] (A B : CommAlgCat R) :
                ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj A B) = TensorProduct R ↑A ↑B
                source
                @[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
                @[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
                @[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
                @[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 ↑A ↑B ↑C)
                source
                @[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 ↑A ↑B ↑C).symm
                source
                instance CommAlgCat.instBraidedCategory {R : Type u} [CommRing R] :
                CategoryTheory.BraidedCategory (CommAlgCat R)
                Equations
                  source
                  @[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
                  @[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
                  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
                  instance CommAlgCat.instCartesianMonoidalCategoryOpposite {R : Type u} [CommRing R] :
                  CategoryTheory.CartesianMonoidalCategory (CommAlgCat R)ᵒᵖ
                  Equations
                    source
                    @[simp]
                    theorem CommAlgCat.fst_unop_hom {R : Type u} [CommRing R] (A B : (CommAlgCat R)ᵒᵖ) :
                    Hom.hom (CategoryTheory.CartesianMonoidalCategory.fst A B).unop = Algebra.TensorProduct.includeLeft
                    source
                    @[simp]
                    theorem CommAlgCat.snd_unop_hom {R : Type u} [CommRing R] (A B : (CommAlgCat R)ᵒᵖ) :
                    Hom.hom (CategoryTheory.CartesianMonoidalCategory.snd A B).unop = Algebra.TensorProduct.includeRight
                    source
                    @[simp]
                    theorem CommAlgCat.toUnit_unop_hom {R : Type u} [CommRing R] (A : (CommAlgCat R)ᵒᵖ) :
                    Hom.hom (CategoryTheory.CartesianMonoidalCategory.toUnit A).unop = Algebra.ofId R ↑(Opposite.unop A)
                    source
                    @[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) ⋯