Jons Mostovojs @jonn@social.doma.dev

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 (Module.free ℤ)) ⋙
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 https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/52f48d25068df0eadf3df5b2ede7bcb087d30527/src/brouwer_fixed_point.lean#L274 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 https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/52f48d25068df0eadf3df5b2ede7bcb087d30527/src/homology_of_spheres.lean#L2043-L2045 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 https://leanprover-community.github.io/mathlib_docs/representation_theory/group_cohomology/basic.html . 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!

hey people who use emacs, scheme, GNU things and other tools that are related to terrible people and problematic organisations: How do you go about carving a space for yourself with those tools given the problems associated with senior people in those communities?

I've got my own tactics, but I'm curious to know how you go about it and when you decide it just isn't worth it any more.

Orcas have sunk 3 boats in Europe and appear to be teaching others to do the same.

Scientists think a traumatized orca initiated the assault on boats after a "critical moment of agony" and that the behavior is spreading among the population through social learning.

https://www.livescience.com/animals/orcas/orcas-have-sunk-3-boats-in-europe-and-appear-to-be-teaching-others-to-do-the-same-but-why

I had a dream where I desperately needed to recall the password to my work account at my first computing job, in the 80s, so I could go back and fix some problem there. It was only when I woke that I recalled: that system was set up with NO PASSWORDS and it was never an issue.

bandcamp won their union! bandcamp won their union!!

i'm so fucking happy for them, and also for the possible knock-on effects of some of epic game's holdings unionizing

their full statement - https://blog.bandcamp.com/2023/05/19/bandcamp-and-bandcamp-united-release-joint-statement-on-union-vote/

log(😅) =💧log(😄)

I visited my grandparents a few days ago, and they have to use a nightmarish miasma of websites that have all been mergerered-and-acquisitioned half a dozen times to order their medications. Due to them having memory issues and generally just being frustrated with bullshit that shouldn't be this hard, one of their children had to go through a bunch of hoops to get added onto my grandpa's account so they can just order some of the meds he needs.

All because usernames and passwords were not saved anywhere on their devices.

It was a small thing in the grand scheme, but it sucked seeing him have to give up a piece of his agency and autonomy so that he could get the medication he needs.

KeePassXC is good, but there are others. Just do *something* while you and your elders are still able to learn and get into habits. I really think it will make things a little easier in the future.