Thin categories, prosets as categories, and poset/toset/lattice #4248

zwang123 · 2024-09-26T13:56:15Z

~~This contains changes in #4242.~~
~~Probably will wait until the previous PR is merged so that I can fix some merge conflicts~~
Now it is the time.

Added

toslat: A toset is a lattice
endmndlem
thinccic: In a thin category, two objects are isomorphic iff there are morphisms between them in both directions.
postc: The converted category is a poset iff no distinct objects are isomorphic.
oppcthin: The opposite of a thin category is thin.
subthinc: A subcategory of a thin category is thin.
functhinc, fullthinc, thincfth: (full) functors to thin categories; faithful functors from thin categories
inpw: Two ways of expressing a collection of subsets
posjidm, posmidm: Poset join/meet is idempotent.
ipolub/ipoglb: LUB/GLB of inclusion poset.
mreclat, mrelatlubALT, and mrelatglbALT: The inclusion poset for a Moore system is a complete lattice
topclat, topdlat, and related
And lots of other theorems supporting the above

Fixed

Description for setc2ohom, latjidm, and latmidm; and others.
Rename monepilem to mpbiran3d and added mpbiran4d.

Changed

Moved to main
- biadanid
- tospos
- tleile
- tltnle

…cepi

set.mm

benjub · 2024-10-01T20:06:12Z

set.mm

@@ -215070,8 +215081,8 @@ an empty base set ( ~ str0 ) and any relation partially orders an empty
      YHYCXFCXMYKVGYHXMFUJYLXIVHYIXFCXMFVIVOVJVKVLCDEKUAVMXHXJKWIXGFFHUOLVPVNVQ
      VRVSNWKXHWMXJKWIWJXGBXFCFBXFVHWPFUBOVTWAWBWLXIKBXFCFOWCWFWDWEWG $.

