arthur @arthur-i.bsky.social · 05/06/2026Every time I see something along the lines of "The careful reader might notice that ..." I'm just like, wow so what am I then, the dumb stupid IDIOT reader???????? 3143
arthur @arthur-i.bsky.social · 21/02/2026inductive types probably the greatest thing humanity has ever invented apart from sliced bread, or like, the tortured poets department 041
arthur @arthur-i.bsky.social · 20/02/2026I hate finsets!!!!! fuck you finsets!!!!! if you're a finset I hope you die!!!!! - me complaining so I magically get better at them 140
arthur @arthur-i.bsky.social · 27/01/2026sometimes I like looking at the wikipedia page for homotopy groups of spheres to see this absolute monstrosity. makes me sick to my stomach 3110
arthur @arthur-i.bsky.social · 23/01/2026this is killing me lol I didn't expect these underscores to actually work 130
arthur @arthur-i.bsky.social · 19/01/2026one of my dream goals atm is to be able to formalize stuff like heine-borel, or like maybe singular = simplicial homology on my own. I'm probably crazy and this requires a ridiculous amount of work, but like idk I have some inkling of hope and/or delusion that it's possible 120
arthur @arthur-i.bsky.social · 19/01/2026ok this bit was just for fun/practice but holy shit I managed to prove exists_infinite_primes from the bottom up LET'S GOOOOOOOO 120
arthur @arthur-i.bsky.social · 15/01/2026there's this section in the book where it shows you how to define the naturals as an inductive type and it asks you to prove a few properties of add and mul before moving on to the next thing, but then I got sidetracked and now a few days later I've done le_total and lt_trichotomy lmao 140
arthur @arthur-i.bsky.social · 13/01/2026downloading hytale rn and I'm just like, wow this is literally 4x smaller than the entirety of mathlib 240
arthur @arthur-i.bsky.social · 05/01/2026oh my god we're gaming??? I wanted to try to formalize schröder-bernstein myself so I got rid of the proof sketch that they gave in the book. this is so scuffed lol 340
arthur @arthur-i.bsky.social · 25/12/2025how am I just now finding out about the Mathematics in Lean book, this is literally all I wanted like a couple years ago lol I just wasn't looking hard enough apparently 140
arthur @arthur-i.bsky.social · 19/12/2025started doing alex kontorovich's real analysis game recently and these limited tactics and theorems are actually destroying me LOL. it's great practice though 230
arthur @arthur-i.bsky.social · 04/07/2024need to be locked back in to making art so no math for like a week or something 😔 I literally have to stop myself from looking at anything math-related lol it's so dire 130
arthur @arthur-i.bsky.social · 03/07/2024need mathematicians to make CAT real at some point. I've written CAT//Set a few times now and I always feel guilty lol 151
arthur @arthur-i.bsky.social · 02/07/2024I'm very annoyed that I can't just focus on both math and art at the same time lol, like learning about adjoint functors has been very fun and all but I need to be spending my time drawing hot men!!!!! 251
arthur @arthur-i.bsky.social · 01/07/2024why are limits so bad lol, I've been trying to generalize (co)limit functors and finally figured out you can turn colimits into a functor Cat//C -> C, but for limits you have to use something disgusting like (Cat^co//C)^op -> C 🤮 120
arthur @arthur-i.bsky.social · 30/06/2024I'm probably completely overthinking this but anyway, if F : Set -> Ab is free and G : Ab -> Set is forgetful, there's a natural isomorphism Ab(Z,-) -> Set(*,G(-)): 220
arthur @arthur-i.bsky.social · 27/06/2024idk if this is like, a very standard way of doing it, but I just figured out you can very elegantly construct the free functor Set -> Ab as the Yoneda extension of the functor * -> Ab sending the single object to Z, since Psh(*) is isomorphic to Set. I'm so happy about this 130
arthur @arthur-i.bsky.social · 19/06/2024I wish I could get back into cohomology but unfortunately I literally could not care less about cohomology classes 😔 120
arthur @arthur-i.bsky.social · 13/06/2024just learned about the nerve functor....... the nerve and realization adjunction is so fucked up but also kind of one of the most incredible things ever 020
arthur @arthur-i.bsky.social · 11/06/2024love studying category theory without thinking about size issues 😇 (<- just wrote a limit diagram with Cat as one of the objects and foolishly looked up what the category of large categories is called) 020
arthur @arthur-i.bsky.social · 09/06/2024I've been so distracted lately lol I went from "yoneda extensions are insanely cool" to "I need comma categories to make sense formally or I will literally lose sleep over this for the rest of my life" to "oooh subobject classifier shiny" 230
arthur @arthur-i.bsky.social · 07/06/2024just saw the definition of a comma category using a single pullback this is insane wtf, actually gave me goosebumps for a little bit which I did not expect to come from comma categories of all things lol 130
arthur @arthur-i.bsky.social · 03/06/2024ok comma categories have been bothering me a bit I think it's mainly the definition I'm working with, where you define objects to be morphisms and morphisms to be pairs of morphisms that make commuting squares. but my issue is you can have the same pair of morphisms create different squares: 230
arthur @arthur-i.bsky.social · 31/05/2024for some reason I used to silently complain about category theory being aggressively functorial and natural, like the double naturality thing in the yoneda lemma or adjunctions, but I get it now...................... 120
arthur @arthur-i.bsky.social · 30/05/2024still think it's crazy you can get all this intuition and prove all this stuff about presheaves just from the directed graph/simplicial set case, and I still don't even know any other examples 😭 130
arthur @arthur-i.bsky.social · 30/05/2024oh my GOD miraculously against all odds I also managed to prove the co-yoneda lemma today LET'S GOOOOOOOOOO my brain is so fried I need to sleep 140
arthur @arthur-i.bsky.social · 29/05/2024finally proved the yoneda lemma..... took Way longer than it should've but I can now die happy 030
arthur @arthur-i.bsky.social · 29/05/2024just spent my entire day trying to prove this and I'm not even halfway done lmaoooo so far I've managed to construct the functor C^op x Psh(C) -> Set sending (c,F) to Hom(よ(c),F) so that's some good progress, anyway I'm gonna go to bed 120
arthur @arthur-i.bsky.social · 28/05/2024yoneda lemma taking up all of my precious drawing time............. worth it tho 050
arthur @arthur-i.bsky.social · 27/05/2024glad I finally have some good intuition for the yoneda lemma lol, it always bothered me when a text would define what a presheaf is and then immediately jump to yoneda, like why should I care about presheaves what are you even trying to tell me 220
arthur @arthur-i.bsky.social · 27/05/2024ok I didn't actually properly think this through the first time I saw it, I thought it would be similar to products of CW complexes, but here you just get the simplicial structure in the product for free???????? what the FUCK 110
arthur @arthur-i.bsky.social · 25/05/2024spent literal days trying to prove this which might just be a skill issue on my part LMAO, but in my defense I wanted to prove it in a way that felt natural, and even stating it in a way that didn't feel like a hack required me to construct the isomorphism Fun(J, Fun(C, D)) -> Fun(C, Fun(J, D)) 320
arthur @arthur-i.bsky.social · 23/05/2024thought I'd try and prove that Fun(A, Fun(B, C)) and Fun(B, Fun(A, C)) are equivalent categories, because 1) it was relevant and 2) I've never done one before. and the sheer amount of work and data...... like wdym I have to define a natural transformation whose components are natural transformations 120
arthur @arthur-i.bsky.social · 22/05/2024for a while I always thought "natural isomorphisms" were a bit of a hazy concept for no reason like why is this important and why should I care about this, but then recently I realized they're just normal isomorphisms in a functor category and suddenly it just made more sense idk why lol 220
arthur @arthur-i.bsky.social · 19/05/2024oh lol I mean I guess the degenerate simplices are good for maps of simplicial sets if you wanna squish things together, but maybe they're also there to ensure that smaller degenerate simplices don't suddenly give the space unwanted holes? 220
arthur @arthur-i.bsky.social · 19/05/2024wait, are simplicial abelian groups not literally just chain groups connected by face/degeneracy maps? and since we're in Ab that means you can also define the boundary maps using the face maps to get a chain complex 120
