Commit 2024-07-15 20:56 4831f315

View on Github →

feat: the category of Hopf algebras (#12010) The category of Hopf algebras over a commutative ring. Mimics Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.

Estimated changes

Modified Mathlib.lean

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

added def BialgEquiv.toHopfAlgebraCatIso

added theorem BialgEquiv.toHopfAlgebraCatIso_refl

added theorem BialgEquiv.toHopfAlgebraCatIso_symm

added theorem BialgEquiv.toHopfAlgebraCatIso_trans

added def CategoryTheory.Iso.toHopfAlgEquiv

added theorem CategoryTheory.Iso.toHopfAlgEquiv_refl

added theorem CategoryTheory.Iso.toHopfAlgEquiv_symm

added theorem CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom

added theorem CategoryTheory.Iso.toHopfAlgEquiv_trans

added theorem HopfAlgebraCat.Hom.toBialgHom_injective

added structure HopfAlgebraCat.Hom

added theorem HopfAlgebraCat.forget₂_bialgebra_map

added theorem HopfAlgebraCat.forget₂_bialgebra_obj

added theorem HopfAlgebraCat.hom_ext

added def HopfAlgebraCat.of

added theorem HopfAlgebraCat.of_comul

added theorem HopfAlgebraCat.of_counit

added theorem HopfAlgebraCat.toBialgHom_comp

added theorem HopfAlgebraCat.toBialgHom_id

added structure HopfAlgebraCat