Skip to content

LRS does not have a small generating set#225

Merged
ScriptRaccoon merged 2 commits into
ScriptRaccoon:mainfrom
dschepler:lrs-no-generator-set
Jun 2, 2026
Merged

LRS does not have a small generating set#225
ScriptRaccoon merged 2 commits into
ScriptRaccoon:mainfrom
dschepler:lrs-no-generator-set

Conversation

@dschepler
Copy link
Copy Markdown
Contributor

@dschepler dschepler commented Jun 2, 2026

This took the number of unknown properties of LRS from 27 to 16.


  • unknown (category, property)-pairs before this PR: 108
  • unknown (category, property)-pairs after this PR: 97

Comment thread databases/catdat/data/categories/LRS.yaml Outdated
@ScriptRaccoon
Copy link
Copy Markdown
Owner

This took the number of unknown properties of LRS from 27 to 16.

Great progress! 🙏🏻

@ScriptRaccoon
Copy link
Copy Markdown
Owner

ScriptRaccoon commented Jun 2, 2026

Here is an alternative proof.

Lemma: Let C be a full reflective subcategory of D. Assume that D has a generating set. Then C has a generating set. (Namely, the reflector applied to a generating set.)

Apply this to the category of affine schemes which is a reflective category of the category of locally ringed spaces. The reflector maps X to the spectrum of the ring of global sections of X. But the category of affine schemes has no generating set since CRing has no cogenerating set.

This also provides an alternative proof for the category of schemes.

(I hope this is correct. I am not fully concentrating right now and will check the details later.)

@ScriptRaccoon
Copy link
Copy Markdown
Owner

ScriptRaccoon commented Jun 2, 2026

Actually, your proof heavily reminds me of the lemma on Missing cogenerating sets which we already use for categories like CRing. Maybe it applies (dualized) by taking F to be the collection of spectra of fields. We only need to define U.

@dschepler
Copy link
Copy Markdown
Contributor Author

dschepler commented Jun 2, 2026

I guess the functor of taking a space to its collection of residue fields could be viewed as a functor $\mathbf{LRS} \to \mathbf{Set}^\rightarrow$ where $X$ maps to the morphism with codomain given by the underlying set of $X$ and domain given by the disjoint union of (the underlying sets of) the residue fields. And for morphisms $f : X \to Y$ we get an injective map from the pullback of $U(Y)$ and the underlying set map of $f$ to the domain of $U(X)$ -- so I guess the target category is not quite $\mathbf{Set}^\rightarrow$ but something with modified morphisms. And even though $U$ might be faithful in some sense, we don't actually need the full power of faithfulness of $U$, just that it acts faithfully on endomorphisms of the objects in $\mathbf{F}$ -- for which in this case, $U$ on any object in $\mathbf{F}$ has a singleton codomain.

But anyway, all that setup seems like a lot of unnecessary complication to generalize the lemma just for this one case.

Edit: A bit of Google searching gave a name of the target category, such that the functor described is a contravariant functor from $\mathbf{LRS}$ to "the total category of the codomain fibration over $\mathbf{Set}$". And I was reminded this is not a faithful functor in general (for example looking at the endomorphisms of $\mathbb{C}[\varepsilon] / \langle \varepsilon^2 \rangle$), so the refinement to use faithfulness on endomorphisms of objects in $\mathbf{F}$ is important in this case.

@ScriptRaccoon
Copy link
Copy Markdown
Owner

Alright. I have made a commit where I have adjusted your proof slightly, and where I also added the alternative proof using the adjunction. Can you please check if it is OK for you?

@dschepler
Copy link
Copy Markdown
Contributor Author

Yes, the edits you made look good to me.

@ScriptRaccoon ScriptRaccoon merged commit f2635bb into ScriptRaccoon:main Jun 2, 2026
1 check passed
@dschepler dschepler deleted the lrs-no-generator-set branch June 2, 2026 15:42
@ScriptRaccoon
Copy link
Copy Markdown
Owner

ScriptRaccoon commented Jun 2, 2026

I just noticed that it's even easier to prove that LRS and Sch don't have a cogenerating set. PR will follow soon.

I made a mistake.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants