Commit 2025-07-11 11:47 765fdacd

View on Github →

feat: CommAlgCat is cocartesian-monoidal (#25365) Construct the cocartesian-monoidal category structure on CommAlgCat R explicitly from the tensor product. From Toric

Estimated changes

deleted structure CategoryTheory.CommAlgCat
added structure CommAlgCat.Hom
added theorem CommAlgCat.coe_of
added theorem CommAlgCat.comp_apply
added theorem CommAlgCat.forget_map
added theorem CommAlgCat.forget_obj
added theorem CommAlgCat.hom_comp
added theorem CommAlgCat.hom_ext
added theorem CommAlgCat.hom_id
added theorem CommAlgCat.hom_ofHom
added theorem CommAlgCat.id_apply
added def CommAlgCat.isoMk
added theorem CommAlgCat.ofHom_apply
added theorem CommAlgCat.ofHom_comp
added theorem CommAlgCat.ofHom_hom
added theorem CommAlgCat.ofHom_id
added def CommAlgCat.ofIso
added structure CommAlgCat