A Universe of Sorts

§ Siddharth Bhat

  1. Ordinals and cardinals
  2. Musing about Specht modules
  3. Every continuous function on [a,b][a, b] attains a maximum
  4. Invisible cities
  5. Associativity of addition in cubicaltt
  6. Etymology of fiber bundle F→E→BF \rightarrow E \rightarrow B
  7. Galois correspondence, functorially
  8. CubicalTT: sharpening thinking about indexed functions
  9. Functors to motivate adjuntions
  10. Madoka Magica: plot thoughts
  11. Chain rule functorially
  12. Lagrange multipliers by algebra
  13. Specht module construction
  14. Even and odd functions through representation theory
  15. Greg egan: Orthogonal
  16. Simplicial approximation: maps can be approximated by simplicial maps (TODO)
  17. Excision (TODO)
  18. Marshall: Andrej (TODO)
  19. Limit is right adjoint to diagonal
  20. Working out why right adjoints preserve limits.
  21. Limit/Colimit/Cone/Cocone: the arrows are consistent!
  22. Representable Functors
  23. Why terminal object is a limit
  24. Excluded middle is not false in intuitionistic logic
  25. Yoneda Lemma and embedding
  26. GHCID
  27. Character theory
  28. Cofibration
  29. Emily Riehl Contrability as uniqueness
  30. Cofactor as derivative of determinant
  31. Homology, the big picture
  32. Normaliztion by evaluation (TODO)
  33. Legal Systems very different from ours
  34. Lefschetz fixed point theorem (TODO)
  35. Shrinking wedge of circles / Hawaiian earring (TODO)
  36. Simplicial approxmation of maps (TODO)
  37. Lebesgue number lemma (TODO)
  38. Big list of learning Lean internals
  39. MicroUI
  40. Proof of tree having (V-1) edges
  41. Creating PDFs to read code
  42. Bias and gain
  43. Barycentric subdivision: edge length decreases
  44. Homotopic maps produce same singular homology: Intuition
  45. Singular homology: induced homomorphism
  46. Demoscene tools
  47. Binaural Beat
  48. Low pass filter by delaying
  49. Octaves are double frequency apart (TODO)
  50. Bias and gain
  51. Show, don't tell
  52. Try and think of natural transformations as intertwinings
  53. Subobject classifier measures how much we need to pay to access fact
  54. Spectral norm of Hermitian matrix equals largest eigenvalue (TODO)
  55. Penrose cohomology [TODO]
  56. Bicycle wheel proof of Gauss Bonnet (TODO)
  57. What is Levi Cevita trying to describe (TODO)
  58. Torsion as giving monodromy of path lifts (TODO)
  59. Cartan's spiral staircase (TODO)
  60. Dupin indicatrix (TODO)
  61. Rodrigues curvature formula (TODO)
  62. Weingarten map (TODO)
  63. When maps cannot be lifted to the universal cover
  64. Nets from Munkres (TODO)
  65. Limit point compactness from Munkres
  66. Proof of Heine Borel from Munkres (compact iff closed, bounded)
  67. Alexandrov topology
  68. Zeroth singular homology group: Intuition
  69. Examples of fiber products / pullbacks
  70. Covariant derivative
  71. Clackety sounds: bucklespring
  72. Submersions and immersions
  73. Ehrsmann connection
  74. Quotes from the culture
  75. Lie bracket commutator from exponentiation (TODO)
  76. Thoughts on proof of fundamental group of unit circle
  77. Pasting lemma
  78. Tensoring with base ring has no effect
  79. Seeing the semidirect product of the dihedral group.
  80. Animating rotations with quaternion curves
  81. Mnemonic for hom-tensor and left-right adjoints
  82. Construction of tensor product: Atiyah macdonald
  83. Recovering topology from sheaf of functions: Proof from Atiyah Macdonald
  84. Urhyson's lemma
  85. Compact Hausdorff spaces are normal
  86. Stone representation theorem: Proof from Atiyah Macdonald
  87. Covariant Hom is left exact
  88. Internal versus External semidirect products
  89. Splitting of semidirect products in terms of projections
  90. Tensor is right exact
  91. Semidirect product as commuting conditions
  92. Exact sequences for semidirect products; fiber bundles
  93. Semidirect product is equivalent to splitting of exact sequence
  94. Intro to topological quantum field theory
  95. Non examples of algebraic varieties
  96. Nilradical is intersection of all prime ideals
  97. Exactness of modules is local
  98. Quotient by maximal ideal gives a field
  99. Ring of power series with infinite positive and negative terms
  100. Mean value theorem and Taylor's theorem. (TODO)
  101. Cayley Hamilton
  102. Nakayama's lemma
  103. Vector fields over the 2 sphere
  104. Learning to talk with your hands
  105. Lovecraftisms
  106. Hairy ball theorem from Sperner's Lemma (TODO)
  107. CS and type theory: Talks by vovodesky
  108. Hilbert basis theorem for polynomial rings over fields (TODO)
  109. Covering spaces
  110. Wedge Sum and Smash Product
  111. Quotient topology
  112. CW Complexes and HEP
  113. Stable homotopy theory
  114. Simply connected spaces
  115. Finitely generated as vector space v/s algebra:
  116. Weak and Strong Nullstllensatz
  117. Screen recording for kakoune pull request
  118. Intuition for why finitely presented abelian groups are isomorphic to product of cyclics
  119. Euler characteristic of sphere
  120. John Conway: The symmetries of things
  121. Semidirect product mnemonic
  122. Non orthogonal projections
  123. Why did maxwell choose his EM wave to be light?
  124. Fast string concatenation in python3
  125. Split infinitive
  126. Yoneda from string concatenation
  127. Right Kan extensions as extending the domain of a functor
  128. Non standard inner products and unitarity of representations
  129. take at most 4 letters from 15 letters.
  130. Flat functions
  131. Hopf Algebras and combinatorics
  132. Butcher group
  133. Neovim frontends
  134. A semidirect product worked on in great detail
  135. Direct and Inverse limits
  136. LEAN 4 overfrom from LEAN together 2021
  137. BLM master thesis
  138. Hololive subculture
  139. RSK correspondence for permutations
  140. Djikstra's using a segtree
  141. Markov and chebyshev from a measure theoretic lens
  142. Among any 51 integers, that are 2 with squares having equal value modulo 100
  143. 1n+2n+⋯+(n−1)n1^n + 2^n + \dots + (n-1)^n is divisible by nn for odd nn
  144. 103n+110^{3n+1} cannot be written as sum of two cubes
  145. Coq-club: the meaning of a specification
  146. SQLite opening
  147. Old school fonts
  148. Stalking syzigies on hackernews
  149. Conditional probability is neither causal nor temporal
  150. Hook length formula
  151. The tyranny of light
  152. Muirhead's inequality
  153. Rearrangement inequality
  154. Triangle inequality
  155. The Heather subculture
  156. Frobenius Kernel
  157. Galois theory by "Abel's theorem in problems and solutions"
  158. Galois theory perspective of the quadratic equation
  159. Burnside lemma by representation theory.
  160. Contributing to SAGEmath
  161. Shadow puppet analogy for entanglement
  162. Books for contest math
  163. Analysing simple games
  164. Linear algebraic proof of the handshaking lemma
  165. Historical contemporaries
  166. Rota's twelvefold way
  167. Counting necklackes with unique elements
  168. Decomposition of projective space
  169. Childhood: Playing pokemon gold in japanese
  170. Tensor is a thing that transforms like a tensor
  171. Tensor Hom adjunction
  172. Schur's lemma
  173. Daughters of destiny
  174. Stuff I learnt in 2020
  175. Line bundles, a high level view as I understand them today
  176. Conversations with a wood carver
  177. Discrete Riemann Roch
  178. Conversation with Olaf Klinke
  179. Topological groups and languages
  180. The mnemonica stack (TODO)
  181. Conversation with Alok about how I read
  182. KMP (Knuth, Morris, Pratt) (TODO)
  183. Reading C declarations
  184. Make mnemonics
  185. Vandermonde and FFT
  186. Thoughts on blitz chess: 950 ELO
  187. Periodic tables and make illegal states unrepresentable
  188. Big list of questions on the structure of graphs
  189. Combinations notation in bijective combinatorics
  190. Arguments for little endian
  191. Expectiles
  192. Depth first search through linear algebra (TODO)
  193. 2-SAT
  194. Longest increasing subsequence, step by step (TODO)
  195. On reading how to rule (TODO)
  196. Strongly Connected Components via Kosaraju's algorithm
  197. Articulation points
  198. Disjoint set union
  199. Making GDB usable
  200. Bouncing light clock is an hourglass
  201. Euler tours
  202. Representation theory of the symmetric group (TODO)
  203. Maximum matchings in bipartite graphs
  204. p-adics, 2's complement, intuition for bit fiddling
  205. Diameter of a tree
  206. Catalan numbers as popular candidate votes (TODO)
  207. The chromatic polynomial (TODO)
  208. Structure theory of finite endo-functions
  209. Number of paths in a DAG
  210. Set partitions
  211. Integer partitions: Recurrence
  212. Stars and bars by direct bijection
  213. DFS and topological sorting
  214. Tournaments
  215. Matching problems (TODO)
  216. Four fundamental subspaces
  217. WHO list of essential medicines (TODO)
  218. why is int i = i allowed in C++?
  219. Kakoune cheatsheet
  220. Assembly IDE
  221. Cohomology is like holism
  222. Flows (TODO)
  223. Amortized analysis
  224. Shelly Kegan: death --- Suicide and rationality (TODO)
  225. Sam harris and jordan peterson: Vancouver 1 (TODO)
  226. Correctness of binary search
  227. readlink -f to access file path
  228. rank/select as compress/decompress
  229. Remembering Eulerian and Hamiltonian cycles
  230. Nice way to loop over an array in reverse
  231. Dynamic Programming: Erik Demaine's lectures
  232. Accuracy vs precision
  233. Why is the gradient covariant?
  234. Politicization of science
  235. Multi ꙮ cular O: ꙮ / Eye of cthulu
  236. You can't measure the one way speed of light
  237. Show me the hand strategy
  238. Words that can be distinguished from letters if we know the sign of the permutation
  239. Easy times don't create weak people, they just allow weak people to survive.
  240. Multiplicative weights algorithm (TODO)
  241. How to fairly compare groups
  242. Z algorithm (TODO)
  243. Bijection from (0, 1) to [0, 1]
  244. Rene Girard
  245. Noam Chomsky on anarchism (TODO)
  246. Slavoj Zizek: Violence
  247. Poverty: Who's to blame?
  248. Learn Zig in Y minutes
  249. The algebraic structure of the 'nearest smaller number' question
  250. Why loss of information is terrifying: Checking that a context-free language is regular is undecidable
  251. Sciences of the artificial
  252. Numbering nodes in a tree
  253. Number of vertices in a rooted tree
  254. Median minimizes L1 norm
  255. LISP quine
  256. A slew of order theoretic and graph theoretic results
  257. Thebes
  258. Beethoven
  259. Neko to follow your cursor around
  260. Non commuting observables: Light polarization
  261. Statement expressions and other GCC C extensions
  262. A quick look at impredicativity
  263. Data oriented programming in C++
  264. Retro glitch
  265. SSA as linear typed language
  266. Nix weirdness on small machines
  267. Autodiff over derivative of integrals
  268. Proof of projective duality
  269. Preventing the collapse of civilization
  270. Violent deaths in ancient societies (TODO)
  271. An elementary example of a thing that is not a vector
  272. Elementary probability theory (TODO)
  273. The handshaking lemma
  274. Git for pure mathematicians
  275. Mutorch
  276. Computing the smith normal form
  277. Laziness for C programmers
  278. Exact sequence of pointed sets
  279. What is a syzygy?
  280. Under the spell of Leibniz's dream
  281. Normal operators: Decomposition into Hermitian operators
  282. Readable pointers
  283. The grassmanian, handwavily
  284. Lie bracket as linearization of conjugation
  285. Computational Origami
  286. Katex in duktape
  287. Kebab case
  288. Localization: Introducing epsilons (TODO)
  289. NaN punning: Storing integers in doubles in JavaScript
  290. Offline Documentation
  291. Using Gurobi
  292. osqp: convex optimizer in 6000 LoC
  293. stars and bars by generating functions
  294. This is not a place of honor
  295. Topological proof of infinitude of primes
  296. Burnside Theorem
  297. The Ise Grand shrine
  298. Edward Kmett's list of useful math
  299. Cokernel is not sheafy
  300. Von neumann: foundations of QM
  301. Discrete schild's ladder
  302. Derivative of step is dirac delta
  303. Extended euclidian algorithm
  304. In a PID, all prime ideals are maximal, geometrically
  305. Prime numbers as maximal among principal ideals
  306. Axiom of Choice and Zorn's Lemma
  307. Local ring in terms of invertibility
  308. Nullstellensatz for schemes
  309. Perspectives on Yoneda
  310. Germs, Stalks, Sheaves of differentiable functions
  311. Connectedness in terms of continuity
  312. Intuition for limits in category theory
  313. Finite topologies and DFS numbering
  314. Categorical definition of products in painful detail
  315. Why is the spectrum of a ring called so?
  316. Ergo proxy
  317. Satisfied and frustrated equations
  318. Combinatorial intuition for Fermat's little theorem
  319. An incorrect derivation of special relativity in 1D
  320. The geometry and dynamics of magnetic monopoles
  321. Sanskrit and Sumerian
  322. Writing Cuneiform
  323. The code of hammurabi
  324. The implicit and inverse function theorem
  325. Whalesong hyperbolic space in detail
  326. Motivating Djikstra's
  327. Intuitions for hyperbolic space
  328. Product of compact spaces in compact
  329. Hyperbolic groups have solvable word problem
  330. Elementary uses of Sheaves in complex analysis
  331. Snake lemma
  332. Kernel, cokernel, image
  333. The commutator subgroup
  334. Simplicity of A5 using PSL(2, 5)
  335. A5 is not solvable
  336. Complex orthogonality in terms of projective geometry
  337. Arithmetic sequences, number of integers in a closed interval
  338. The arg function, continuity, orientation
  339. Odd partitions, unique partitions
  340. Continued fractions, mobius transformations
  341. Permutations-and-lyndon-factorization
  342. Graphs are preorders
  343. Crash course on DCPO: formalizing lambda calculus
  344. Parallelisable version of maximum sum subarray
  345. Thoughts on implicit heaps
  346. Discriminant and Resultant
  347. Polynomial root finding using QR decomposition
  348. A hacker's guide to numerical analysis
  349. Mobius inversion on Incidence Algebras
  350. Finite differences and Umbral calculus
  351. Permutahedron
  352. Lyndon + Christoffel = Convex Hull
  353. Geometric proof of e^x >= 1+x, e^(-x) >= 1-x
  354. Ranking and Sorting
  355. Proof of minkowski convex body theorem
  356. Burrows Wheeler
  357. Intuitionstic logic as a Heytig algebra
  358. Edit distance
  359. Evolution of bee colonies (TODO)
  360. Best practices for array indexing
  361. Algebraic structure for vector clocks
  362. Networks are now faster than disks
  363. Einstein-de Haas effect
  364. Rank-select as adjunction
  365. Bounding chains: uniformly sample colorings
  366. Coupling from the past
  367. Word problems in Russia and America
  368. Encoding mathematical hieararchies
  369. Learning code by hearing it
  370. Your arm can be a spinor
  371. Self modifying code for function calls: Look ma, I don't need a stack!
  372. Adjunctions as advice
  373. Reversible computation as groups on programs
  374. Blazing fast math rendering on the web
  375. VC dimension
  376. Symplectic version of classical mechanics
  377. Theorems for free
  378. How to reason with half-open intervals
  379. How does one build a fusion bomb?
  380. Christoffel symbols, geometrically
  381. A natural vector space without an explicit basis
  382. Cache oblivious B trees
  383. Krohn-Rhodes decomposition
  384. Proving block matmul using program analysis
  385. Why I like algebra over analysis
  386. using for cleaner function type typedefs
  387. A walkway of lanterns (TODO)
  388. Natural transformations
  389. The hilarious commentary by dinosaure in OCaml git
  390. How to link against MLIR with CMake
  391. Energy as triangulaizing state space
  392. The cutest way to write semidirect products
  393. My Favourite APLisms
  394. Proof of chinese remainder theorem on rings
  395. monic and epic arrows
  396. The geometry of Lagrange multipliers
  397. Efficient tree transformations on GPUs (TODO)
  398. Things I wish I knew when I was learning APL
  399. Every ideal that is maximal wrt. being disjoint from a multiplicative subset is prime
  400. Getting started with APL
  401. SpaceChem was the best compiler I ever used
  402. Mnemonic for Kruskal and Prim
  403. Legendre transform
  404. Cartesian Trees
  405. DFS numbers as a monotone map
  406. Self attention? not really
  407. Coarse structures
  408. Matroids for greedy algorithms (TODO)
  409. Grokking Zariski
  410. My preferred version of quicksort
  411. Geometric proof of Cauchy Schwarz inequality
  412. Dataflow analysis using Grobner basis
  413. Fenwick trees and orbits
  414. Dirichlet inversion
  415. Incunabulum for the 21st century: Making the J interpreter compile in 2020
  416. An example of a sequence whose successive terms get closer together but isn't Cauchy (does not converge)
  417. Krylov subspace method
  418. Good reference to the Rete pattern matching algorithm
  419. Leapfrog Integration
  420. Comparison of forward and reverse mode AD
  421. An invitation to homology and cohomology, Part 1 --- Homology
  422. An invitation to homology and cohomology, Part 2 --- Cohomology
  423. Stuff I learnt in 2019
  424. A motivation for p-adic analysis
  425. Line of investigation to build physical intuition for semidirect products
  426. Topology is really about computation --- part 2
  427. Topology is really about computation --- part 1
  428. PSLQ algorithm: finding integer relations between reals
  429. Geometric characterization of normal subgroups
  430. Handy characterization of adding an element into an ideal, proof that maximal ideal is prime
  431. Radical ideals, nilpotents, and reduced rings
  432. My disenchantment with abstract interpretation
  433. Computing equivalent gate sets using grobner bases
  434. The janus programming language --- Time reversible computation
  435. A = B --- A book about proofs of combinatorial closed forms
  436. Generating k bitsets of a given length n:
  437. Bondi k-calculus
  438. Topology as an object telling us what zero-locus is closed:
  439. Vivado toolchain craziness
  440. What the hell is a Grobner basis? Ideals as rewrite systems
  441. Lie bracket versus torsion
  442. Blog post: Weekend paper replication of STOKE, the stochastic superoptimizer
  443. Collapsing BlockId, Label, Unique:
  444. Spatial partitioning data structures in molecular dynamics
  445. Vector: Arthur Whitney and text editors
  446. Representing CPS in LLVM using the @coro.* intrinsics
  447. Bug in the LLVM code generator: Lowering of MO_Add2 and MO_AddWordC
  448. Discrete random distributions with conditioning in 20 lines of haskell
  449. Everything you know about word2vec is wrong
  450. Hamiltonian monte carlo, leapfrog integrators, and sympletic geometry
  451. Small Haskell MCMC implementation
  452. The smallest implementation of reverse mode AD (autograd) ever:
  453. Timings of passes in GHC, and low hanging fruit in the backend:
  454. Varargs in GHC: T7160.hs
  455. Debugging debug info in GHC
  456. GHC LLVM code generator: Switch to unreachable
  457. Concurrency in Haskell
  458. Handy list of differential geometry definitions
  459. Lazy programs have space leaks, Strict programs have time leaks
  460. Presburger arithmetic can represent the Collatz Conjecture
  461. Using compactness to argue about covers
  462. Japanese Financial Counting system
  463. Stephen wolfram's live stream
  464. Cleave as a word has some of the most irregular inflections
  465. McCune's single axiom for group theory
  466. Word2Vec C code implements gradient descent really weirdly
  467. Arthur Whitney: dense code
  468. How does one work with arrays in a linear language?
  469. Linear optimisation is the same as linear feasibility checking
  470. Quantum computation without complex numbers
  471. Linguistic fun fact: Comparative Illusion
  472. Long-form posts:
  473. Big list of emacs
  474. Big list of Coq
  475. Big list of writing
  476. Big list of Latex
  477. Big list of Architecture
  478. Big list of Recipes
  479. Big list of history
  480. Big list of words
  481. Big list of Music
  482. Big list of Social Science
  483. Big list of clojure
  484. Big list of quotes
  485. Empathy
  486. Big list of Vim
  487. Big list of Chess
  488. Big list of shitposting
  489. Cardistry
  490. Poems to memorize
  491. X86
  492. Big list of writing/paper writing thoughts
  493. Big list of interpersonal thoughts
  494. Big list of common lisp
  495. Big list of Agda
  496. Big list of Hacker news
  497. Big list of speaking / oration