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
    • One or more equations did not get rendered due to their size.
    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
        • One or more equations did not get rendered due to their size.
        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
        • One or more equations did not get rendered due to their size.
        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
        • One or more equations did not get rendered due to their size.
        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) ⋯