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(😄)