Commit 2024-12-13 13:44 ddbd4951

View on Github →

refactor(Algebra/Category/Ring): make morphisms a structure (#19757) Following the pattern of #19065, we introduce a Hom structure for morphisms in SemiRingCat, CommSemiRingCat, RingCat and CommRingCat allowing for many simplified proofs and reducing the need of erw. Besides the additional explicitness in form of ofHom and Hom.hom, the main regression is friction with the FunLike instance from the general ConcreteCategory API, causing the need for explicit rws between f.hom x and (forget RingCat).map f x. This regression can be fixed by replacing the general ConcreteCategory.instFunLike by a CoeFun (or FunLike) instance that is part of the ConcreteCategory data.

Estimated changes

modified structure BialgebraCat
added structure BoolRing.Hom
added theorem BoolRing.hom_ext
deleted def BoolRing.of
added structure BoolRing
deleted def BoolRing
modified structure HopfAlgebraCat
added structure CommRingCat.Hom
deleted theorem CommRingCat.coe_comp
deleted theorem CommRingCat.coe_comp_of'
deleted theorem CommRingCat.coe_comp_of
deleted theorem CommRingCat.coe_id
deleted theorem CommRingCat.coe_id_of
modified theorem CommRingCat.coe_of
modified theorem CommRingCat.comp_apply
deleted theorem CommRingCat.ext
deleted theorem CommRingCat.ext_of
modified theorem CommRingCat.forget_map
modified theorem CommRingCat.forget_obj
added theorem CommRingCat.hom_comp
added theorem CommRingCat.hom_ext
added theorem CommRingCat.hom_id
added theorem CommRingCat.hom_ofHom
modified theorem CommRingCat.id_apply
deleted def CommRingCat.of
deleted def CommRingCat.ofHom
deleted theorem CommRingCat.ofHom_apply'
modified theorem CommRingCat.ofHom_apply
added theorem CommRingCat.ofHom_comp
added theorem CommRingCat.ofHom_hom
added theorem CommRingCat.ofHom_id
added theorem CommRingCat.of_carrier
added structure CommRingCat
added structure CommSemiRingCat.Hom
deleted theorem CommSemiRingCat.coe_comp
deleted theorem CommSemiRingCat.coe_id
deleted theorem CommSemiRingCat.coe_id_of
modified theorem CommSemiRingCat.coe_of
deleted theorem CommSemiRingCat.ext
deleted theorem CommSemiRingCat.ext_of
modified theorem CommSemiRingCat.forget_map
added theorem CommSemiRingCat.hom_id
deleted def CommSemiRingCat.of
modified theorem CommSemiRingCat.ofHom_apply
added structure CommSemiRingCat
added structure RingCat.Hom
deleted theorem RingCat.RingEquiv_coe_eq
deleted theorem RingCat.coe_comp
deleted theorem RingCat.coe_comp_of'
deleted theorem RingCat.coe_comp_of
deleted theorem RingCat.coe_id
deleted theorem RingCat.coe_id_of
modified theorem RingCat.coe_of
deleted theorem RingCat.coe_ringHom_id
added theorem RingCat.comp_apply
deleted theorem RingCat.ext
deleted theorem RingCat.ext_of
modified theorem RingCat.forget_map
added theorem RingCat.forget_obj
added theorem RingCat.hom_comp
added theorem RingCat.hom_ext
added theorem RingCat.hom_id
added theorem RingCat.hom_inv_apply
added theorem RingCat.hom_ofHom
added theorem RingCat.id_apply
added theorem RingCat.inv_hom_apply
deleted def RingCat.of
deleted def RingCat.ofHom
deleted theorem RingCat.ofHom_apply'
modified theorem RingCat.ofHom_apply
added theorem RingCat.ofHom_comp
added theorem RingCat.ofHom_hom
added theorem RingCat.ofHom_id
added theorem RingCat.of_carrier
added structure RingCat
deleted theorem RingHom.comp_id_ringCat
deleted theorem RingHom.id_ringCat_comp
added structure SemiRingCat.Hom
deleted theorem SemiRingCat.coe_comp
deleted theorem SemiRingCat.coe_comp_of'
deleted theorem SemiRingCat.coe_comp_of
deleted theorem SemiRingCat.coe_id
deleted theorem SemiRingCat.coe_id_of
modified theorem SemiRingCat.coe_of
added theorem SemiRingCat.comp_apply
deleted theorem SemiRingCat.ext
deleted theorem SemiRingCat.ext_of
modified theorem SemiRingCat.forget_map
added theorem SemiRingCat.forget_obj
added theorem SemiRingCat.hom_comp
added theorem SemiRingCat.hom_ext
added theorem SemiRingCat.hom_id
added theorem SemiRingCat.hom_ofHom
added theorem SemiRingCat.id_apply
deleted def SemiRingCat.of
deleted def SemiRingCat.ofHom
deleted theorem SemiRingCat.ofHom_apply'
modified theorem SemiRingCat.ofHom_apply
added theorem SemiRingCat.ofHom_comp
added theorem SemiRingCat.ofHom_hom
added theorem SemiRingCat.ofHom_id
added theorem SemiRingCat.of_carrier
added structure SemiRingCat
deleted def ringEquivIsoRingIso
modified theorem isLocalHom_of_iso
added theorem RingHom.coe_id