Jons Mostovojs @jonn@social.doma.dev

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

Tech bros: idk, it works on my machine

Added my inks to the print shop! Shipping is free the whole weekend too! https://www.inprnt.com/gallery/allisonchinart/

The New York Times has a profile by Siobhan Roberts on the Online Encyclopedia of Integer Sequences, celebrating its 50th anniversary: https://www.nytimes.com/2023/05/21/science/math-puzzles-integer-sequences.html, https://web.archive.org/web/20230522005810/https://www.nytimes.com/2023/05/21/science/math-puzzles-integer-sequences.html

Worthwhile reminder for all you designer types out there

Cleaning your space is self care, too.

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