TITLE: Defining homotopy via the “doubling” endofunctor of a simplicial category
QUESTION [0 upvotes]: I am looking for a reference explicitly defining simplicial homotopy
in terms of endofunctors of $\Delta$, and developing homotopy theory in this terms.
The following is a particular question.
Is it possible to rephrase the following definition of simplicial homotopy in e.g. (8.3.11 of An introduction to homological algebra by C. Weibel)
in terms of endofunctors of $\Delta$ ?

We say $f$ and $g$ are (strictly) simplicial homotopic if if for each
$p\geq 0$, there exists morphisms $$ h_i=h^p_i:X_p\to Y_{p+1} \text{
 for } i=0,\ldots,p $$ such that the following conditions hold.

$$\partial_0 h_0=f_p, \partial_{p+1}h_p=g_p;$$

$$ \partial_ih_j=\begin{cases}h_{j-1}\partial_i & i<j\\ \partial_ih_{i-1} &i=j\\ h_j\partial_{i-1} & i>j+1; \end{cases}$$

$$ s_ih_j=\begin{cases}h_{j+1}\partial_i & i\leq j\\ h_js_{i-1} & i>j. \end{cases} $$

One way to try to do it is as follows.
Let $[\times 2]:\Delta\to\Delta$ denote the endomorphism "doubling" each linear order:
$$[0\le 1\le \dotsb \le n] \longmapsto [0 \le 0' \le 1 \le 1'\le \dotsb \le n \le n'] $$
$$ f:[0\le 1\le \dotsb \le n]\to [0\le 1\le \dotsb \le m] \,\longmapsto\, f':[0 \le 0' \le 1 \le 1'\le \dotsb \le n \le n'] \to [0 \le 0' \le 1 \le 1'\le \dotsb \le m \le m']$$
$$
f'(i)=f(i), f'(i')=f(i)' \forall 0\leq i\leq n.$$
If I understand correctly the answer by Dmitri Pavlov, a standard argument gives that $Y_\bullet[\times 2]$ is a path object:
$$Y_\bullet\xrightarrow{w_\bullet} Y_\bullet[\times 2]\xrightarrow{p_\bullet}  Y_\bullet\times Y_\bullet$$
where each $w_n:Y_n \to Y_{2n+1}$  corresponds to the map of preorders
$$[0 \le 0' \le 1 \le 1'\le \dotsb \le n \le n']\to [0  \le 1 \le \dotsb \le n] , i,i'\mapsto i $$
"repeating each coordinate twice",
and the projections $p^\text{even}_\bullet,p^\text{odd}_\bullet:Y_\bullet[\times 2]\to Y_\bullet$ are maps "leaving only even/odd coordinates", i.e. are given by
$p_n^\text{even}: Y_{2n+1}\to Y_n $  corresponding to
$$[0  \le 1 \le \dotsb \le n]\to [0 \le 0' \le 1 \le 1'\le \dotsb \le n \le n'], i\mapsto i$$
and
$p_n^\text{odd}: Y_{2n+1}\to  Y_n $
corresponding to
$$[0  \le 1 \le \dotsb \le n]\to[0 \le 0' \le 1 \le 1'\le \dotsb \le n \le n'], i\mapsto i'$$
Question. Is it true (under some “niceness” assumptions) that in a simplicial category
for $X_\bullet$ connected,
two maps $f_\bullet,g_\bullet:X_\bullet\to Y_\bullet$ are (strictly) homotopic
iff both maps $ X_\bullet\xrightarrow {f_\bullet}  Y_\bullet$ and $ X_\bullet\xrightarrow {g_\bullet}  Y_\bullet$
factor via $Y_\bullet[\times 2]$ as
$$ X_\bullet\xrightarrow {\tilde h_\bullet} Y_\bullet\circ[\times 2] \xrightarrow{p^\text{even}_\bullet}  Y_\bullet$$
$$ X_\bullet\xrightarrow {\tilde h_\bullet} Y_\bullet\circ[\times 2] \xrightarrow{p^\text{odd}_\bullet}  Y_\bullet$$
where  $p^\text{even}_\bullet:X_\bullet\circ[\times 2]\to X_\bullet$ and $p^\text{odd}_\bullet:X_\bullet\circ[\times 2]\to X_\bullet$
are maps induced by “forgetting” the odd/even half of the “doubled” linear order $0\le 1 \le \dotsb \le n \le 0' \le 1'\le \dotsb\le n'$, as above.
This appears to be true if one of the maps is trivial (i.e. is a map to a point), see Defining homotopy via endofunctors of a simplicial category.

REPLY [4 votes]: Once we correct the definition of $[×2]$ to make it a functor (currently it does not preserve identities) by setting $f'=f⊔f$, it is true that the construction described in the main post gives rise to an equivalent notion of homotopy, assuming $Y$ is Kan.
Indeed, $[⨯2]$ is a right Quillen functor from simplicial sets to simplicial sets, with its left adjoint being the unique left Quillen functor that sends $Δ^n$ to $Δ^n\ast Δ^n$, the join of $Δ^n$ with itself.
We also have canonical inclusions given by the adjoints of projection maps in the main post: $X→X\ast X$ can be included as the left or right factor.
The induced natural transformation $X⊔X→X\ast X$ exhibits $X\ast X$ as a (generalized) cylinder object for $X$, where instead of a genuine codiagonal map $X\ast X→X$ we only have a zigzag $X\ast X→Y←X$, where $X→Y$ is a weak equivalence.  But this is sufficient to answer the original question in the affirmative.
Equivalently, $Y[⨯2]$ together with the two natural maps $Y[⨯2]→Y$ is a (generalized) path object.
A bit of elementary model category theory (see the cited articles) then implies that the notion of homotopy induced by this new cylinder (or path) object coincides with the old notion, assuming $Y$ is Kan.


TITLE: Proof convexity of mean absolute error
QUESTION [6 upvotes]: I am given the cost function: mean absolute error
$$ \frac{1}{N} \sum_{n=1}^{N} \big|y_n - f(x) \big|$$
If $f(x)$ is a linear regression: $f(x) = x^Tw$, where $w$ are the parameters of the regression function and $x$ the input, how can I prove that the mean absolute error is convex as a function of the parameters $w$ ?
convexity is defined here: http://mathworld.wolfram.com/ConvexFunction.html

REPLY [2 votes]: I too am in the process of working it out, but here is what I have:
We only need to verify that $g(w)=\lvert{y_n-f(x_n)}\rvert$ is convex, since we know that the sum of convex functions is also a convex function.
The condition for convexity is the following: for $0\leq\lambda\leq1$ a function g is convex iff
$g(\lambda w_1 + (1-\lambda)w_2) \leq \lambda g(w_1)+(1-\lambda)g(w_2)$
So we have for our function $g(w)=\lvert{y_n-x_n^{T}w}\rvert$,
$\lvert y_n-x_n^{T}(\lambda w_1 + (1-\lambda)w_2)\rvert \leq \lambda \lvert{y_n-x_n^{T}w_1}\rvert + (1-\lambda)\lvert{y_n-x_n^{T}w_2}\rvert$
Since $0\leq\lambda\leq1$, I can put the $\lambda$ and $(1-\lambda)$ inside the absolute value, since these are positive and therefore won't make a difference to the equation.
$\lvert y_n-x_n^{T}(\lambda w_1 + (1-\lambda)w_2)\rvert \leq  \lvert{\lambda y_n -\lambda x_n^{T}w_1}\rvert + \lvert{(1-\lambda)y_n- (1-\lambda)x_n^{T}w_2}\rvert$
This looks familiar, since I can see that if I take the right hand side of my inequality and denote the insides of the absolute values by $a$ and $b$
$a = {\lambda y_n -\lambda x_n^{T}w_1}$
$b = {(1-\lambda)y_n- (1-\lambda)x_n^{T}w_2}$
And the inside of the absolute value on the left side of my inquality is:
$a+b = y_n-x_n^{T}(\lambda w_1 + (1-\lambda)w_2)$
Then I see that my inequality is actually
$\lvert a+b \rvert \leq \lvert a \rvert + \lvert b \rvert $, which is true. Therefore $g(w)$ is convex and $MAE(w)$ is convex.


TITLE: How does one translate Lean to Coq (and visa versa)?
QUESTION [0 upvotes]: I am interested in translated Lean to Coq and visa versa. One first reason is because I want to translate the miniF2F data set in Lean to Coq but lack the expertise to do it. Though in general I'd like to translate as many theorem/lemma statements (and proofs if possible) in each others language. How does one do this? Are there tools that do this?
One crazy idea I thought was to translate lean statements to SMT format then to Coq -- since hammers often try to translate back their proofs to the proof assistants language. Other more crazy ideas could be using LLMs & perhaps prompting them with example translations.
Any other ideas are welcomed!

REPLY [2 votes]: First, I think you mean translate from idiomatic Lean to idiomatic Coq.  Automatic translations (or transpilations) of code are notorious for being non-idiomatic, and addressing this is certainly an area of academic research.
Second, since you are talking about mini-F2F, I think you are only interested in translating statements, not proofs.  That would certainly be easier than translating proofs idiomatically.
It is pretty clear why this would be a challenge when translating from Lean to Coq.  Imagine you have a theorem that you as a human are trying to translate.  That theorem uses definitions, say the real numbers and some basic operators on the real numbers.  One would have to either automatically redefine the Lean definition of the real numbers into Coq, leading to a less useful (and less idiomatic) translation, or maintain an alignment dictionary between Lean and Coq.  This later approach is called concept alignment and can get tricky fast, but is likely reasonable for simple definitions.
If you are interested in translating proofs (which you are not, but I'll mention anyway), that gets even more tricky.  The library of facts and the library of tactics could be very different at points.  This would make it very difficult to automatically get an idiomatic and maintainable proof in the target language (without machine learning).  If you don't care about idiomatic proofs, you could transpile the raw kernel proof if the logics are similar enough (or the source logic can be encoded in the target logic), but remember if you care about idiomatic translations of statements where concepts are aligned and you are using the target definition of the concept, then you can't take a Lean proof about the Lean real numbers and expect to automatically get a Coq proof about the Coq real numbers without doing the hard work of showing that the Lean and Coq real numbers (as well as every operator you use in your theorem statement) are isomorphic.  This was the challenge that Mario Carnerio had when translating Metamath into Lean.  He took the time to map how the Metamath natural numbers and some basic functions and relations on the natural numbers are isomorphic.  This allowed him to translate the Metamath proof of Dirichlet's theorem into Lean (again, not an idiomatic proof and it was never put into Lean' library).  However, he didn't take the time to do the same for Metamath's prime number theorem proof.
Practically, you could try the tools mentioned in the comments.  I think the Coq-Lean-Import is just for kernel level translation and doesn't have concept alignment so it is likely not helpful to you.  Dedukti has a concept alignment project called Logipedia.  You might want to give it a try.  I have no idea if it would be good enough for your purposes, and if the statements would come out looking idiomatic or computer generated.
Also, you mention large pre-trained language models like OpenAI's Codex.  A year ago, this would have sounded futuristic, but this year, they are really starting to show promise.  The way they work, is that you give Codex a few (maybe 6) examples of the translation you are trying to do, and then feed it the Lean example you want to translate to Coq.  I think it would actually do fairly well on mini-F2F.  Here is a paper on this, and here is a github repo doing this for human to Lean translation.  Of course, there are no guarantees on your translation accuracy.
But honestly, my understanding is that the largest barrier to translating mini-F2F from Lean to Coq is not the amount of work.  The mini-F2F people told me it would only take a week for an expert in Coq.  The problem I think is there is a lot of uncertainty on how to translate mini-F2F into Coq idiomatically.  Coq, unlike Lean, has many libraries of mathematics and it isn't clear which should be used (or maybe even which definition of the reals should be used).  These are not things that any automated system can answer.  Once these decisions are made, then one can start to automate the translation (or teach someone like your self or an AI how to translate those statement), but not until.  I assume decisions like this are usually at the forefront of every translation project and add to the complexity of the project.


TITLE: What are the projective submodules of $\Bbb Z/n\Bbb Z$ as a module over itself?
QUESTION [5 upvotes]: Let $R$ be the ring $\mathbb{Z}/n\mathbb{Z}$ with $n \in \mathbb{N}$ composite and consider $R$ as a right module over itself.
I'd like to determine the projective submodules of $R$ if there are any.
First $R$ is free over itself, $\{1+n\mathbb{Z}\}$ being a base.
Now as an additive group $R$ is the direct product of its Sylow subgroups.
My doubts begin here: is it correct to infer that as a right $R$-module $R$ is the direct sum of its Sylow subgroups seen as right $R$-submodules?
If it were so then each Sylow subgroup is a projective $R$-submodule being a direct addend of a free $R$-module.
Clearly none of the former is free since it contains torsion elements.
Next question is: is there any other projective submodule?
If the answer is no then I just proved that the ring $\mathbb{Z}/n\mathbb{Z}$ is hereditary if and only if $n$ is square-free, right?
Any suggestion or critique is widely appreciated.

REPLY [0 votes]: Modules over $R=\mathbb{Z}/n\mathbb{Z}$ are exactly the same as modules over $\mathbb{Z}$ on which $n$ acts trivially. So an abelian group on which $n$ acts trivially splits as a direct sum of abelian groups if and only if it splits as a direct sum of $R$-modules.


TITLE: Probability for a survey.
QUESTION [1 upvotes]: A major coca company sponsors a national taste test, in which subjects sample its cola as well as the best-selling brand. Neither is identified by brand, they're asked to choose which one tastes better. We survey 25 people, who have no preference, and arbitrarily choose one of the colas. Find the probability that 15 or more choose the cola from the sponsor company.
My attempt:
mean = n*p= (25)(.5)=12.5
standard deviation = $\sqrt{n*p*q} = \sqrt{25*.5*.5} = \sqrt {6.25} = 2.5$
z= (15-12.5)/2.5= 1
Prob(x>15) = $1-\int^1_{-\infty} \frac{1}{\sqrt{2\pi}}e^{-.5x^2} dx = .1586 $
But these are none of the answer choices available, so I guess I did something wrong. Any help is appreciated!
Answers choices that are given are: .0983, .2830, .1847, .3731, .2119

REPLY [1 votes]: $X$ is a discrete variable. Therefore $P(X\geq 15)=1-P(X\leq 14)$
You want to apply the central limit theorem. With the continuity correction factor ($+0.5$) the equation is
$$P(X\geq 15)\approx 1-\Phi\left( \frac{14+0.5-12.5}{2.5} \right)=1-\Phi(0.8)$$
Note that this is an approximation.
Using integral representation it becomes
$$P(X\geq 15)\approx 1-\int^{0.8}_{-\infty} \frac{1}{\sqrt{2\pi}}e^{-0.5\cdot x^2} dx$$


TITLE: Product measure: How does this fit together?
QUESTION [2 upvotes]: I am a bit confused.
Consider $(\left\{0,1,2\right\}^{\mathbb{Z}},\mathcal{B},P)$, where $\mathcal{B}$ is the Borel-$\sigma$-Algebra generated by the cylinder sets of the form
$$
\text{cyl}(y_{i}^{i+n})=\left\{x\in\left\{0,1,2\right\}^{\mathbb{Z}}: x_i=y_i,x_{i+1}=y_{i+1},\ldots,x_{i+n}=y_{i+n}\right\},
$$
and $P$ is a product measure on $\mathcal{B}$, such that
$$
P(\text{cyl}(y_i^{i+n}))=\prod_{k=i}^{i+n}p(y_k), \text{ where} \sum_{k=0}^2 p(k)=1.
$$

Now there is the expression
$P\left\{x(0)=1\right\}$.
I do not see how that fits! Because $P$ is a product measure, how can it measure an event like $\left\{x(0)=1\right\}$? Is this event in $\mathcal{B}$?

REPLY [1 votes]: The event $x(0)=1$ is a cylinder set. Let $y_k=1$ for all $k\in\Bbb Z$; then the event in question is $\operatorname{cyl}(y_0^0)$.