-    $( Domain of the least upper bound function of a poset.  (Contributed by
-       NM, 6-Sep-2018.) $)
+    $( Domain of the least upper bound function of a set.  (Contributed by NM,


Why? "Poset" is good, here and below.

The definition doesn’t mention anything about poset. In fact for a poset, there is at most one glb/lub for any subset, proved somewhere in dual iirc. So the uniqueness is unnecessary for a poset. See my eldm2 theorems. I think this theorem works for any sets instead of just posets.

The role of comments is not to strictly paraphrase the formal statement (the formal statement suffices for that), but to convey the idea of the statement. "Least upper bound" needs at least some kind of order relation to make sense, even if the encoding in set.mm allows some "junk theorems", so "poset" is good here.

I agree that some order relation must be there for the theorem to be meaningful. But does it have to be a partial order? I suppose a preorder should suffice. The difference is that a preorder could have multiple LUBs/GLBs so existence does not guarantee uniqueness.

I understand that people usually reference GLB/LUB in posets but we could be more creative here.

That's why I wrote "some kind of order relation". Anyway, I think "poset" is good enough, and then people are free to wonder what happens under weaker hypotheses.

benjub · 2024-10-01T20:06:41Z

set.mm

+    $d x y B $.  $d x y X $.  $d y Y $.  $d x y .<_ $.
+    tleile.b $e |- B = ( Base ` K ) $.
+    tleile.l $e |- .<_ = ( le ` K ) $.
+    $( In a Toset, two elements must compare.  (Contributed by Thierry Arnoux,


Suggested change

$( In a Toset, two elements must compare. (Contributed by Thierry Arnoux,

$( In a Toset, any two elements are comparable. (Contributed by Thierry Arnoux,

benjub · 2024-10-01T20:08:27Z

set.mm

+    $( In a Toset, less-than is equivalent to not inverse "less than or equal
+       to" see ~ pltnle .  (Contributed by Thierry Arnoux, 11-Feb-2018.) $)


Suggested change

$( In a Toset, less-than is equivalent to not inverse "less than or equal

to" see ~ pltnle . (Contributed by Thierry Arnoux, 11-Feb-2018.) $)

$( In a Toset, "less than" is equivalent to the negation of the converse of

"less than or equal to", see ~ pltnle . (Contributed by Thierry Arnoux,

11-Feb-2018.) $)

benjub · 2024-10-01T20:08:55Z

set.mm

-    $( Lattice join is idempotent.  (Contributed by NM, 8-Oct-2011.) $)
+    latjidm.b $e |- B = ( Base ` K ) $.
+    latjidm.j $e |- .\/ = ( join ` K ) $.
+    $( Lattice join is idempotent.  ( ~ unidm analog.)  See ~ posjidm for a


Suggested change

$( Lattice join is idempotent. ( ~ unidm analog.) See ~ posjidm for a

$( Lattice join is idempotent. Analogue of ~ unidm analog. See ~ posjidm for a

Same below. Also, remove the "stronger statement" sentence here and below, and do another PR to move those statements from your mathbox to Main.

I could potentially do that but the dependency chain is quite long… Moving those might take a while. Maybe revise it to “see also ~ xxx “ before posjidm and posmidm moved to main?

Also, I think some of the theorems indirectly referenced by these two might depend on dual so #4253 should be handled first.

I cannot look at the details. In short: you can make comments in your mathbox referencing Main, but the opposite is less common. There are many such examples in contributors' mathboxes.

benjub · 2024-10-01T20:13:31Z

set.mm

@@ -217781,12 +217825,13 @@ net proof size (existence part)? $)
  ${
    $d I x y $.  $d C x y $.  $d G x y $.  $d L x y $.  $d U x y $.
    $d F x y $.  $d X x y $.
-    mreclat.i $e |- I = ( toInc ` C ) $.
+    mreclatBAD.i $e |- I = ( toInc ` C ) $.


You cannot make that kind of changes in the main part of set.mm.

If you have proposals for better alternatives, first put them in your mathbox where you can say in the comment there that it is a better alternative, but do not modify the main part. Then, you can propose in an issue to move these to Main or to make other adjustments.

I do not have good proposals. The original theorem is self-referenced BAD. The sole reason I renamed this is that I wanted to prove the good version but couldn’t resolve the name clash. This is just temporary before I move the good version to main.

If renaming a main theorem is an absolute no, I can revert the change and rename mine as GOOD instead.

The database and website are not targeted only at contributors. Imagine a reader who runs into the page for mreclatBAD. That does not give a good image of the website.

I totally agree with you. The bad news, is that, it is already there: https://us.metamath.org/mpeuni/mreclatBAD.html

I am trying to fix it but first I need to polish the fixed one in my Mathbox.

Anyways I will revert the change and rename mine as GOOD. Does that sound okay?

In fact, there are more than one “BAD” theorems in main…

Given that it's just a hypothesis, I'm fine with either renaming this hypothesis BAD or the other hypothesis GOOD
Probably renaming the other hypothesis GOOD would be the option, then

Better to relabel the version in the mathbox, and to not have "BAD" in the main part.

zwang123 · 2024-10-02T13:34:06Z

Out of town now so could not edit before I come back…

benjub · 2024-10-04T23:29:45Z

Let's try and merge it soon. Do not add new theorems or ideas, and only fix open conversations and address existing remarks.

zwang123 · 2024-10-05T10:14:43Z

Let's try and merge it soon. Do not add new theorems or ideas, and only fix open conversations and address existing remarks.

Won’t be back until 2 weeks later as mentioned in #4248 (comment)
Looks like those open conversations are easy fixes but it’s hard to do it on my end…

benjub · 2024-10-05T10:25:47Z

Let's try and merge it soon. Do not add new theorems or ideas, and only fix open conversations and address existing remarks.

Won’t be back until 2 weeks later as mentioned in #4248 (comment) Looks like those open conversations are easy fixes but it’s hard to do it on my end…

No worries. Since it's mostly in your mathbox, merge conflicts will be easily resolved. What I meant is that potential new developments should go in a separate PR (also for ease of review), and that new commits in this PR should be only to address existing comments.

zwang123 added 30 commits September 17, 2024 20:58

Move moel to main; add ThinCat and indiscrete category

efc9759

add thincc

dd59b38

Add catcone0 to main; add catprs, prsthinc and related theorems

ed125d4

remove ax-un dependency in f1omo

eacc384

remove ax-un for 2oexw and prsthinc

18882e4

remove ax-un and ax-pow for indthinc

68f32e5

shorten 2oexw

94f7937

add mo0sn

a5bf4d0

add mofasn2 and related

58ccf8b

add mofsn3 and rename theorems xxfa* -> xxf*

12c113f

add setcthin and setc2othin

ae8003f

shorten proof by mof02

889d39f

rename mofsn3 -> mofmo; and fix description

8ac55a8

Add ProsetToCat defining and important properties

4f1190f

added two redundant hypotheses to prstchom for explicitness

38bae43

add prstchom2ALT

238382a

add thincn0eu and prstchom2

2ed222d

Resolve merge conflict by incorporating both suggestions

0c1f8cd

revive ALT theorems

ed5216e

prevent basendx usage

148e9ac

shorten prstchomval

c5f8254

sylibda->sylbida

2ee397d

Add idmon and idepi

b9220e6

add MndToCat

80c1fd8

add grptcmon and grptcepi

c9e8378

add dtrucor3

3b043e4

merge develop and resolve conflict

49325b7

add monepilem, thincid, thincmon, thincepi; shorten grptcmon and grpt…

d311b8d

…cepi

add mndtcbas2

fc498a5

revise mndtcco2; add thinccic and related; add thinccd to shorten proofs

dda1028

benjub reviewed Sep 26, 2024

View reviewed changes

set.mm Outdated Show resolved Hide resolved

zwang123 added 3 commits September 27, 2024 10:53

monepilem -> mpbiran3d; add mpbiran4d

e1ac292

rename: catmnd -> endmndlem

dcd2a97

add posjidm and posmidm; fix latjidm and latmidm

685c75e

avekens mentioned this pull request Sep 27, 2024

Move 'monoid of endomorphisms' subsection from my mathbox to Main. #4249

Open

zwang123 added 7 commits September 28, 2024 13:51

add ipolubdm and related

19cc828

prove ipolub

3d8d787

prove ipoglb and ipoglbdm

5f24022

add oppcthin

23c8fe3

Resolve merge conflict

5b9cc98

fix descriptions

3467275

add mreclat, mrelatlubALT, and mrelatglbALT

ba21945

zwang123 marked this pull request as ready for review September 29, 2024 15:33

zwang123 added 2 commits September 30, 2024 02:53

Add topclat

51d15fd

Add ipolub00, ipoglb0; toplatlub/toplatglb/toplatglb0

6c480da

zwang123 requested a review from benjub September 30, 2024 03:53

zwang123 added 8 commits September 30, 2024 18:24

add topdlat and related

21759cc

add subthinc

7780eec

Add fullthinc

386c83d

revise fullthinc; add fullthinc2

a1fdf3d

add thincfth

2b0225f

move theorems related to functions to its right place

03deb08

Add functhinc; functhinclem1 -> mofeu

f228c53

detailed descriptions

344b2bb

benjub reviewed Oct 1, 2024

View reviewed changes

icecream17 mentioned this pull request Oct 4, 2024

Remove ax-riotaBAD [mathbox] #4265

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Thin categories, prosets as categories, and poset/toset/lattice #4248

Thin categories, prosets as categories, and poset/toset/lattice #4248

zwang123 commented Sep 26, 2024 •

edited

Loading

benjub Oct 1, 2024

zwang123 Oct 2, 2024

benjub Oct 2, 2024

zwang123 Oct 3, 2024

benjub Oct 4, 2024

benjub Oct 1, 2024

benjub Oct 1, 2024

benjub Oct 1, 2024

benjub Oct 1, 2024

zwang123 Oct 2, 2024

benjub Oct 2, 2024

benjub Oct 1, 2024

zwang123 Oct 2, 2024 •

edited

Loading

benjub Oct 2, 2024 •

edited

Loading

zwang123 Oct 3, 2024

zwang123 Oct 3, 2024

icecream17 Oct 4, 2024 •

edited

Loading

benjub Oct 4, 2024

zwang123 commented Oct 2, 2024

benjub commented Oct 4, 2024

zwang123 commented Oct 5, 2024

benjub commented Oct 5, 2024

	$( In a Toset, two elements must compare. (Contributed by Thierry Arnoux,
	$( In a Toset, any two elements are comparable. (Contributed by Thierry Arnoux,

		$( In a Toset, less-than is equivalent to not inverse "less than or equal
		to" see ~ pltnle . (Contributed by Thierry Arnoux, 11-Feb-2018.) $)

	$( Lattice join is idempotent. ( ~ unidm analog.) See ~ posjidm for a
	$( Lattice join is idempotent. Analogue of ~ unidm analog. See ~ posjidm for a

Thin categories, prosets as categories, and poset/toset/lattice #4248

Are you sure you want to change the base?

Thin categories, prosets as categories, and poset/toset/lattice #4248

Conversation

zwang123 commented Sep 26, 2024 • edited Loading

Added

Fixed

Changed

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zwang123 Oct 2, 2024 • edited Loading

Choose a reason for hiding this comment

benjub Oct 2, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

icecream17 Oct 4, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zwang123 commented Oct 2, 2024

benjub commented Oct 4, 2024

zwang123 commented Oct 5, 2024

benjub commented Oct 5, 2024

zwang123 commented Sep 26, 2024 •

edited

Loading

zwang123 Oct 2, 2024 •

edited

Loading

benjub Oct 2, 2024 •

edited

Loading

icecream17 Oct 4, 2024 •

edited

Loading