Commit 2025-08-31 05:03 50468bbd

View on Github →

feat: the category of commutative bialgebras (#27120) Define the bundled category CommBialgCat R of commutative bialgebras over a fixed commutative ring R along with the forgetful functor to CommAlgCat. From Toric

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/CommAlgCat/Basic.lean

added def CommAlgCat.algEquivOfIso

deleted def CommAlgCat.ofIso

Created Mathlib/Algebra/Category/CommBialgCat.lean

added theorem CommAlgCat.mul_op_of_unop_hom

added theorem CommAlgCat.one_op_of_unop_hom

added def CommBialgCat.Hom.Simps.hom

added structure CommBialgCat.Hom

added def CommBialgCat.bialgEquivOfIso

added theorem CommBialgCat.coe_of

added theorem CommBialgCat.comp_apply

added theorem CommBialgCat.forget_map

added theorem CommBialgCat.forget_obj

added theorem CommBialgCat.forget₂_commAlgCat_map

added theorem CommBialgCat.forget₂_commAlgCat_obj

added theorem CommBialgCat.hom_comp

added theorem CommBialgCat.hom_ext

added theorem CommBialgCat.hom_id

added theorem CommBialgCat.hom_inv_apply

added theorem CommBialgCat.hom_ofHom

added theorem CommBialgCat.id_apply

added theorem CommBialgCat.inv_hom_apply

added def CommBialgCat.isoEquivBialgEquiv

added def CommBialgCat.isoMk

added theorem CommBialgCat.ofHom_apply

added theorem CommBialgCat.ofHom_comp

added theorem CommBialgCat.ofHom_hom

added theorem CommBialgCat.ofHom_id

added def CommBialgCat.ofSelfIso

added structure CommBialgCat

added def commBialgCatEquivComonCommAlgCat

added theorem commBialgCatEquivComonCommAlgCat_functor_map_unop_hom

added theorem commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom