Commit 2025-09-17 06:03 d7c56523

View on Github →

chore: rename Mon_, Comon_, ... to Mon, Comon, etc (#29660) Moves:

  • Mon_ -> Mon
  • Comon_ -> Comon
  • Bimon_ -> Bimon
  • Hopf_ -> Hopf
  • IsMon_Hom -> IsMonHom
  • IsComon_Hom -> IsComonHom
  • IsBimon_Hom -> IsBimonHom Mod_ and Grp_/CommGrp_ will follow in a later PR. Zulip

Estimated changes

modified def CoalgCat.toComon
modified theorem Bimod.id_whiskerLeft_bimod
modified theorem Bimod.id_whiskerRight_bimod
modified def Bimod.isoOfIso
modified theorem Bimod.pentagon_bimod
modified theorem Bimod.triangle_bimod
modified theorem Bimod.whiskerLeft_id_bimod
modified theorem Bimod.whiskerRight_id_bimod
modified theorem Bimod.whisker_assoc_bimod
modified structure Bimod
added theorem Bimon.comp_hom'
added theorem Bimon.compatibility
added theorem Bimon.ext
added def Bimon.forget
added theorem Bimon.id_hom'
added def Bimon.mk'
added def Bimon.mk'X
added theorem Bimon.mul_counit
added def Bimon.ofMonComon
added theorem Bimon.one_comul
added def Bimon.toComon
added theorem Bimon.toComon_forget
added def Bimon.toMonComon
added theorem Bimon.toMon_forget
added def Bimon.toTrivial
added def Bimon.trivial
added def Bimon.trivialTo
added def Bimon
deleted theorem Bimon_.BimonObjAux_comul
deleted theorem Bimon_.BimonObjAux_counit
deleted theorem Bimon_.comp_hom'
deleted theorem Bimon_.compatibility
deleted theorem Bimon_.ext
deleted def Bimon_.forget
deleted theorem Bimon_.id_hom'
deleted def Bimon_.mk'
deleted def Bimon_.mk'X
deleted theorem Bimon_.mul_counit
deleted def Bimon_.ofMon_Comon_
deleted theorem Bimon_.one_comul
deleted def Bimon_.toComon_
deleted theorem Bimon_.toComon_forget
deleted def Bimon_.toMon_Comon_
deleted theorem Bimon_.toMon_forget
deleted def Bimon_.toTrivial
deleted def Bimon_.trivial
deleted def Bimon_.trivialTo
deleted def Bimon_
added def cartesianComon
deleted def cartesianComon_
modified def comonEquiv
deleted def iso_cartesianComon_
modified theorem GrpObj.div_comp
modified theorem GrpObj.inv_comp
modified theorem GrpObj.zpow_comp
modified def Grp_.homMk
modified def Mod_.trivialAction
added theorem Mon.fst_hom
added theorem Mon.lift_hom
added theorem Mon.snd_hom
modified theorem MonObj.mul_comp
modified theorem MonObj.one_comp
modified theorem MonObj.pow_comp
deleted theorem Mon_.fst_hom
deleted theorem Mon_.lift_hom
deleted theorem Mon_.snd_hom
modified def yonedaMon
modified theorem CommGrp_.id'
modified theorem CommGrp_.id_hom
deleted def CommGrp_.toCommMon_
added theorem CommMon.comp'
added theorem CommMon.comp_hom
added def CommMon.forget
added theorem CommMon.hom_ext
added theorem CommMon.id'
added theorem CommMon.id_hom
added def CommMon.mkIso'
added def CommMon.toMon
added def CommMon.trivial
added structure CommMon
deleted theorem CommMon_.comp'
deleted theorem CommMon_.comp_hom
deleted def CommMon_.forget
deleted theorem CommMon_.hom_ext
deleted theorem CommMon_.id'
deleted theorem CommMon_.id_hom
deleted def CommMon_.mkIso'
deleted def CommMon_.toMon_
deleted def CommMon_.trivial
deleted structure CommMon_
added structure Comon.Hom
added def Comon.comp
added theorem Comon.comp_hom'
added theorem Comon.ext
added def Comon.forget
added theorem Comon.forget_δ
added theorem Comon.forget_ε
added theorem Comon.forget_η
added theorem Comon.forget_μ
added def Comon.id
added theorem Comon.id_hom'
added def Comon.mkIso'
added def Comon.mkIso
added theorem Comon.tensorObj_X
added theorem Comon.tensorObj_comul'
added theorem Comon.tensorObj_comul
added theorem Comon.tensorObj_counit
added def Comon.trivial
added structure Comon
deleted structure Comon_.Hom
deleted def Comon_.comp
deleted theorem Comon_.comp_hom'
deleted theorem Comon_.ext
deleted def Comon_.forget
deleted theorem Comon_.forget_δ
deleted theorem Comon_.forget_ε
deleted theorem Comon_.forget_η
deleted theorem Comon_.forget_μ
deleted def Comon_.id
deleted theorem Comon_.id_hom'
deleted def Comon_.mkIso'
deleted def Comon_.mkIso
deleted theorem Comon_.tensorObj_X
deleted theorem Comon_.tensorObj_comul'
deleted theorem Comon_.tensorObj_comul
deleted theorem Comon_.tensorObj_counit
deleted def Comon_.trivial
deleted structure Comon_
modified theorem GrpObj.inv_hom
modified theorem GrpObj.lift_inv_comp_left
modified theorem GrpObj.lift_inv_comp_right
modified theorem Grp_.id'
modified theorem Grp_.id_hom
added def Grp_.toMon
deleted def Grp_.toMon_
added def Hopf.toBimon
added structure Hopf
modified theorem HopfObj.hom_antipode
deleted def Hopf_.toBimon_
deleted structure Hopf_
added def Mon.limit
added def Mon.limitCone
deleted def Mon_.limit
deleted def Mon_.limitCone
modified def Mod_.comap
added theorem Mon.Hom.ext'
added structure Mon.Hom
added def Mon.comp
added theorem Mon.comp_hom'
added def Mon.forget
added theorem Mon.hom_injective
added def Mon.id
added theorem Mon.id_hom'
added def Mon.mkIso'
added def Mon.trivial
added structure Mon
deleted theorem Mon_.Hom.ext'
deleted structure Mon_.Hom
deleted def Mon_.comp
deleted theorem Mon_.comp_hom'
deleted def Mon_.forget
deleted theorem Mon_.hom_injective
deleted def Mon_.id
deleted theorem Mon_.id_hom'
deleted def Mon_.mkIso'
deleted def Mon_.trivial
deleted structure Mon_
modified def MonObj.mopEquiv