Commit 2024-05-27 14:30 39dd4f33

View on Github →

feat: category of coalgebras (#11972) The category of coalgebras over a commutative ring. Mimics Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Iso.toCoalgEquiv

added theorem CategoryTheory.Iso.toCoalgEquiv_refl

added theorem CategoryTheory.Iso.toCoalgEquiv_symm

added theorem CategoryTheory.Iso.toCoalgEquiv_toCoalgHom

added theorem CategoryTheory.Iso.toCoalgEquiv_trans

added def CoalgEquiv.toIso

added theorem CoalgEquiv.toIso_refl

added theorem CoalgEquiv.toIso_symm

added theorem CoalgEquiv.toIso_trans

added theorem CoalgebraCat.Hom.toCoalgHom_injective

added structure CoalgebraCat.Hom

added theorem CoalgebraCat.forget₂_map

added theorem CoalgebraCat.forget₂_obj

added theorem CoalgebraCat.hom_ext

added theorem CoalgebraCat.moduleCat_of_toModuleCat

added def CoalgebraCat.of

added theorem CoalgebraCat.of_comul

added theorem CoalgebraCat.of_counit

added theorem CoalgebraCat.toCoalgHom_comp

added theorem CoalgebraCat.toCoalgHom_id

added structure CoalgebraCat