search

metamath / set.mm

Metamath source file for logic and set theory
Other
244 stars 88 forks source link

Update of the topological structure overview figure #3805

Open tirix opened 7 months ago

tirix commented 7 months ago

As mentioned by @benjub in #3801 :

regarding https://us.metamath.org/mpeuni/mmtopstr.html can you:

  • update "SGrp" to "Smgrp" and "SemiGroup" to "Semigroup"
  • remove the arrows from Rng to Grp and from Ring to Abel and replace them with an arrow from Rng to Abel ?
  • what is the double arrow from "Neutral element" to "Set" ? Probably a glitch ?
  • the blue arrow "mulGrp" should probably target "Monoid"
  • Preset --> Proset
  • For Ring, is it possible to put the star as a normal character instead of a superscript ? (same with r)
tirix commented 7 months ago

what is the double arrow from "Neutral element" to "Set" ? Probably a glitch ?

The blue arrows are for structure components/properties, and the bold arrows for subset relationships. The fact that a neutral element is an element of the base set is a membership relation, so none of the above. It's not used elsewhere so maybe I should simply remove it.

benjub commented 7 months ago

The fact that a neutral element is an element of the base set is a membership relation, so none of the above. It's not used elsewhere so maybe I should simply remove it.

Ah, I see. Yes, I think removing it makes the picture clearer. The "Ring Unit" is also an element, and the other circles are functions from the base set to the base set. I think it is not necessary to indicate these relations.

icecream17 commented 7 months ago

In addition to df-sgrp, there are also some 404 links due to label changes:

df-rng --> df-ring df-preset --> df-proset

(Technically there is a ringLMod arrow from Ring to LMod and CRing to AssAlg, but it seems too complicated to add under the current design)

There is also an arrow from https://us.metamath.org/mpeuni/df-rng0.html to Abel because of the definition but I'm not sure if this is standard

benjub commented 7 months ago

There is also an arrow from https://us.metamath.org/mpeuni/df-rng0.html to Abel because of the definition but I'm not sure if this is standard

That's the one in the initial post of this issue, isn't it ?

After the link in the "Structures" page is corrected, @avekens's ~df-rng0 can probably be relabeled df-rng (after having checked that the label/label-root for rings is indeed ring everywhere, and not rng).

@avekens : for rng morphisms, I would use the token and symbol RngHom instead of RngHomo: the latter is very uncommon (the "Homo" part does not make me think of morphisms, but rather of homo sapiens, homo habilis and friends !).