Commit 2024-06-10 20:38 c95c52ea

View on Github →

feat: category of bialgebras (#11973) The category of bialgebras over a commutative ring. Mimics Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.lean.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/BialgebraCat/Basic.lean

added def BialgEquiv.toBialgebraCatIso

added theorem BialgEquiv.toBialgebraCatIso_refl

added theorem BialgEquiv.toBialgebraCatIso_symm

added theorem BialgEquiv.toBialgebraCatIso_trans

added theorem BialgebraCat.Hom.toBialgHom_injective

added structure BialgebraCat.Hom

added theorem BialgebraCat.forget₂_algebra_map

added theorem BialgebraCat.forget₂_algebra_obj

added theorem BialgebraCat.forget₂_coalgebra_map

added theorem BialgebraCat.forget₂_coalgebra_obj

added theorem BialgebraCat.hom_ext

added def BialgebraCat.of

added theorem BialgebraCat.of_comul

added theorem BialgebraCat.of_counit

added theorem BialgebraCat.toBialgHom_comp

added theorem BialgebraCat.toBialgHom_id

added structure BialgebraCat

added def CategoryTheory.Iso.toBialgEquiv

added theorem CategoryTheory.Iso.toBialgEquiv_refl

added theorem CategoryTheory.Iso.toBialgEquiv_symm

added theorem CategoryTheory.Iso.toBialgEquiv_toBialgHom

added theorem CategoryTheory.Iso.toBialgEquiv_trans

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

added def CoalgEquiv.toCoalgebraCatIso

added theorem CoalgEquiv.toCoalgebraCatIso_refl

added theorem CoalgEquiv.toCoalgebraCatIso_symm

added theorem CoalgEquiv.toCoalgebraCatIso_trans

deleted def CoalgEquiv.toIso

deleted theorem CoalgEquiv.toIso_refl

deleted theorem CoalgEquiv.toIso_symm

deleted theorem CoalgEquiv.toIso_trans