@ah oh I guess that makes it somewhat more surprising then

@takeoutweight we have some kind of rechargeable Dyson thingy that for all I can tell works pretty good. I wouldn't be surprised if plug-in beats rechargeable for suction power or something, but I distinctly prefer cordless as a UX. But whatever, if you found something you like better, I'm non ironically happy for you :)

@ah I think it's a pretty common store brand mop

The water in the bucket after first mop of the kitchen floor was as opaque as chocolate milk. I guess all previous pre-mop cleaning attempts were crap.

@amy (but the folks on that thread were super helpful explaining the available workarounds)

@amy except for syntax declarations! you don't seem to get either `hiding` or `renaming` for those, which I found a bit of a roadbump. https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/.E2.9C.94.20Hiding.20notations.20or.20macros.3F/with/512152590

@amy open with renaming has been good enough for me in practice, but maybe I'm not understanding their usecase enough... (https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#Lean___Parser___Command___openRenaming)

@amy I miss being able to use agda-style parameterized anonymous modules in Lean. variable blocks are so close but not quite the same thing...

Karolina brought home a mop bucket with a little foot pedal with kind of a flywheel action that spins the mop around to dry it and I am a boring middle-aged adult enough to say I frickin love it

A funny construction that occurred to me after further ruminating on the post from yesterday.

I guess with parametricity you can faithfully embed any category in types-over-B for a cleverly* chosen B? That's pretty neat.

https://jcreedcmu.github.io/posts/2025-06-13/

*where "cleverly" means "Yonedaly"

@OscarCunningham a sheaf in general need not look like a *vector* bundle, even though it is, loosely speaking, very bundle-y, in being a bunch of local data bundled together

@OscarCunningham ah, good point; I think I can help clarify though. All of sheaves, vector bundles, quasicoherent sheaves all have an aspect of locality to them, which means "sheaves are like vector bundles" is a correct intuition. More specifically, though, I think it is right to say (informally) that
- a scheme S is a sheaf that locally looks like a ring at a sufficiently small open U
- a qc sheaf over S is a sheaf that locally, at U, looks like a module over S(U)

@anuytstt well you've convinced one person at least

anyway for me personally at least, progress in learning mathematics is inexorably tied to decreasing, by patient and strenuous effort, the set of terms that make my brain go "nope nope nope" and immediately shut off

(1) fleshing out the intuition that "qc sheaf : over a scheme :: vector bundle : over a space"
(2) giving a number field example: the nonprincipal ideal (2, 1 + √-5) in ℤ[√-5] is apparently somehow a nontrivial "1-d vector bundle" over Spec(ℤ[√-5]), sort of like the moebius bundle over the circle. This is the kind of thing that feels like actual payoff for the ever-tantalizing slogan that algebraic geometry lets you have geometric intuitions for things that naively aren't at all geometric

I've long been blocked in my algebraic geometry journey by reacting to the phrase "quasicoherent sheaf" by skittering under the bed and screeching in terror, BUT i should have simply skipped ahead to episode 28 of borcherd's alggeo series (https://www.youtube.com/watch?v=2MJhDNFT6Lc) where he discusses some examples that start making things click a bit for me, both in terms of

@chrisamaphone this is a scene in disco elysium right

@anuytstt in any case, yeah, I think I agree strongly "the collection of blorks is a blork" is wrong as a general rule, even if I don't know how to generally answer the question "the collection of blorks is a {?}"

@anuytstt ah this is a good and interesting example, thanks, I will have to think about it... Is it also relevant here that Ab is an abelian category, where I am well aware that "abelian category" is defined almost exactly to be "a category having all the nice properties that the category Ab has"?