Commit 2025-01-30 16:37 4f099bd2

View on Github →

feat(Algebra/Category): concrete category refactor for MonCat (#21222) This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 This PR updates the concrete category definitions of (Add)(Comm)MonCat to match the standard set by AlgebraCat, ModuleCat and RingCat:

  • Package objects and homs into structures.
  • Replace HasForget with ConcreteCategory.
  • Set up a good @[simp] set.
  • Ensure constructors and projections are reducible. See MathlibTest/CategoryTheory/ConcreteCategory/MonCat.lean for the specification of all the new functionality. Currently there are still a couple issues around actions and tensor products, where simp [the_lemma] doesn't work even though simp [(the_lemma)] does. Not sure why this is happening, the discrimination tree keys look perfectly normal and trace.Meta.Tactic.simp doesn't say anything useful. I have not tried to look for code that can be cleaned up now, only at what broke. I want to get started on cleanup when the other concrete category instances are in.

Estimated changes

added structure AddCommMonCat.Hom
added structure AddCommMonCat
added structure AddMonCat.Hom
added structure AddMonCat
added structure CommMonCat.Hom
added theorem CommMonCat.comp_apply
added theorem CommMonCat.hom_comp
added theorem CommMonCat.hom_ext
added theorem CommMonCat.hom_id
added theorem CommMonCat.hom_ofHom
added theorem CommMonCat.id_apply
deleted def CommMonCat.of
deleted def CommMonCat.ofHom
added theorem CommMonCat.ofHom_comp
added theorem CommMonCat.ofHom_hom
added theorem CommMonCat.ofHom_id
added structure CommMonCat
deleted def CommMonCat
added structure MonCat.Hom
modified theorem MonCat.coe_of
added theorem MonCat.comp_apply
modified theorem MonCat.forget_map
added theorem MonCat.hom_comp
added theorem MonCat.hom_ext
added theorem MonCat.hom_id
added theorem MonCat.hom_inv_apply
added theorem MonCat.hom_ofHom
added theorem MonCat.hom_one
added theorem MonCat.id_apply
added theorem MonCat.inv_hom_apply
deleted def MonCat.of
deleted def MonCat.ofHom
added theorem MonCat.ofHom_comp
added theorem MonCat.ofHom_hom
added theorem MonCat.ofHom_id
modified theorem MonCat.oneHom_apply
added structure MonCat
deleted def MonCat
modified theorem MonoidHom.comp_id_monCat
modified theorem MonoidHom.id_monCat_comp
modified theorem Action.ρ_one
modified theorem Action.tensorUnit_ρ
modified theorem Action.tensor_ρ