Commit 2025-02-09 16:53 651f76be

View on Github →

feat(CategoryTheory): group objects (#21347) Define group objects in cartesian monoidal categories. Show that the associativity diagram of a group object is always cartesian and deduce that morphisms of group objects commute with taking inverses. Show that a finite-product-preserving functor takes group objects to group objects.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

added theorem Mon_.lift_comp_one_left

added theorem Mon_.lift_comp_one_right

added theorem Mon_.lift_lift_assoc

Created Mathlib/CategoryTheory/Monoidal/Grp_.lean

added theorem Grp_.comp'

added theorem Grp_.comp_hom

added theorem Grp_.eq_lift_inv_left

added theorem Grp_.eq_lift_inv_right

added def Grp_.forget

added def Grp_.forget₂Mon_

added theorem Grp_.forget₂Mon_comp_forget

added theorem Grp_.forget₂Mon_map_hom

added theorem Grp_.forget₂Mon_obj_mul

added theorem Grp_.forget₂Mon_obj_one

added def Grp_.fullyFaithfulForget₂Mon_

added theorem Grp_.hom_ext

added theorem Grp_.id'

added theorem Grp_.id_hom

added theorem Grp_.inv_hom

added theorem Grp_.isPullback

added theorem Grp_.lift_comp_inv_left

added theorem Grp_.lift_comp_inv_right

added theorem Grp_.lift_inv_comp_left

added theorem Grp_.lift_inv_comp_right

added theorem Grp_.lift_inv_left_eq

added theorem Grp_.lift_inv_right_eq

added def Grp_.mkIso

added theorem Grp_.mkIso_hom_hom

added theorem Grp_.mkIso_inv_hom

added def Grp_.trivial

added structure Grp_