Show more


Hey look, an enemy of the people of Canada.

It's a funny way to put it because commies love this term.

Unironically hope that there's a registey of underbeaten (another commie term) red plague sufferers in the West.

PSA, if someone asks you for contact info (e.g. a phone number) of someone you know, the correct response is "I can't give that to you, but I can give them yours".

It's efficient and adds no round-trips, it's privacy friendly, it's non-awkward and it's social engineering resistant. It's a universally good rule.

And the corollary, of course: Don't ask someone for another person's contact info - ask them to pass on yours.

Alt: a small mountain in Sawabian Alps, covered with fog.

Show thread

Everyone: the racist, sexist, violent system has failed us

Tech bros: idk, it works on my machine

I wonder if since I have defederated fuckheads from, if I can still expose russkies to their own history by tagging

Show thread

Odd how Portugal. The Man is a well known band who made it and I was literally listening to them before it was too cool! That said, I am a not a huge fan of their 2017 album. It's a bit boring in places, especially with how it starts. And not in a good a way.

Funny is that the most quintessential old school PTM style songs were the ones that made it, namely "Feel It Still" and "1989".

I can easily imagine these songs on "The Satanic Satanist", which is my favorite album of theirs.

Show thread

Portugal. The Man has an album coming up in June too, I have preordered it and matched the price in donation to Ukrainian Armed Forces.

Show thread

2023 is tasty: russian attacks are choking, the West wakes up and starts to give Ukraine a bit more reasonable amounts of hardware, the Cat Empire seems to be in the process if slowly releasing an album, song by song, and Portugal. The Man has released a pretty good single:

Tomorrow I'm off to Canada (Banff) for a week, to work on cohomology theories in Lean. Adam Topaz is one of the organisers of the conference, and he whetted our appetite earlier this week by writing down the definition of singular homology:

def integral_singular_homology (n : ℕ) : Top.{0} ⥤ Module ℤ :=
Top.to_sSet ⋙ ((simplicial_object.whiskering _ _).obj ( ℤ)) ⋙
algebraic_topology.alternating_face_map_complex _ ⋙ homology_functor _ _ n

In fact this definition has been kicking around for a while -- Brendan Seamas Murphy used it here eight months ago in his proof of the Brouwer fixed point theorem. It's all well and good making enough definitions in category theory to give a cool looking definition of the homology of a topological space; the big testing ground in formalisation is not "can you define the object", it's "can you actually prove some theorems about your definition"? A lousy definition might be unusable in practice. Brendan proved for example here that $H_n(S^n,R)$ was isomorphic to $R$, for $R$ a nonzero commutative ring.

My PhD student Amelia Livingston has done the same thing for group cohomology; her definition has hit Lean's maths library, which means that it will live for as long as Lean lives. It's here . Amelia has further work proving things like Inf-Res, Hilbert 90 and so on, proving that her definition is usable.

After next week it will be interesting to see how much more progress we have made with cohomology theories. Topological K-theory is close, and another target for this week is etale and proetale cohomology of schemes. Wish us luck in the mountains of Canada!

Show more
Doma Social

Mastodon server of