Power Objects $PX$ are Injective

Proposition

Let $\mathcal{E}$ be a topos and $X \in \mathcal{E}$ an object. If $PX$ is a power object of $X$, then $PX$ is injective.

Proof

By definition of power object, we have $\text{Hom}_{\mathcal{E}}(X \times Y, \Omega) \simeq \text{Hom}_{\mathcal{E}}(X\times Z, \Omega)$ where the isomorphism is in $\textbf{Set}$ (homsets are <i>sets</i>!), for any $X,Y,Z \in \mathcal{E}$.  

Take 

Comments

Post a Comment

Popular posts from this blog

90% visual proof of Contravariant Yoneda Lemma

By the fact that $\alpha_X : \text{Hom}_C(X,X) \to AX$ we have that $\alpha_X(\text{id}_X) =: u \in AX$ and we're done with mapping any natural map $\alpha : \text{Hom}_C(\cdot, Y) \to A$ to an element $u \in AX$. The sides of the triangular prism in the bottom diagram need to commute for each $f:Y\to X, g : Z \to Y$ in $C$. For one, the triangular endcaps must commute because $A, \text{Hom}_C(\cdot, X)$ are both contravariant functors. Next, the three square sides commute by naturality. We must then have that any time $\alpha_Y(f) = A(f)\circ u$, the diagram commutes.
Read more

Elementary counting formula for the number of $2k$-separated prime pair averages in an interval.

Proof of 2k-separated prime pairs in an interval, counting formula Let all intervals be of integers. Fix a natural number k ≥ 1 k \geq 1 k ≥ 1 . Primorial p n # p_n\# p n ​ # is defined as usual to be p 1 p 2 ⋯ p n p_1 p_2 \cdots p_n p 1 ​ p 2 ​ ⋯ p n ​ . Let an undeclared p p p or q q q just mean any prime number. Lemma 1. The number of x ∈ [ 0 , y ] x \in [0,y] x ∈ [ 0 , y ] such that x 2 = k 2 ( m o d p i ) x^2 = k^2 \pmod {p_i} x 2 = k 2 ( mod p i ​ ) for no i = 1.. n i = 1..n i = 1.. n is given by: f ( y ) = ∑ d ∣ p n # ,   d ≤ y ( − 1 ) ω ( d ) ∑ c ∣ d ,   gcd ⁡ ( c , 2 k ) = 1 ⌊ y − ( z c , d ) ( d ) d ⌋ (0) f(y) = \sum_{d \mid p_n\#, \ \\ d \leq y } (-1)^{\omega(d)}\sum_{c \mid d, \ \\ \gcd(c,2k) = 1} \lfloor \dfrac{y - (z_{c,d})_{(d)}}{d}\rfloor \tag{0} f ( y ) = d ∣ p n ​ # ,   d ≤ y ∑ ​ ( − 1 ) ω ( d ) c ∣ d ,   g c d ( c , 2 k ) = 1 ∑ ​ ⌊ d y − ( z c , d ​ ) ( d ) ​ ​ ⌋ ( 0 ) Where ( z c , d ) ( d ) (z_{c,d})_{(d)} ( z ...
Read more

I wrote a KaTeX (essentially "MathJax") parser in Python/Lark

I wrote a Lark EBNF grammar (Python) that is fed to Lark which generates a parser that can parse a huge subset of KaTeX if anyone is interested. This means you can do various things with the resulting parse tree, like: 1. LaTeX-based calculators. 2. Parsing LaTeX to CAS's. 3. A LaTeX-based proof assistant. 4. Standardizing KaTeX formulas so that say \mathscr{A}_1'' is the same thing as \mathscr{A}''_1 (because they appear 100% the same to the user when rendered, so that is important). 5. Extracting your custom definition of variable from KaTeX (and/or MathJax - same difference here) formulas. 6. Converting the parse tree to a Regex so that you can match similar formulas up to variable-substitution. 7. Scraping http://math.stackexchange.com for some killer math app you're working on. And so on... The grammar is huge. Though it can easily be extended should your users request other currently unsupported operators. You may license it ($), and receive some...
Read more