π¬ Smallproofs
β f : A βΆ B
e m
β A βΆ I βΆ B
f = m β e
π
structure Factorization (A B : Type) :=
(I : Type)
(e : A β I) -- epi
(m : I β B) -- mono
(f : A β B := m β e)
Factor to basic building blocks (irreducibles), then simplify via a universal arrow.
I am learning about factorisation #
because I noticed I still don't really know what to do with simple calculus equations when I see something to factorise I might not yet know why or how to do it
so I found interesting stuff, for example these factorisation exercises can be designed, with tweakable components,
there is also seem to be abstract foundational meaning to them,
for example maybe f = m β e
, where an expression is sent to it's prime factors by e
, and maybe a universal arrow is found via m
. Which stand for epi and monic arrows, so this perhaps has to do with injectivity and surjectivity.
I'm making my own ferment jars π₯¬π₯π§ πΏ #
and I am surprised how easy it is, and how beautiful and fun it is to ferment stuff
I blend/ground veggies and herbs with water, and add about a teaspoon of salt to each jarful. Then I pour the mix into jars and leave the jars indoors or outdoors with the lid left loosely on top.
- Previous: fragments 2025-06-29
- Next: π§ mindful(t), entries in logic