TITLE: What is interesting/useful about Castelnuovo-Mumford regularity?
QUESTION [16 upvotes]: What is interesting/useful about Castelnuovo-Mumford regularity?

REPLY [21 votes]: Here's how I think about Castelnuovo-Mumford regularity.  It's an invariant of an ideal (or module or sheaf) which provides a measure of how complicated that ideal (or module or sheaf) is.  This invariant is related to free resolutions, and thus it measures complexity from that perspective.
Why is it interesting?  One answer is that it can be used to provide an effective bound for two famous theorems.  The first theorem I have in mind is that the Hilbert function of a graded ideal (or a finitely generated graded module) over the polynomial ring eventually agrees with the Hilbert polynomial of that ideal (or module).  The second theorem I have in mind is Serre vanishing, which says that, given a coherent sheaf $\mathcal F$ on $\mathbb P^n$, there exists $d$ such that $H^i(\mathbb P^n, \mathcal F(e))=0$ for all $i>0$ and all $e>d$. These two theorems are related: if $M$ is a graded module of depth $> 0$, and $\mathcal F$ is the associated sheaf of $M$, then the Hilbert function of $M$ in degree $e$ equals $H^0(\mathbb P^n,\mathcal F(e))$.
An example where Castelnuovo-Mumford is particularly useful comes from the construction of the Hilbert scheme (I have heard that this is related to Mumford's original use, though I have no reference.)  The basic point is that you can parametrize the set of ideals with a given Hilbert function by considering subloci of certain Grassmanians satisfying determinantal criteria, whereas it's less clear (at least to me) how to parametrize ideals with a given Hilbert polynomial.
Another great example where  Castelnuovo-Mumford is useful is presented in Eisenbud "The Geometry of Syzygies" chapter 4, where he solves the interpolation problem for points in affine space.


text:
\shrink
\section*{Broader Impact}
\label{sec:impact}
\shrink

\Perception plays an essential role in robotics applications ranging from autonomous driving, robotic manipulation, autonomous flight, to robotic search and rescue. Occasional perception failures are almost inevitable while operating in the wild (\eg~due to sensor
malfunction, or incorrect data association resulting from neural networks or hand-crafted feature matching techniques). These failures, if not detected and handled properly, have detrimental effects, especially in safety-critical and high-integrity applications (\eg~they may put passengers at risk in autonomous driving or damage a satellite in space applications). Existing perception algorithms (\eg~fast heuristics) can fail without notice.

On the contrary, the certifiable algorithms presented in this work perform geometric perception with optimality guarantees and act as safeguards to detect perception failures.

The development of certifiable algorithms has the potential to enhance the robustness of perception systems, inform system certification and monitoring, and increase the
trustworthiness of autonomous systems.

On the negative side, the use of certifiable algorithms as an enabler for robots and autonomous systems inherits the shortcomings connected to the misuse of these technologies. The use of autonomous systems in military applications as well as the impact of robotics and automation on the (human) workforce must be carefully pondered to ensure a positive societal impact.

config: arxiv


TITLE: How to show that a discrete valuation ring has only two prime ideals?
QUESTION [5 upvotes]: In the book Algebraic Geometry by Hartshorne, page 74, it is said that the spectrum of a discrete valuation ring $R$ has only two points. How to show that a discrete valuation ring has only two prime ideals? In http://en.wikipedia.org/wiki/Discrete_valuation_ring, it is said that a discrete valuation ring has exactly one non-zero maximal ideal.

REPLY [10 votes]: Here is an argument starting from the definition of a DVR as a ring admitting a discrete valuation:
if $P$ is a non-zero prime ideal, then it contains a non-zero element, which can be written in the form $u t^n$, where $u$ is a unit (i.e. has valuation $0$), and $t$ is a uniformizer (i.e. has valuation $1$).  Then $t^n \in P$ (multiply by $u^{-1}$), and then $t \in P$ (using primality).  Thus the unique non-zero ideal of $R$ is the (maximal) ideal of elements of valuation $\geq 1$.


TITLE: On homomorphisms between vertex transitive graphs
QUESTION [1 upvotes]: In general there is no relation between automorphism groups of subgraphs and the main graph. However, this question is about vertex transitive graphs.
Given vertex transitive $G$ and $H$ such that $|\mathcal{V}(G)|<|\mathcal{V}(H)|$.
If $\mathcal{Aut}(G)\supset\mathcal{Aut}(H)$, is $G\leq H$?
If $G\leq H$, is $\mathcal{Aut}(G)\supset\mathcal{Aut}(H)$?
(I suspect the answer to the second question is no.)
Given vertex transitive $G$ and $H$ such that $|\mathcal{V}(G)|>|\mathcal{V}(H)|$.
If $\mathcal{Aut}(G)\supset\mathcal{Aut}(H)$, is $G\rightarrow H$?
If $G\rightarrow H$, is $\mathcal{Aut}(G)\supset\mathcal{Aut}(H)$?
(Again I suspect the answer to the second question is no.)
$\rightarrow$ implies homomorphism exists in the direction suggested.

REPLY [3 votes]: The answer to the first question is certainly no. The automorphism group of the Petersen graph $H$ is $\mathfrak S_5$ so is equal to the automorphism group of the complete graph $G=K_5$, which has strictly fewer vertices. Both these graphs are vertex transitive and yet the Petersen graph has no $5$-clique, so $G$ is not a subgraph of $H$.
The second question is very strange. I must misunderstand, otherwise the isolated vertex in a non-trivial vertex transitive graph (say a 3-cycle for concreteness) is an immediate counterexample.
The third question also immediately admits a negative answer: take $G$ equal to the Petersen graph again and $H$ equal to 5 isolated vertices.
I don't know about the fourth question, though one can reduce to $H$ being a (connected) core.


TITLE: Determine if an infinite series is con- or divergent
QUESTION [0 upvotes]: Consider the following infinite series:
$$\sum_{n=1}^\infty\frac{(-1)^n}{4n+(-1)^n}$$
I need to determine whether this sum converges or diverges. The root and ration test were inconclusive as I've tried them and by now I could not come up with a suitable comparable sum. My best guess by now is that it diverges.

REPLY [2 votes]: Let,
$ a_n=\frac{1}{4n+(-1)^n}$
Note that sequence $\{a_n\}$ is monotonically decreasing and $a_n \to 0$.
Hence by Leibniz’s test, above series converges.


TITLE: Prove that $\;A\cdot\text{adj}(A + B)\cdot B = B\cdot\text{adj}(A +B)\cdot A$
QUESTION [2 upvotes]: Let $\;A,B\;$ be $\;n\times n\;$ matrices in $F.$
Prove that $\;A\cdot\text{adj}(A + B)\cdot B = B\cdot\text{adj}(A + B)\cdot A$
Hint : Start with the identity $\;C\cdot\text{adj}(C) =\det(C)\cdot I$.
In for $\;C\;$ being an $\;n\times n\;$ matrix in $F.$
I've been able to find that $\;C\cdot\text{adj}(C)=\text{adj}(C)\cdot C=\det(C)\cdot I\;,\;$ but I can't figure out where to go from here because we have $\text{ adj}(A + B)\;$ and not $\text{ adj}(A)\;$ or $\text{ adj}(B)\;.$
Any help would be much appreciated.

REPLY [1 votes]: Let $\;A,B\;$ be $\;n\times n\;$ matrices in $F.$
Prove that $\;A\cdot\text{adj}(A+B)\cdot B=B\cdot\text{adj}(A+B)\cdot A\;.$
Proof :
$\;A\cdot\text{adj}(A+B)\cdot B=$
$=A\cdot\text{adj}(A+B)\cdot\big[(A+B)-A\big]=$
$=A\cdot\text{adj}(A+B)\cdot(A+B)-A\cdot\text{adj}(A+B)\cdot A=$
$=A\cdot\big(\det(A+B)\cdot I\big)-A\cdot\text{adj}(A+B)\cdot A=$
$=\big(\det(A+B)\cdot I\big)\cdot A-A\cdot\text{adj}(A+B)\cdot A=$
$=(A+B)\cdot\text{adj}(A+B)\cdot A-A\cdot\text{adj}(A+B)\cdot A=$
$=\big[(A+B)-A\big]\cdot\text{adj}(A+B)\cdot A=$
$=B\cdot\text{adj}(A+B)\cdot A\;\;,$
hence
$\;A\cdot\text{adj}(A+B)\cdot B=B\cdot\text{adj}(A+B)\cdot A\;.$


text:
\subsection{Proof of the main theorem}\label{c:dowod}

\begin{proof}{(\sc of Theorem \ref{t:main})}
We check that the boundary $\bd{W_N}$ satisfies the conditions from Proposition \ref{f:charmenger}.

\smallskip
\emph{Metrisability, compactness.} See Remark \ref{u:wlbrzeg}\ref{u:wlbrzegzwme}.

\smallskip
\emph{1-dimensionality.} We have the following equality: $\dim\bd{W_N}\!=\!\max\{n\!:\!\widetilde{H}^n(N)\neq0\;\mathrm{or}\;\widetilde{H}^n(N\setminus\Delta)\neq0\;\mathrm{for\;some\;simplex}\,\Delta\!\subseteq\! N\}$ (where $\widetilde{H}^*$ denotes the reduced cohomology), \cite[proof of Lemma 2.5]{Swiat16}.

By the assumption, $\dim\bd{W_N}\leq1$.
If we had $\dim\bd{W_N}=0$, then $W_N$ would be virtually free,  \cite[Corollary 8.5.6]{DavBook08}. On the other hand, since $N$ is inseparable and is not a simplex, $W_N$ is 1-ended, \cite[Lemma 2.3]{Swiat16}, a contradiction.

\smallskip
\emph{Connectedness.} Follows by \cite[Lemma 2.3]{Swiat16}.

\smallskip
\emph{Local connectedness.} This property follows by the argument in the first paragraph of the proof of Lemma 3.1 in \cite{Swiat16}.

\smallskip
\emph{No local cut-points.}
By the assumption, we have that $\bd{W_N}$ has no local cut-points or $N$ is a triangulation of $S^1$ or $W_N$ is a direct sum of a special subgroup $W_K$ with nerve $K$ being a triangulation of $S^1$ and a finite special subgroup $W_L$, \cite[second paragraph of the proof of Lemma 3.1]{Swiat16}.
We will exclude the two latter cases.
If $N$ is a triangulation of $S^1$, by flagness, $|N^{(0)}|\geq4$, so $N$ has a separating pair of non-adjacent vertices.
If $W_N=W_K\oplus W_L$ for some $K,L$ as in the second case, then $|K^{(0)}|\geq 4$, $L$ is a simplex and $N$ is a simplicial join of $K$ and $L$. Therefore $N$ is separated by a suspension of the simplex $L$. Both of these cases contradict inseparability of the nerve $N$.

\smallskip
\emph{No planar open subsets.} By Theorem \ref{t:nieplan} there is an embedding of some non-planar graph $H$ into the boundary $\bd{W_N}$. By \cite[Lemma 7]{KaKl98}, if there were some planar neighbourhood of some point in the boundary $\bd{W_N}$, then the graph $H$ would embed into this neighbourhood.

\end{proof}

\begin{remark}\label{u:mainkonieczne}
\begin{enumerate}[(i)]
	\item By the formula for $\dim\bd{W_N}$ given in the above proof, the condition on cohomology in the assumption of Theorem \ref{t:main} is a necessary condition for the boundary $\bd{W_N}$ to be 1-dimensional.
	\label{u:mainkonieczne1}

	\item The condition that $N$ is inseparable and is not a simplex is necessary for the boundary $\bd{W_N}$ to be connected and have no local cut-points, \cite[Lemma 2.2]{Swiat16}.
	\label{u:mainkonieczne2}

	\item The observations from above two remarks and the proofs of compactness, metrisability, 1-dimensionality and connectedness do not require the assumption that the group $W_N$ is hyperbolic.
	Omitting or weakening of the assumption of hyperbolicity in the other three parts of the proof seems to be a non-trivial task.

	\item The boundary of a Coxeter group having a planar nerve is planar (it does not require hyperbolicity), \cite[Lemma 2.4]{Swiat16}, therefore non-planarity of the nerve $N$ is a necessary condition for the boundary $\bd{W_N}$ to be the Menger curve.
	\label{u:mainkonieczne4}

\end{enumerate}
\end{remark}


TITLE: Possible number of Arrangement of given word with following conditions:
QUESTION [0 upvotes]: so that no two vowel come together.
Repetition of letter is allowed.

For example:
Example 1 : "abe"
Answer : number of arrangements are 2.
1)abe
2)eba
Example 2: "ae"
Answer : 0.
No possible arrangements.
Example 3: "abab"
Answer : 3
1)abab
2)baba
3)abba
I got stuck to generalize the formula for this. Thank you in advance.

REPLY [1 votes]: Instead of the so called subtraction method, use the gap method.
Suppose there are $5$ vowels and $8$ consonants
$- C - C - C - C - C - C - C - C -$
The $5$ vowels can go into any of the $9$ gaps, thus $\binom85$ placements.
If all the letters are distinct, $\binom955!8!$ permutations.
If, say, one vowel is repeated twice, and one consonant thrice, $\binom95\frac{5!8!}{2!3!}$ permutations.
You should now be in a position to derive a generalised formula.
Happy New Year !


TITLE: Expressing a transformation relative to a basis of the domain and the codomain
QUESTION [0 upvotes]: Let the linear transformation from 2-d to 3-d space T defined by T(x,y) = (3x+y,x+y,x+3y).
Determine the matrix representing T relative to the standard basis for the codomain and the basis {(3,1),(4,1)} for the domain.
I am unsure of how to obtain such a matrix. My attempt consists of applying T on the columns of the basis of the domain:
T(3,1)=(10,4,7): first column.
T(4,1)=(13,5,7): second column.
Is this correct?

REPLY [0 votes]: The columns of a transformation matrix are the images of the basis vectors. Your approach is correct. Note that if the basis of the codomain were not the standard basis, you’d have to express the two images in coordinates relative to that basis.


TITLE: Is Hyperbolic Space $H3$ the best representation space for momenta, in momentum-scale invariant theories?
QUESTION [0 upvotes]: The motivation is the following:
For each particle of mass m, we could write :
$- (E/m)^2 + (p_x/m)^2  + (p_y/m)^2 + (p_z/m)^2 = -1$,
which is nothing than a equation for a point in the hyperbolic space $\mathbb H3$, which can be seen, with Poincaré representation (Poincaré ball), as a (full) sphere (with hyperbolic distance)
For photons, we may give us a very tiny mass, so photons could be considered, in the limit where this tiny mass is zero, as living at the boundary of $\mathbb H3$, which is $\mathbb CP1$ (Riemann sphere $S^2$)
With these prescriptions, we cannot distinguish, photons with proportionnal momenta, but if the theory is momentum-scale invariant, it seems OK.
So could we use Hyperbolic Space $H3$ as representation space for momenta, in momentum-scale invariant theories?

REPLY [1 votes]: In English, unlike French, "impulsions" are known as "momenta".
Yes, massive particles' momentum 4-vectors belong to a $H^3$. On the other hand, massless particles' momentum 4-vectors don't belong to a boundary of $H^3$. Instead, they belong to a degenerate, singular version of an $H^3$ which is the same thing as $CP^1$ (semidirectly or fibered) times the scaling $R^+$. This statement means that the overall normalization of the photon's energy or momentum always matters. If two photons are moving in the same direction, to the same point of the $CP^1$, it clearly doesn't mean that they have the same momentum or energy, does it? An X-ray flying from Paris to Lyon is something else than a radio wave photon flying from Paris to Lyon.
In scale-invariant theories, particles have to be massless and physics of particles with one momentum 4-vector and its multiple is "physically equivalent" - related by a symmetry transformation. But it doesn't mean it's the same photon. The photons with differently scaled energies are still different and the ratio of energies of two photons, at least overlapping or nearby ones, may always differ from one and may be determined.


text:
\begin{document}  \date{}
\title{\ksl\ \sul\ : Some Observations}
\author{S.G. Dani}
\maketitle

\begin{abstract}

The \ksl\ \sul\ has been much less studied or discussed from a modern
perspective, even though the first English translation of two {\it
  adhy\=aya}s (chapters) from it, by Thibaut, appeared as far back as
1882. Part of the reason for this seems to be that the general
approach to the \sul\ studies has been focussed on ``the
mathematical knowledge found in them''; as the other earlier \suls,
especially \bsl\ and \asl\ substantially cover the ground in this
respect the other two \suls, \msl\ and \ksl, received much less
attention, the latter especially so.

On the other hand the broader purpose of historical mathematical
studies
extends far beyond cataloguing what was known in various cultures,
rather
to understand the ethos of the respective times from a mathematical
point of view, in their own setting, in order to evolve a more complete
picture of the mathematical developments, ups as well as downs, over
history.

Viewed from this angle, a closer look at \ksl\ \sul\ assumes
significance.
Coming at the tail-end of the \suls\ period, after which the \suls\
tradition died down due to various historical reasons that
are really only partly understood, makes it special in certain ways. What it
omits to mention from the body of knowledge found in the earlier \suls\ would
also be of relevance to analyse in this context, as much as what it
chooses to record. Other aspects such as the difference in language,
style, would also reflect on the context. It is the purpose here to
explore this direction of inquiry.

\end{abstract}

The performance of the {\it yajna}s in the Vedic period involved
construction of altars
({\it vedi}) and fireplaces ({\it citi} or {\it agni}) in a variety of
intricate shapes, such as birds, tortoise and others, of quite large
sizes; the dimensions of the {\it vedi}s often extended to over 100 feet and the {\it agni}s
could be 15 feet and 20 feet, or more, in width and length. This
warranted detailed
description of procedures for their construction, which is the subject
of the \suls, which are parts of the {\it
  Kalpas\u tra}s associated with the {\it yajurveda}. Apart from the
direct aspect of step by step
description in the form of manuals, the \suls\
also include enunciation of various geometric principles involved, thereby
setting up a body of geometric
ideas and framework.

The different {\it \'s\ia kh\ia}s (branches) of the Vedic people had
their respective versions of \sulscu, though, as may be expected, a
degree of intrinsic unity may be seen in their overall contents.
Notwithstanding the fact that there were a large number of  {\it
  \'s\ia kh\ia}s, possibly in hundreds, only eight (or nine?)
\suls\ with mathematical content have been known in our times.
Baudh\a yana, \A pastamba,
M\a nava, Maitr\a yan\i ya, Var\a ha, Saty\a \d s\a \d dha, and V\a
dul associated with the {\it K\d r\d sna yajurveda}, and
a sole \ksl\ \sul\ associated with {\it \'sukla yajurveda} are known.
Of these, \asl,  Var\a ha, and V\a dul\ are literally the same
\cite{Kh}. (???) \msl\
and  Maitr\a yan\i ya are understood to be versions of each other
(though a detailed comparison does not seem to have been made yet).
\bsl, \asl, \msl, and \ksl\ \suls\ are independent in overall
character, even
though, as noted above, there are many commonalities.

The dates of the
\suls ~are uncertain; according to Kashikar, as quoted in \cite{K},
 the following ranges may be associated with the  composition of the
 respective \suls\ :  \bsl\ and V\a dul ~(800~-~500~BCE), \asl~and
~\msl ~(650~-~300~BCE) and \ksl, Saty\a \d s\a \d dha and Var\a ha
~(300~BCE - 400~CE). There have also been other suggestions in this
respect (see \cite{SB} for a discussion on this), placing \bsl\ around
5th or 6th century BCE, \asl\ around 5th
and 4th century BCE, \msl\ between them, and \ksl\ around 350 BCE.
However all dates seem to be quite speculative, and
there do not seem to be dependable inputs on the issue.

The \suls
~are composed in the {\it s\u tra} (aphoristic) style,  mostly
in prose form, though parts of some of \msl\ and \ksl\ \suls\ are
found to be in
verse form.  The texts  have been divided by later
  commentators into convenient segments, treated as individual
{\it s\u tras}, with numbers attached, and grouped into Chapters. As
presented in \cite{SB}
\bsl~ has 21 Chapters adding to 285 s\u tras, \asl ~has 21 Chapters
adding to   202 s\u tras,  \msl ~has
  16 Chapters adding to 228 s\u tras, and  \ksl ~has 6 Chapters adding
  to 67 s\u tras.\footnote{An extra chapter of \ksl\ is found in the
    version given in     \cite{Kh}.}

It is an enigma in the subject that the \bsl\ \sul\ which is the oldest
happens to be the most systematic and comprehensive one in many
ways. While the
others do have some things in addition in certain respects, there are
some crucial things that are omitted, and
one also senses in them a general lack of harmony in the presentation.
It is almost as if the seeds of eventual decline are embedded into the \sul\
literature, though indeed this would be a rather simplistic view to take.

There have been many pre-modern commentaries on the \suls, and they have
proved helpful in understanding the original \suls;
(unfortunately even the dates of the commentaries can not be ascertained).
There are commentaries of Dw\a rak\a n\a tha Yajwa and Venkate\'swara
Dik\'sit  on \bsl, of Kapardisw\a m\i, Karavinda Sw\a m\i\ and
Sundarar\a ja on \asl, and of Karka and Mah\i dhara on \ksl\ (no pre-modern
commentaries are known on \msl\ \sul.)

The \suls\ became part of the modern global scholarship through the works of
European scholars, producing translations and edited versions of them
in European languages. George Thibaut published an English translation
of \bsl\ \sul\
and the commentary of Dw\a rak\a n\a tha Yajwa, in the journal {\it
  Pandit}, published from Benaras, during 1874 - 76. Edmund Burk
brought out a translation of the  \asl\ \sul\ in German in
1901. Translation of
\msl\ \sul\ was produced by J.M. van Gelder in 1964. There have also been
various subsequent studies of these \suls, by western as well as
Indian scholars. An English translation of
all the four \suls, with commentaries,  was brought out by S.N. Sen and
A.K. Bag~\cite{SB} in 1983.

On the whole the \ksl\ \sul\
has been much less studied or discussed in modern
writings, even though the first English translation of two {\it
  adhy\=aya}s (chapters) from it, by Thibaut, appeared as far back as
1882. Part of the reason for this seems to be that the general
approach to the \sul\ studies has been focussed on the
mathematical knowledge from the tradition as a whole; indeed, many
writers do not make adequate distinction between individual \suls\
in the overall discourse. Since the earlier \suls,
especially \bsl\ and \asl\ substantially cover the ground in this
respect the other two \suls, \msl\ and \ksl, received much less
attention, the latter especially so. On the other hand, for a fuller
understanding from a historical point of view it would be important to
study the \suls\ with attention to their individual identities,
comparisons between them etc.

Our aim here will be to discuss the \ksl\ \sul\ in this
overall context, concentrating on its specialities in relation to the
earlier \suls, especially \bsl\ \sul. Special significance is lent to
this by the fact that \ksl\ is from  substantially
later times, towards the fag end of the Vedic period, after which the {\it
  yajna}s lost their sheen, as a historical phenomenon, though some
feeble remnants of the idea are seen
embodied in the later day Hindu ritual practices, including in our
times. We shall however content ourselves with comparisons of the technical
mathematical aspects, with some modest hints of their possible
significance. The differences in various
individual aspects would perhaps have various possible explanations,
or they could even be coincidental. However it seems worthwhile to
``identify'' them so that eventually a more comprehensive picture may
emerge,  throwing light on broader historical issues
relating to the transformation of the \sul\ literature over its
period, and in turn of the Vedic people.

\section{The general features}

One of the most striking distinctive features of the \ksl\ \sul\ is its
rather small size compared to the others (as the alert reader may have
noted from the figures mentioned above in this respect). What is this
economy in aid of?  Broadly speaking the difference in size is
accounted for by the fact that \ksl\ does not go into much detail of
the construction of the individual {\it citi}s, on which \bsl, for
instance, expends considerable amount of space, many chapters in terms
of the later organization of the text. \ksl\ \sul\ is largely focussed on
``theory'', though there are some parts touching upon arrangement of
the {\it vedi}s and specific features of certain {\it citi}s. Why was
such a policy adopted? It would seem that the practice of {\it yajna}s
become too
diffuse for it to be worthwhile to go into the details, and it was
considered best to confine to discussing ``general principles''.
Notwithstanding the small size, one does not find ``stinginess'' in
the discussion of the mathematical parts. In fact in some cases there
is a lingering discourse on what may be considered quite
elementary. An example, though
rather an extreme one, is the part with the s\u tra translated
as ``Square on
a side of 2 units is 4, on 3 units it is 9 and on 4 units it is 16.''
which is then followed by the general statement for integers and then
again separately for select fractions $\frac 12, \frac 13$ and $\frac
14$ for the length of the side.

\section{Presentation of measures}

The \bsl ~\sul~gives at the outset (in s\u tra 1.3, right after two
s\u tras which are in the nature of an ``Abstract'' for what is to
follow) names of
length measures with various magnitudes. There are 18 of them, the
smallest being  {\it tila} (sesame seed) is
$\frac 1{34}$th\footnote{It was postulated by
  Thibaut
(see \cite{T}, page 15) that the unit  owes its origin to the fact
that they had a  formula for $\sqrt 2$ involving the fraction $\frac
1{34}$.}  of an {\it  a\n gula} (finger) and the largest one is {\it
\i \d s\a} (pole) which is 188 {\it a\n gula}s; the commonly occurring
large unit however is {\it puru\d sa} (man),
which is 120 {\it  a\n gula}s.\footnote{
 Many of the intermediate units do not bear
a simple fractional relation with {\it puru\d sa} however; e.g. a {\it
  b\a hu} is 36 {\it a\n gula}s, a {\it yuga} is 86 {\it a\n gula}s,
etc..}   The {\it  a\n gula} measure
was about $\frac 34$th of an inch, or about 1.9 centimetres.
Many of the units occur infrequently, only in the description of
specific {\it vedi}s.

\ksl\ \sul\ involves only 9 units, all from \bsl's list, except that a term
{\it vitasti} is used for a measure of 12 {\it angula}s, which is
{\it pr\a de\'sa} in \bsl, and {\it pada} is also taken to be same
measure (12 {\it angula}s). The units range only between the  {\it
  a\n gula} to  {\it \i \d s\a}, thus excluding in particular the fine unit
measures {\it a\d nu} and {\it tila}; these are also absent in \asl\
and \msl\ \suls.
Unlike in the \bsl\ \sul\ no systematic listing of the units  is found
in \ksl\ \sul. On the face of it
this may suggest a greater standardisation of units over the
period, but on the other hand it could also be because \ksl\ does not
deal with many practical situations as involved in \bsl. The fact that
the small
units do not appear in \ksl, as also in \asl\ and \msl\ \suls,
shows that they were not part of the practical need in
the Vedic practices, and feature in \bsl\ on account of specific
theoretical preoccupations, corroborating Thibaut's hypothesis
connecting {\it tila} to a term in the expression for $\sqrt 2$.
The theoretical inclination seems to have been lost over a period.

\section{Cardinal directions}

Unlike the earlier \suls\ \ksl\ gives explicitly a prescription for
locating and fixing the cardinal directions, over any day. The
east-west line is obtained as the line joining the two points on a
circle drawn around the base of a pole where the shadow of the tip of
the pole falls on the circle in the course of a day. The north-south
line is then obtained  through a process of drawing a perpendicular to the east-west line; the process consisted of
tieing the ends of a rope to two poles along the east-west line,
stretching the rope on either side
of the line by holding it at its midpoint, and then joining the two
points marked by the midpoint on either side.

One may wonder how the cardinal directions were
fixed in the earlier times, especially since from the beginning they
have been very
important to the \'sulva constructions, in terms of the spiritual
motivation, and the description of the constructions has typically
been with reference
to the east-west line. It has been suggested that it was determined by
the shadow of the pole on the equinox day, and verified by the rising
and setting points of the the star K\d rttik\a\
\cite{SB}. Interestingly, even though the method as above is
explained at the outset of \ksl\ \sul, in Chapter 7 of it there is a
verse (Chapter VII, verse 35) about determining the East as
the direction of
rising of the stars {\it K\d rttik\a, \'Srava\d na} or {\it Pu\d sya}
or as the midway of the directions of
rising of {\it Citr\a}  and {\it Sw\a t\i}.
Presumably both procedures coexisted, and used
for confirmation of each other; one wonders however why then they were
not mentioned together. Notwithstanding the reasons for this and
whatever their  mutual role in practice, the
procedure as above marks a significant advance from a broader mathematical
point of view.

\section{Construction of rectilinear figures}

Towards construction of the basic figures needed to be drawn,
viz. rectangles, isosceles
triangles, symmetric trapezia, with prescribed sizes, the
\suls\ principally describe the steps for drawing perpendiculars to the
line of symmetry (such a line was  a common feature of the figures
involved, it being along the east-west direction); these are
however packaged into complete procedures, as in a manual,
for drawing the desired figures; see \cite{D2} for a discussion on
this.

\bsl's well-known construction of the square involves the method of
drawing a perpendicular that is now a familiar compass construction in
school geometry; given a line and a point on it, at which the perpendicular is to be drawn to the line, one picks two points on the line that are equidistant from the point and located on opposite sides, and draws arcs with centres at the points with radius greater than the distance from the point - the arcs intersect in two points, one on each side of the line, and joining them provides the desired  perpendicular  to the line passing through the given point. In
this form this method is absent in \ksl, though a variation may be
said to be involved in \ksl's prescription for locating the
north-south direction, after the east-west direction is drawn, as
mentioned above. On the whole during the entire \'sulva period it was
not common to use the compass construction as above for drawing perpendiculars, and it seems to
have disappeared by the time of \ksl.
A method, known as \N\ (also called {\it Niranchana}) method,
was more prevalent, and in \ksl\ it appears
as the ``canonical'' method for drawing perpendiculars. The
method is based on the converse of Pythagoras theorem, that in a
triangle with sides of lengths $a,b,c$
if $c^2=a^2+b^2$ then the sides with lengths $a$ and $b$ are
perpendicular to each other;\footnote{It was believed at one time that the ancient Egyptians also
  adopted such a method, but it has subsequently been discounted - see
  \cite{G}. In the case of the \suls\ however such a method is seen all over
  the place.} see \cite{D2} for details on the method and its
convenience as a tool.
 For the $a,b, c$ as above one uses what we now call
Pythagorean triples, the three being integers such that
$c^2=a^2+b^2$. The same of two such triples, $(3,4,5)$
and $(5,12,13)$, are involved in
the constructions in \bsl\ and \ksl\ \suls, using {\it Nyancana}. \bsl\ includes
a list with 5 primitive Pythagorean
triples, including the above and also  $(8,15, 17)$, $(12,35, 37)$ and
$(7,24,25)$, though they were not adopted for use with the \N\ method
(they are noted right after the statement of the Pythagorean theorem, and presumably meant as illustrations of the theorem
- see \cite{D2}). In
\ksl\ there is no mention of any of these other triples (or of other
new ones), though in \asl\ we find four of the above triples, excluding
 $(7,24,25)$, used in the construction of the {\it Mah\a vedi} by the
 \N\  method.

\section{Pythagoras theorem and its applications}

The most notable feature of the \suls ~in terms of geometric theory is
the statement of the so called Pythagoras theorem. This stands out
especially in the context of the fact that some of them, especially
\bsl, possibly predate Pythagoras.
Actually neither the notion of a right angle nor of a right angled
triangle
are found in the \suls, as concepts; of course right angled triangles
appeared as parts of various figures, and were implicit in the \N
~operations, but were not identified separately. Thus the statement of the
Pythagoras theorem occurs not with respect to right angled triangles,
but rather with reference to rectangles. A close translation of how it
is stated in \bsl ~would be ``the diagonal of a rectangle makes as much
(area) as (the areas) made separately by the base and the side put
together''.  The same statement also
 appears in \ksl\ (s\u tra 2.7) where it is followed by a clause ``{\it iti
  k\s etrajn\a nam}''. The term {\it
  k\s etra} involved in this has been translated as ``area'' by
Thibaut, but as
``figure'' by Datta \cite{Dat}. It is argued in \cite{SB} that \suls\
use the term {\it bh\u mi} for area, so the expression as above
means ``this is the knowledge about plane figures''. Whatever be
precise nuance of the meaning, the clause is evidently intended to
emphasize the importance of the statement to the reader. In this
respect it has a pedagogical value which seems significant.

\medskip
The Pythagoras theorem is also applied in the \suls\ for constructing
squares with area equal to the sum of areas of
  two given  squares (including doubling of a square, called {\it
    dvikara\d ni} which is described separately), and the difference
  of areas of
  two given squares (with unequal areas). The constructions, which are
 of course a direct application of the
Pythagoras theorem, are
  illustrated in the following Figure; see \cite{D2} for details.

\begin{figure}[ht!]
\begin{center}
\includegraphics[width=50mm]{pic1.jpg}~~~~~~~
\includegraphics[width=50mm]{pic2.jpg}
\caption{{The thick lines give the sides of the squares with areas equal to the sum and difference,
respectively, of two given squares, with bases PA and PB as in the figure.}}
\end{center}
\end{figure}

The procedure for ``squaring'' of the difference of two squares is
also used in
the \suls, except \msl\ \sul, for squaring a rectangle, by first
expressing it as a difference of two squares (by moving around half of the
extra part on the longer side); see \cite{D2} for details.

The augmentation of squares was used systematically in the \suls\
for replicating
given figures in larger size, by simply enhancing the size of the reference
unit by the desired amount; e.g. to produce a replica of a figure with
area $7\frac 12$ {\it puru\d sa} to one with area $8\frac 12$ {\it
  puru\d sa}, as was required, the unit would be changed in a way that
the area will increase by a factor of $1+\frac 2{15}$; the side for
this would be obtained as a combination of the original unit with a
square
of area $\frac 2{15}$th  of it. In fact this problem may have been the
inspiration for their discovery of the Pythagoras theorem; see
\cite{D2} for a discussion on how they may have arrived at the
theorem.

While the conceptual framework in this respect is common to all the
\suls, \ksl\ is seen to deal with some of the
features involved more dexterously than in the earlier \suls. The use
of the method
combining squares and rectangles seems to have become by now an art,
with the individual steps dealt with almost casually.
In the construction of the {\it dro\d naciti} (s\u tras at the
beginning of Chapter~4) for instance, it
is quite casually prescribed to divide the square into 10 parts and to make
one of them into a square and the rest into another
square.\footnote{In \cite{SB}, both in the translation of the s\u tra
  for this (4.2 on page 123) and the commentary on it page 268, it is
  said that the square is to be divided into 100 parts; that
  interpretation is
  however incorrect, as can be seen from \cite{Kh} and \cite{K}.}
On the problem of augmenting the unit for the purpose as described
above, \ksl\ introduces a ``rule of thumb'' method; it however does
not seem to conform to the standard stipulations accurately; apparently it was decided to pay a price in terms of accuracy in aid  of simplicity of execution.

There is one especially notable mathematical observation found in
\ksl\ in this context. It is the procedure to produce a square with
area equal to any desired multiple of the unit. In the general \suls\
spirit this could be done by augmentation of squares of smaller
squares, starting with complete squares. \ksl\ proposes  a direct
method, that it be constructed as the altitude of an isosceles
triangle whose base is one less than the desired number (of area
multiple) and the two
equal sides add to one more than the desired number. This is an
interesting application of Pythagoras theorem and the identity
$\frac 14 (n+1)^2-\frac 14(n-1)^2=n$. While there is indeed nothing quite like an
abstract ``variable'' $n$ in the modern sense involved, the identity
seems to
have been realised in terms of the desired number of unit squares to
be combined ({\it  y\a vatpram\a \d n\a ni samacaturasr\a \d ni}),
presumably by inspection of square grids.

\section{The square and the circle}

\ksl\ \sul\ gives the same method as \bsl\ for ``transforming'' a square into a
circle, namely for producing a circle with area equal to that of the
given square; it may be recalled that this consists of taking half the
diagonal of the square, dropping it from the centre along
the midriff, and drawing the circle with radius which includes half
the side and a third of
the part jutting out, namely $PR$ as seen in the Figure~2 (see \cite{D2}
for details).

 \begin{figure}[ht!]
\begin{center}
\includegraphics[width=65mm]{pic3.jpg}
\caption{{Circling the square: the thick line PR is given as the radius of the desired circle with area equal to that of the square ABCD.}}
\end{center}
\end{figure}

While the procedure
is interesting (especially in its application of an intuitive
``mean-value principle'') it is not very accurate. The area of this circle
for the unit square works out to be $1.0172524...$, about $1.7 \%$ more than
that of the original square, and a computation of the value of $\pi$
with it comes to  $3.088 ...$). Despite this, there seems to have
been no change made from \bsl\ to \ksl. On the other hand the \msl\
\sul, though less ``sophisticated'' than either of these, and
substantially older than \ksl, seems to contain a more accurate
procedure for producing a circle with the area of a given square; see
\cite{D2}. The {Maitr\a ya\n \i ya} \sul,
which is akin to \msl\ \sul\  gives a construction which involves
taking the radius of the desired circle to be $\frac 9{16}$ times the
side of the given square; see \cite{RCG}. Both of these involve only
about $\frac 12$ percent error.

The converse problem of  ``squaring the circle'' viz. finding a square
with the area of a
given circle is also considered in the \suls. Typically the treatment is not
geometric, but by assigning a numerical relation between the
side of the desired square to the diameter of the given
circle; according to \cite{Hay}, sutra 3.2.10 from
\msl ~is in fact a geometric construction for squaring the circle,
but we shall not go into it here; see \cite{D2}. \bsl\ \sul\
gives two formulae for squaring the circle.
The first one gives the value for the side of the square with area
equal to that of the circle with unit radius to be $${\frac 78}+\frac
1{8\times 29}-
\frac 1{8\times 29 \times 6}+\frac 1{8\times 29\times 6 \times 8}. \
\ \ \ \ (*)$$
 The area of the square with that as the side works out to be
 $3.088...$, about $98.3\%$ of the actual value. The second
 prescription consists of  taking $\frac {13}{15}$th of
the diameter of the given circle for the side of the desired square.
 The second is qualified by \bsl\ as
an ``incidental'' ({\it anitya}) method for squaring, signifying that
not wishing
to use the cumbersome formula one could do with this approximate one.
Curiously, only this crude formula, giving a value that is smaller
by $4\%$ has been described in
\ksl ~\suls\ (as also \asl) for the purpose.

\section{The square root of 2}

Three of the four \suls,
\bsl, \asl ~and \ksl, describe a formula for $\sqrt 2$ (in
words) which corresponds to expressing the value as
$$1+\frac 13 + \frac 1{3\times 4}-\frac 1{3\times 4 \times 34}.$$
In decimal expansion the value works out to be $1.4142157\dots$, and
is noted to be accurate upto 5 decimal places.\footnote{It may be
  recalled here that the Babylonians also had a similarly close
  approximation for $\sqrt 2$, as $1.4142129\dots$, expressed in the
  sexagesimal   system that they used.}

The s\u tra giving the formula is followed by ``{\it savi\'se\s a\h}''
in \bsl, ``{\it  sa vi\'
  se\s a\h}'' in \asl ~and ``{\it  sa vi\'se\s a iti vi\'se\s a\h}'' in
\ksl. The word {\it vi\'se\s a\h} means ``extra''. However it does not
refer to any comparison with an accurate value of $\sqrt 2$. It is
known from the tradition of {\it \'sulvavid}s that {\it vi\'se\s a\h}
was used as a technical term for the difference between the {\it
  dvikara\d ni}, namely $\sqrt 2$, and the unit (signifying what comes
up as extra in terms of the side, while doubling a square), and in
conjunction with it  {\it savi\'se\s a\h} stood for the {\it
  dvikara\d ni} itself. Occurrence of the phrase following the s\u tra
is what tells us what the number in the s\u tra stands for (the rest of
the s\u tra only provides a number and contains no reference to what it is).

In \cite{SB} the second part ``{\it iti vi\'se\s a\h}'' has been
translated as ``this is approximate.'' (curiously, reference the s\u
tra is missing from the commentary section in the book); see also
\cite{P}, pp. 21. However, there does not seem to be adequate
justification for interpreting or connecting the part with an
assertion about the value being approximate. Khadilkar \cite{Kh}
translates the part, in Marathi, as ``Ha {\it dvikara\d
  ni} \d tharavi\d nyaca nira\d la prak\a ra.'', or ``This is a different
method of determining {\it dvikara\d
  ni}''.\footnote{My translation from the Marathi version.}

The Karka bh\a \d sya commentary
seems to confirm this; see \cite{Kh} for the commentary. The overall
context seems to favour this interpretation. From all indications the
close to accurate value
of $\sqrt 2$ was computed, by \bsl\ or around the time, not for
practical application, for which it is not at all suitable, but to
facilitate the computation of the intricate formula for squaring the
circle,  $(*)$ as above; see \cite{Sei} and \cite{D2} for detailed
argument in this respect. However, subsequent to \bsl\ somehow no one
seems to have been interested in that formula, they being content to use
the simple proportion of 13:15 for the desired ratio. The formula for
$\sqrt 2$ then became a curiosity, bereft of its
original significance (a nice-looking formula propounded by masters of
a bygone era). It was thus a different, unusual, formula for the
{\it dvikara\d ni}, which actually for their purpose they could simply
measure out from the diagonal with a rope.

There is also another interpretation possible. As noted above
 {\it vi\'se\s a\h} stands for the excess of the {\it dvikara\d
  ni} over the unit. The s\u tra thus seems to say that {\it vi\'se\s
  a\h} is such that {\it  sa vi\'se\s a} is given by the previous
expression. This is suggested by the translation in \cite{K}, where
{\it iti vi\'se\s a\h} is translated, in Hindi, as ``Yaha vi\'se\d sa
ki vy\a khy\a\ hai''. It may also be recalled here that the word
``{\it iti}'' in Sanskrit corresponds to ``in this manner'', ``thus'' or
``as you know'' (see \cite{M}) which fits well with this
interpretation.

Of course it would have been known, at least when the formula $\sqrt
2$ was first
established, that it is not exact. A formula of this kind had
to be arrived at in some way (see \cite{D2} for a discussion on the
possibilities in this respect), and whichever way it was, it would
have been clear that an adjustment remained to be made. There is
however no indication that they considered it a significant fact worth
noting.
\iffalse
Inclination to distinguish between a
conceptualised accurate value with a tangible value close to
it, and keep track of it, is not found in \suls\ and it seems
unrealistic to expect it in the addendum to the s\u tra as above.
\fi
\bigskip

\section{Concluding remarks}

On the whole one notices that in the directions which were applicable
to the practical issues they met with, in terms of constructing various
rectilinear figures with conditions on the area etc., there was
progress in terms of simplifying the procedures and devising new
ones. However not much attention seems to have been paid,
collectively, to preserving
interesting findings, even those with high aesthetic qualities, that
were not directly involved in regular practice. In some ways this could be the
result of a diffused organisation, with feeble communication and
inadequate opportunities for intellectual interaction.

\bigskip
\noindent{\it Acknowledgement}: The author would like to thank Kim Plofker for some useful comments on an earlier version of the manuscript and Manoj Choudhury for producing soft versions of the figures.

{\small


TITLE: Exact sequences and (semi) direct product
QUESTION [3 upvotes]: Let $0 \longrightarrow H \longrightarrow G  \longrightarrow K \longrightarrow 0$ be a short exact sequence. My question is quite general: how can one recover $G$ knowing $H$ and $K$?

Naive question: is $G$ isomorphic to $ H \times K$? Clearly not, take any non trivial semidirect product.
Is $G$ isomorphic to a semidirect product between $H$ and $K$? It seems very unlikely since in that case $K$ would have to lift to a subgroup of $G$, but I can't think of a counterexample.
Under this last assumption (that $K$ lifts to a subgroup of $H$ on which the restriction of the last arrow induces an isomorphism), is $G$ isomorphic to a semidirect product between $H$ and $K$?
More generally, are there classification of short exact sequences under nontrivial assumptions?

Thanks for your answers!

REPLY [9 votes]: Point 4 in full generality is the extension problem, which is a seriously difficult one.
For point $2$, take $G$ to be the cyclic group of order $4$, and $H$ its subgroup of order $2$.
For point 3, yes. (Of course you mean $K$ lifts to a subgroup of $G$.)
An important special case of point 4 is the Schur–Zassenhaus theorem, for the case when $H$ and $K$ have coprime orders.


TITLE: Do spaces admit a weak cogenerating set?
QUESTION [11 upvotes]: Let $\mathcal C$ be a category. Say that a class of objects $\mathcal S \subseteq \mathcal C$ is weakly cogenerating if the functors $Hom_{\mathcal C}(-,S)$ are jointly conservative, for $S \in \mathcal S$. That is, a map $X \to Y$ in $\mathcal C$ is an isomorphism if and only if it induces bijections $Hom_C(Y,S) \to Hom_C(X,S)$ for every $S \in \mathcal S$.
Of course, every category $C$ admits a weakly cogenerating class -- namely, take $\mathcal S = \mathcal C$. But it's frequently important to have a cogenerating set -- i.e. to require that $\mathcal S$ is small.
Question: Does the homotopy category (of spaces) admit a weak cogenerating set?
It's clear that the homotopy category of simply-connected spaces admits a weak cogenerating set -- we can take $\mathcal S = \{K(\mathbb Z, n) \mid n \geq 2\}$ or alternatively $\mathcal S = \{K(k,n) \mid n \geq 2, k \in \{\mathbb Q, \mathbb F_p\}\}$ in this case by the cohomology Whitehead theorem. But I'm pessimistic about the chances of doing something similar with arbitrary spaces.

Relatedly, I wonder whether the category of groups admits a weak cogenerating set.
I also wonder whether the class of truncated spaces -- those spaces $S$ for which $\pi_k(S) = 0$ for $k$ sufficiently large -- is a cogenerating class for the homotopy category. What about the class of Eilenberg-MacLane spaces?

REPLY [6 votes]: For any infinite set $X$ let $S_X$ be the group of bijections $\sigma \colon X\to X$ such that $\{x : \sigma(x)\neq x\}$ is finite.  This still has signature homomorphism, and the alternating subgroup $A_X$ is simple, and has the same cardinality as $X$.  Now let $\mathcal{G}$ be a set of groups, and put $\kappa = \max \{|G|:G\in\mathcal{G}\}$.  Then $\text{Hom}(A_X,G)$ will be a singleton for all $G\in\mathcal{G}$ and $X$ with $|X|>\kappa$ (because the kernel of any homomorphism is nontrivial by cardinality, and so is the whole of $A_X$ by simplicity).  So $\mathcal{G}$ is not a weak cogenerating set.
It doesn't seem to be straightforward to deduce the corresponding result for the homotopy category.
EDIT To summarize the discussion in the comments, we can indeed deduce the corresponding result for the homotopy category with a little more work. Choose an acyclic simple group $G$ bigger than the fundamental group of any space in $\mathcal S$. Then any map $f: BG \to S$ for $S \in \mathcal S$ is trivial on $\pi_1$ by simplicity, so it lifts to the universal cover $\tau_{\geq 2} S$. By acyclicity, the composite map $BG \to \tau_{\geq 2} S \to K(\pi_2(S),2)$ is trivial so $f$ lifts through the 2-connected cover $\tau_{\geq 3} S$. Continue in this manner, lifting through the Whitehead tower to see that $f$ is nullhomotopic. Thus $\mathcal S$ does not distinguish $BG$ from a point, and is not weakly cogenerating.


text:
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura
-/
import algebra.group_power.order
import algebra.big_operators.basic

/-!
# Definitions and properties of `gcd`, `lcm`, and `coprime`

-/

namespace nat

/-! ### `gcd` -/

theorem gcd_dvd (m n : ℕ) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) :=
gcd.induction m n
  (λn, by rw gcd_zero_left; exact ⟨dvd_zero n, dvd_refl n⟩)
  (λm n npos, by rw ←gcd_rec; exact λ ⟨IH₁, IH₂⟩, ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩)

theorem gcd_dvd_left (m n : ℕ) : gcd m n ∣ m := (gcd_dvd m n).left

theorem gcd_dvd_right (m n : ℕ) : gcd m n ∣ n := (gcd_dvd m n).right

theorem gcd_le_left {m} (n) (h : 0 < m) : gcd m n ≤ m := le_of_dvd h $ gcd_dvd_left m n

theorem gcd_le_right (m) {n} (h : 0 < n) : gcd m n ≤ n := le_of_dvd h $ gcd_dvd_right m n

theorem dvd_gcd {m n k : ℕ} : k ∣ m → k ∣ n → k ∣ gcd m n :=
gcd.induction m n (λn _ kn, by rw gcd_zero_left; exact kn)
  (λn m mpos IH H1 H2, by rw gcd_rec; exact IH ((dvd_mod_iff H1).2 H2) H1)

theorem dvd_gcd_iff {m n k : ℕ} : k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n :=
iff.intro (λ h, ⟨h.trans (gcd_dvd m n).left, h.trans (gcd_dvd m n).right⟩)
          (λ h, dvd_gcd h.left h.right)

theorem gcd_comm (m n : ℕ) : gcd m n = gcd n m :=
dvd_antisymm
  (dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n))
  (dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m))

theorem gcd_eq_left_iff_dvd {m n : ℕ} : m ∣ n ↔ gcd m n = m :=
⟨λ h, by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left],
 λ h, h ▸ gcd_dvd_right m n⟩

theorem gcd_eq_right_iff_dvd {m n : ℕ} : m ∣ n ↔ gcd n m = m :=
by rw gcd_comm; apply gcd_eq_left_iff_dvd

theorem gcd_assoc (m n k : ℕ) : gcd (gcd m n) k = gcd m (gcd n k) :=
dvd_antisymm
  (dvd_gcd
    ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_left m n))
    (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_right m n))
      (gcd_dvd_right (gcd m n) k)))
  (dvd_gcd
    (dvd_gcd (gcd_dvd_left m (gcd n k)) ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_left n k)))
    ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))

@[simp] theorem gcd_one_right (n : ℕ) : gcd n 1 = 1 :=
eq.trans (gcd_comm n 1) $ gcd_one_left n

theorem gcd_mul_left (m n k : ℕ) : gcd (m * n) (m * k) = m * gcd n k :=
gcd.induction n k
  (λk, by repeat {rw mul_zero <|> rw gcd_zero_left})
  (λk n H IH, by rwa [←mul_mod_mul_left, ←gcd_rec, ←gcd_rec] at IH)

theorem gcd_mul_right (m n k : ℕ) : gcd (m * n) (k * n) = gcd m k * n :=
by rw [mul_comm m n, mul_comm k n, mul_comm (gcd m k) n, gcd_mul_left]

theorem gcd_pos_of_pos_left {m : ℕ} (n : ℕ) (mpos : 0 < m) : 0 < gcd m n :=
pos_of_dvd_of_pos (gcd_dvd_left m n) mpos

theorem gcd_pos_of_pos_right (m : ℕ) {n : ℕ} (npos : 0 < n) : 0 < gcd m n :=
pos_of_dvd_of_pos (gcd_dvd_right m n) npos

theorem eq_zero_of_gcd_eq_zero_left {m n : ℕ} (H : gcd m n = 0) : m = 0 :=
or.elim (nat.eq_zero_or_pos m) id
  (assume H1 : 0 < m, absurd (eq.symm H) (ne_of_lt (gcd_pos_of_pos_left _ H1)))

theorem eq_zero_of_gcd_eq_zero_right {m n : ℕ} (H : gcd m n = 0) : n = 0 :=
by rw gcd_comm at H; exact eq_zero_of_gcd_eq_zero_left H

@[simp] theorem gcd_eq_zero_iff {i j : ℕ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
begin
  split,
  { intro h,
    exact ⟨eq_zero_of_gcd_eq_zero_left h, eq_zero_of_gcd_eq_zero_right h⟩, },
  { rintro ⟨rfl, rfl⟩,
    exact nat.gcd_zero_right 0 }
end

theorem gcd_div {m n k : ℕ} (H1 : k ∣ m) (H2 : k ∣ n) :
  gcd (m / k) (n / k) = gcd m n / k :=
or.elim (nat.eq_zero_or_pos k)
  (λk0, by rw [k0, nat.div_zero, nat.div_zero, nat.div_zero, gcd_zero_right])
  (λH3, nat.eq_of_mul_eq_mul_right H3 $ by rw [
    nat.div_mul_cancel (dvd_gcd H1 H2), ←gcd_mul_right,
    nat.div_mul_cancel H1, nat.div_mul_cancel H2])

theorem gcd_greatest {a b d : ℕ} (hda : d ∣ a) (hdb : d ∣ b)
  (hd : ∀ e : ℕ, e ∣ a → e ∣ b → e ∣ d) : d = a.gcd b :=
(dvd_antisymm (hd _ (gcd_dvd_left a b) (gcd_dvd_right a b)) (dvd_gcd hda hdb)).symm

theorem gcd_dvd_gcd_of_dvd_left {m k : ℕ} (n : ℕ) (H : m ∣ k) : gcd m n ∣ gcd k n :=
dvd_gcd ((gcd_dvd_left m n).trans H) (gcd_dvd_right m n)

theorem gcd_dvd_gcd_of_dvd_right {m k : ℕ} (n : ℕ) (H : m ∣ k) : gcd n m ∣ gcd n k :=
dvd_gcd (gcd_dvd_left n m) ((gcd_dvd_right n m).trans H)

theorem gcd_dvd_gcd_mul_left (m n k : ℕ) : gcd m n ∣ gcd (k * m) n :=
gcd_dvd_gcd_of_dvd_left _ (dvd_mul_left _ _)

theorem gcd_dvd_gcd_mul_right (m n k : ℕ) : gcd m n ∣ gcd (m * k) n :=
gcd_dvd_gcd_of_dvd_left _ (dvd_mul_right _ _)

theorem gcd_dvd_gcd_mul_left_right (m n k : ℕ) : gcd m n ∣ gcd m (k * n) :=
gcd_dvd_gcd_of_dvd_right _ (dvd_mul_left _ _)

theorem gcd_dvd_gcd_mul_right_right (m n k : ℕ) : gcd m n ∣ gcd m (n * k) :=
gcd_dvd_gcd_of_dvd_right _ (dvd_mul_right _ _)

theorem gcd_eq_left {m n : ℕ} (H : m ∣ n) : gcd m n = m :=
dvd_antisymm (gcd_dvd_left _ _) (dvd_gcd dvd_rfl H)

theorem gcd_eq_right {m n : ℕ} (H : n ∣ m) : gcd m n = n :=
by rw [gcd_comm, gcd_eq_left H]

-- Lemmas where one argument is a multiple of the other

@[simp] lemma gcd_mul_left_left (m n : ℕ) : gcd (m * n) n = n :=
dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (dvd_mul_left _ _) dvd_rfl)

@[simp] lemma gcd_mul_left_right (m n : ℕ) : gcd n (m * n) = n :=
by rw [gcd_comm, gcd_mul_left_left]

@[simp] lemma gcd_mul_right_left (m n : ℕ) : gcd (n * m) n = n :=
by rw [mul_comm, gcd_mul_left_left]

@[simp] lemma gcd_mul_right_right (m n : ℕ) : gcd n (n * m) = n :=
by rw [gcd_comm, gcd_mul_right_left]

-- Lemmas for repeated application of `gcd`

@[simp] lemma gcd_gcd_self_right_left (m n : ℕ) : gcd m (gcd m n) = gcd m n :=
dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (gcd_dvd_left _ _) dvd_rfl)

@[simp] lemma gcd_gcd_self_right_right (m n : ℕ) : gcd m (gcd n m) = gcd n m :=
by rw [gcd_comm n m, gcd_gcd_self_right_left]

@[simp] lemma gcd_gcd_self_left_right (m n : ℕ) : gcd (gcd n m) m = gcd n m :=
by rw [gcd_comm, gcd_gcd_self_right_right]

@[simp] lemma gcd_gcd_self_left_left (m n : ℕ) : gcd (gcd m n) m = gcd m n :=
by rw [gcd_comm m n, gcd_gcd_self_left_right]

-- Lemmas where one argument consists of addition of a multiple of the other

@[simp] lemma gcd_add_mul_right_right (m n k : ℕ) : gcd m (n + k * m) = gcd m n :=
by simp [gcd_rec m (n + k * m), gcd_rec m n]

@[simp] lemma gcd_add_mul_left_right (m n k : ℕ) : gcd m (n + m * k) = gcd m n :=
by simp [gcd_rec m (n + m * k), gcd_rec m n]

@[simp] lemma gcd_mul_right_add_right (m n k : ℕ) : gcd m (k * m + n) = gcd m n :=
by simp [add_comm _ n]

@[simp] lemma gcd_mul_left_add_right (m n k : ℕ) : gcd m (m * k + n) = gcd m n :=
by simp [add_comm _ n]

@[simp] lemma gcd_add_mul_right_left (m n k : ℕ) : gcd (m + k * n) n = gcd m n :=
by rw [gcd_comm, gcd_add_mul_right_right, gcd_comm]

@[simp] lemma gcd_add_mul_left_left (m n k : ℕ) : gcd (m + n * k) n = gcd m n :=
by rw [gcd_comm, gcd_add_mul_left_right, gcd_comm]

@[simp] lemma gcd_mul_right_add_left (m n k : ℕ) : gcd (k * n + m) n = gcd m n :=
by rw [gcd_comm, gcd_mul_right_add_right, gcd_comm]

@[simp] lemma gcd_mul_left_add_left (m n k : ℕ) : gcd (n * k + m) n = gcd m n :=
by rw [gcd_comm, gcd_mul_left_add_right, gcd_comm]

-- Lemmas where one argument consists of an addition of the other

@[simp] lemma gcd_add_self_right (m n : ℕ) : gcd m (n + m) = gcd m n :=
eq.trans (by rw one_mul) (gcd_add_mul_right_right m n 1)

@[simp] lemma gcd_add_self_left (m n : ℕ) : gcd (m + n) n = gcd m n :=
by rw [gcd_comm, gcd_add_self_right, gcd_comm]

@[simp] lemma gcd_self_add_left (m n : ℕ) : gcd (m + n) m = gcd n m :=
by rw [add_comm, gcd_add_self_left]

@[simp] lemma gcd_self_add_right (m n : ℕ) : gcd m (m + n) = gcd m n :=
by rw [add_comm, gcd_add_self_right]

/-! ### `lcm` -/

theorem lcm_comm (m n : ℕ) : lcm m n = lcm n m :=
by delta lcm; rw [mul_comm, gcd_comm]

@[simp]
theorem lcm_zero_left (m : ℕ) : lcm 0 m = 0 :=
by delta lcm; rw [zero_mul, nat.zero_div]

@[simp]
theorem lcm_zero_right (m : ℕ) : lcm m 0 = 0 := lcm_comm 0 m ▸ lcm_zero_left m

@[simp]
theorem lcm_one_left (m : ℕ) : lcm 1 m = m :=
by delta lcm; rw [one_mul, gcd_one_left, nat.div_one]

@[simp]
theorem lcm_one_right (m : ℕ) : lcm m 1 = m := lcm_comm 1 m ▸ lcm_one_left m

@[simp]
theorem lcm_self (m : ℕ) : lcm m m = m :=
or.elim (nat.eq_zero_or_pos m)
  (λh, by rw [h, lcm_zero_left])
  (λh, by delta lcm; rw [gcd_self, nat.mul_div_cancel _ h])

theorem dvd_lcm_left (m n : ℕ) : m ∣ lcm m n :=
dvd.intro (n / gcd m n) (nat.mul_div_assoc _ $ gcd_dvd_right m n).symm

theorem dvd_lcm_right (m n : ℕ) : n ∣ lcm m n :=
lcm_comm n m ▸ dvd_lcm_left n m

theorem gcd_mul_lcm (m n : ℕ) : gcd m n * lcm m n = m * n :=
by delta lcm; rw [nat.mul_div_cancel' ((gcd_dvd_left m n).trans (dvd_mul_right m n))]

theorem lcm_dvd {m n k : ℕ} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k :=
or.elim (nat.eq_zero_or_pos k)
  (λh, by rw h; exact dvd_zero _)
  (λkpos, dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left n (pos_of_dvd_of_pos H1 kpos)) $
    by rw [gcd_mul_lcm, ←gcd_mul_right, mul_comm n k];
       exact dvd_gcd (mul_dvd_mul_left _ H2) (mul_dvd_mul_right H1 _))

theorem lcm_dvd_mul (m n : ℕ) : lcm m n ∣ m * n :=
lcm_dvd (dvd_mul_right _ _) (dvd_mul_left _ _)

lemma lcm_dvd_iff {m n k : ℕ} : lcm m n ∣ k ↔ m ∣ k ∧ n ∣ k :=
⟨λ h, ⟨(dvd_lcm_left _ _).trans h, (dvd_lcm_right _ _).trans h⟩,
  and_imp.2 lcm_dvd⟩

theorem lcm_assoc (m n k : ℕ) : lcm (lcm m n) k = lcm m (lcm n k) :=
dvd_antisymm
  (lcm_dvd
    (lcm_dvd (dvd_lcm_left m (lcm n k)) ((dvd_lcm_left n k).trans (dvd_lcm_right m (lcm n k))))
    ((dvd_lcm_right n k).trans (dvd_lcm_right m (lcm n k))))
  (lcm_dvd
    ((dvd_lcm_left m n).trans (dvd_lcm_left (lcm m n) k))
    (lcm_dvd ((dvd_lcm_right m n).trans (dvd_lcm_left (lcm m n) k))
      (dvd_lcm_right (lcm m n) k)))

theorem lcm_ne_zero {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 :=
by { intro h, simpa [h, hm, hn] using gcd_mul_lcm m n, }

/-!
### `coprime`

See also `nat.coprime_of_dvd` and `nat.coprime_of_dvd'` to prove `nat.coprime m n`.
-/

instance (m n : ℕ) : decidable (coprime m n) := by unfold coprime; apply_instance

theorem coprime_iff_gcd_eq_one {m n : ℕ} : coprime m n ↔ gcd m n = 1 := iff.rfl

theorem coprime.gcd_eq_one {m n : ℕ} (h : coprime m n) : gcd m n = 1 := h

theorem coprime.lcm_eq_mul {m n : ℕ} (h : coprime m n) : lcm m n = m * n :=
by rw [←one_mul (lcm m n), ←h.gcd_eq_one, gcd_mul_lcm]

theorem coprime.symm {m n : ℕ} : coprime n m → coprime m n := (gcd_comm m n).trans

theorem coprime_comm {m n : ℕ} : coprime n m ↔ coprime m n := ⟨coprime.symm, coprime.symm⟩

theorem coprime.symmetric : symmetric coprime := λ m n, coprime.symm

theorem coprime.dvd_of_dvd_mul_right {m n k : ℕ} (H1 : coprime k n) (H2 : k ∣ m * n) : k ∣ m :=
let t := dvd_gcd (dvd_mul_left k m) H2 in
by rwa [gcd_mul_left, H1.gcd_eq_one, mul_one] at t

theorem coprime.dvd_of_dvd_mul_left {m n k : ℕ} (H1 : coprime k m) (H2 : k ∣ m * n) : k ∣ n :=
by rw mul_comm at H2; exact H1.dvd_of_dvd_mul_right H2

theorem coprime.dvd_mul_right {m n k : ℕ} (H : coprime k n) : k ∣ m * n ↔ k ∣ m :=
⟨H.dvd_of_dvd_mul_right, λ h, dvd_mul_of_dvd_left h n⟩

theorem coprime.dvd_mul_left {m n k : ℕ} (H : coprime k m) : k ∣ m * n ↔ k ∣ n :=
⟨H.dvd_of_dvd_mul_left, λ h, dvd_mul_of_dvd_right h m⟩

theorem coprime.gcd_mul_left_cancel {k : ℕ} (m : ℕ) {n : ℕ} (H : coprime k n) :
   gcd (k * m) n = gcd m n :=
have H1 : coprime (gcd (k * m) n) k,
by rw [coprime, gcd_assoc, H.symm.gcd_eq_one, gcd_one_right],
dvd_antisymm
  (dvd_gcd (H1.dvd_of_dvd_mul_left (gcd_dvd_left _ _)) (gcd_dvd_right _ _))
  (gcd_dvd_gcd_mul_left _ _ _)

theorem coprime.gcd_mul_right_cancel (m : ℕ) {k n : ℕ} (H : coprime k n) :
   gcd (m * k) n = gcd m n :=
by rw [mul_comm m k, H.gcd_mul_left_cancel m]

theorem coprime.gcd_mul_left_cancel_right {k m : ℕ} (n : ℕ) (H : coprime k m) :
   gcd m (k * n) = gcd m n :=
by rw [gcd_comm m n, gcd_comm m (k * n), H.gcd_mul_left_cancel n]

theorem coprime.gcd_mul_right_cancel_right {k m : ℕ} (n : ℕ) (H : coprime k m) :
   gcd m (n * k) = gcd m n :=
by rw [mul_comm n k, H.gcd_mul_left_cancel_right n]

theorem coprime_div_gcd_div_gcd {m n : ℕ} (H : 0 < gcd m n) :
  coprime (m / gcd m n) (n / gcd m n) :=
by rw [coprime_iff_gcd_eq_one, gcd_div (gcd_dvd_left m n) (gcd_dvd_right m n), nat.div_self H]

theorem not_coprime_of_dvd_of_dvd {m n d : ℕ} (dgt1 : 1 < d) (Hm : d ∣ m) (Hn : d ∣ n) :
  ¬ coprime m n :=
λ co, not_lt_of_ge (le_of_dvd zero_lt_one $ by rw [←co.gcd_eq_one]; exact dvd_gcd Hm Hn) dgt1

theorem exists_coprime {m n : ℕ} (H : 0 < gcd m n) :
  ∃ m' n', coprime m' n' ∧ m = m' * gcd m n ∧ n = n' * gcd m n :=
⟨_, _, coprime_div_gcd_div_gcd H,
  (nat.div_mul_cancel (gcd_dvd_left m n)).symm,
  (nat.div_mul_cancel (gcd_dvd_right m n)).symm⟩

theorem exists_coprime' {m n : ℕ} (H : 0 < gcd m n) :
  ∃ g m' n', 0 < g ∧ coprime m' n' ∧ m = m' * g ∧ n = n' * g :=
let ⟨m', n', h⟩ := exists_coprime H in ⟨_, m', n', H, h⟩

@[simp] theorem coprime_add_self_right {m n : ℕ} : coprime m (n + m) ↔ coprime m n :=
by rw [coprime, coprime, gcd_add_self_right]

@[simp] theorem coprime_self_add_right {m n : ℕ} : coprime m (m + n) ↔ coprime m n :=
by rw [add_comm, coprime_add_self_right]

@[simp] theorem coprime_add_self_left {m n : ℕ} : coprime (m + n) n ↔ coprime m n :=
by rw [coprime, coprime, gcd_add_self_left]

@[simp] theorem coprime_self_add_left {m n : ℕ} : coprime (m + n) m ↔ coprime n m :=
by rw [coprime, coprime, gcd_self_add_left]

@[simp] lemma coprime_add_mul_right_right (m n k : ℕ) : coprime m (n + k * m) ↔ coprime m n :=
by rw [coprime, coprime, gcd_add_mul_right_right]

@[simp] lemma coprime_add_mul_left_right (m n k : ℕ) : coprime m (n + m * k) ↔ coprime m n :=
by rw [coprime, coprime, gcd_add_mul_left_right]

@[simp] lemma coprime_mul_right_add_right (m n k : ℕ) : coprime m (k * m + n) ↔ coprime m n :=
by rw [coprime, coprime, gcd_mul_right_add_right]

@[simp] lemma coprime_mul_left_add_right (m n k : ℕ) : coprime m (m * k + n) ↔ coprime m n :=
by rw [coprime, coprime, gcd_mul_left_add_right]

@[simp] lemma coprime_add_mul_right_left (m n k : ℕ) : coprime (m + k * n) n ↔ coprime m n :=
by rw [coprime, coprime, gcd_add_mul_right_left]

@[simp] lemma coprime_add_mul_left_left (m n k : ℕ) : coprime (m + n * k) n ↔ coprime m n :=
by rw [coprime, coprime, gcd_add_mul_left_left]

@[simp] lemma coprime_mul_right_add_left (m n k : ℕ) : coprime (k * n + m) n ↔ coprime m n :=
by rw [coprime, coprime, gcd_mul_right_add_left]

@[simp] lemma coprime_mul_left_add_left (m n k : ℕ) : coprime (n * k + m) n ↔ coprime m n :=
by rw [coprime, coprime, gcd_mul_left_add_left]

theorem coprime.mul {m n k : ℕ} (H1 : coprime m k) (H2 : coprime n k) : coprime (m * n) k :=
(H1.gcd_mul_left_cancel n).trans H2

theorem coprime.mul_right {k m n : ℕ} (H1 : coprime k m) (H2 : coprime k n) : coprime k (m * n) :=
(H1.symm.mul H2.symm).symm

theorem coprime.coprime_dvd_left {m k n : ℕ} (H1 : m ∣ k) (H2 : coprime k n) : coprime m n :=
eq_one_of_dvd_one (by delta coprime at H2; rw ← H2; exact gcd_dvd_gcd_of_dvd_left _ H1)

theorem coprime.coprime_dvd_right {m k n : ℕ} (H1 : n ∣ m) (H2 : coprime k m) : coprime k n :=
(H2.symm.coprime_dvd_left H1).symm

theorem coprime.coprime_mul_left {k m n : ℕ} (H : coprime (k * m) n) : coprime m n :=
H.coprime_dvd_left (dvd_mul_left _ _)

theorem coprime.coprime_mul_right {k m n : ℕ} (H : coprime (m * k) n) : coprime m n :=
H.coprime_dvd_left (dvd_mul_right _ _)

theorem coprime.coprime_mul_left_right {k m n : ℕ} (H : coprime m (k * n)) : coprime m n :=
H.coprime_dvd_right (dvd_mul_left _ _)

theorem coprime.coprime_mul_right_right {k m n : ℕ} (H : coprime m (n * k)) : coprime m n :=
H.coprime_dvd_right (dvd_mul_right _ _)

theorem coprime.coprime_div_left {m n a : ℕ} (cmn : coprime m n) (dvd : a ∣ m) :
  coprime (m / a) n :=
begin
  by_cases a_split : (a = 0),
  { subst a_split,
    rw zero_dvd_iff at dvd,
    simpa [dvd] using cmn, },
  { rcases dvd with ⟨k, rfl⟩,
    rw nat.mul_div_cancel_left _ (nat.pos_of_ne_zero a_split),
    exact coprime.coprime_mul_left cmn, },
end

theorem coprime.coprime_div_right {m n a : ℕ} (cmn : coprime m n) (dvd : a ∣ n) :
  coprime m (n / a) :=
(coprime.coprime_div_left cmn.symm dvd).symm

lemma coprime_mul_iff_left {k m n : ℕ} : coprime (m * n) k ↔ coprime m k ∧ coprime n k :=
⟨λ h, ⟨coprime.coprime_mul_right h, coprime.coprime_mul_left h⟩,
  λ ⟨h, _⟩, by rwa [coprime_iff_gcd_eq_one, coprime.gcd_mul_left_cancel n h]⟩

lemma coprime_mul_iff_right {k m n : ℕ} : coprime k (m * n) ↔ coprime k m ∧ coprime k n :=
by simpa only [coprime_comm] using coprime_mul_iff_left

lemma coprime.gcd_left (k : ℕ) {m n : ℕ} (hmn : coprime m n) : coprime (gcd k m) n :=
hmn.coprime_dvd_left $ gcd_dvd_right k m

lemma coprime.gcd_right (k : ℕ) {m n : ℕ} (hmn : coprime m n) : coprime m (gcd k n) :=
hmn.coprime_dvd_right $ gcd_dvd_right k n

lemma coprime.gcd_both (k l : ℕ) {m n : ℕ} (hmn : coprime m n) : coprime (gcd k m) (gcd l n) :=
(hmn.gcd_left k).gcd_right l

lemma coprime.mul_dvd_of_dvd_of_dvd {a n m : ℕ} (hmn : coprime m n)
  (hm : m ∣ a) (hn : n ∣ a) : m * n ∣ a :=
let ⟨k, hk⟩ := hm in hk.symm ▸ mul_dvd_mul_left _ (hmn.symm.dvd_of_dvd_mul_left (hk ▸ hn))

theorem coprime_one_left : ∀ n, coprime 1 n := gcd_one_left

theorem coprime_one_right : ∀ n, coprime n 1 := gcd_one_right

theorem coprime.pow_left {m k : ℕ} (n : ℕ) (H1 : coprime m k) : coprime (m ^ n) k :=
nat.rec_on n (coprime_one_left _) (λn IH, H1.mul IH)

theorem coprime.pow_right {m k : ℕ} (n : ℕ) (H1 : coprime k m) : coprime k (m ^ n) :=
(H1.symm.pow_left n).symm

theorem coprime.pow {k l : ℕ} (m n : ℕ) (H1 : coprime k l) : coprime (k ^ m) (l ^ n) :=
(H1.pow_left _).pow_right _

@[simp] lemma coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ)  :
  nat.coprime (a ^ n) b ↔ nat.coprime a b :=
begin
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn.ne',
  rw [pow_succ, nat.coprime_mul_iff_left],
  exact ⟨and.left, λ hab, ⟨hab, hab.pow_left _⟩⟩
end

@[simp] lemma coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a b : ℕ)  :
  nat.coprime a (b ^ n) ↔ nat.coprime a b :=
by rw [nat.coprime_comm, coprime_pow_left_iff hn, nat.coprime_comm]

theorem coprime.eq_one_of_dvd {k m : ℕ} (H : coprime k m) (d : k ∣ m) : k = 1 :=
by rw [← H.gcd_eq_one, gcd_eq_left d]

@[simp] theorem coprime_zero_left (n : ℕ) : coprime 0 n ↔ n = 1 :=
by simp [coprime]

@[simp] theorem coprime_zero_right (n : ℕ) : coprime n 0 ↔ n = 1 :=
by simp [coprime]

theorem not_coprime_zero_zero : ¬ coprime 0 0 := by simp

@[simp] theorem coprime_one_left_iff (n : ℕ) : coprime 1 n ↔ true :=
by simp [coprime]

@[simp] theorem coprime_one_right_iff (n : ℕ) : coprime n 1 ↔ true :=
by simp [coprime]

@[simp] theorem coprime_self (n : ℕ) : coprime n n ↔ n = 1 :=
by simp [coprime]

lemma gcd_mul_of_coprime_of_dvd {a b c : ℕ} (hac : coprime a c) (b_dvd_c : b ∣ c) :
  gcd (a * b) c = b :=
begin
  rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩,
  rw [gcd_mul_right],
  convert one_mul b,
  exact coprime.coprime_mul_right_right hac,
end

section big_operators

open_locale big_operators

/-- See `is_coprime.prod_left` for the corresponding lemma about `is_coprime` -/
lemma coprime_prod_left
  {ι : Type*} {x : ℕ} {s : ι → ℕ} {t : finset ι} :
  (∀ (i : ι), i ∈ t → coprime (s i) x) → coprime (∏ (i : ι) in t, s i) x :=
finset.prod_induction s (λ y, y.coprime x) (λ a b, coprime.mul) (by simp)

/-- See `is_coprime.prod_right` for the corresponding lemma about `is_coprime` -/
lemma coprime_prod_right
  {ι : Type*} {x : ℕ} {s : ι → ℕ} {t : finset ι} :
  (∀ (i : ι), i ∈ t → coprime x (s i)) → coprime x (∏ (i : ι) in t, s i) :=
finset.prod_induction s (λ y, x.coprime y) (λ a b, coprime.mul_right) (by simp)

end big_operators

lemma coprime.eq_of_mul_eq_zero {m n : ℕ} (h : m.coprime n) (hmn : m * n = 0) :
  m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 :=
(nat.eq_zero_of_mul_eq_zero hmn).imp
  (λ hm, ⟨hm, n.coprime_zero_left.mp $ hm ▸ h⟩)
  (λ hn, ⟨m.coprime_zero_left.mp $ hn ▸ h.symm, hn⟩)

/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`. -/
def prod_dvd_and_dvd_of_dvd_prod {m n k : ℕ} (H : k ∣ m * n) :
  { d : {m' // m' ∣ m} × {n' // n' ∣ n} // k = d.1 * d.2 } :=
begin
cases h0 : (gcd k m),
case nat.zero
{ obtain rfl : k = 0 := eq_zero_of_gcd_eq_zero_left h0,
  obtain rfl : m = 0 := eq_zero_of_gcd_eq_zero_right h0,
  exact ⟨⟨⟨0, dvd_refl 0⟩, ⟨n, dvd_refl n⟩⟩, (zero_mul n).symm⟩ },
case nat.succ : tmp
{ have hpos : 0 < gcd k m := h0.symm ▸ nat.zero_lt_succ _; clear h0 tmp,
  have hd : gcd k m * (k / gcd k m) = k := (nat.mul_div_cancel' (gcd_dvd_left k m)),
  refine ⟨⟨⟨gcd k m,  gcd_dvd_right k m⟩, ⟨k / gcd k m, _⟩⟩, hd.symm⟩,
  apply dvd_of_mul_dvd_mul_left hpos,
  rw [hd, ← gcd_mul_right],
  exact dvd_gcd (dvd_mul_right _ _) H }
end

theorem gcd_mul_dvd_mul_gcd (k m n : ℕ) : gcd k (m * n) ∣ gcd k m * gcd k n :=
begin
rcases (prod_dvd_and_dvd_of_dvd_prod $ gcd_dvd_right k (m * n)) with ⟨⟨⟨m', hm'⟩, ⟨n', hn'⟩⟩, h⟩,
replace h : gcd k (m * n) = m' * n' := h,
rw h,
have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _,
apply mul_dvd_mul,
  { have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n',
    exact dvd_gcd hm'k hm' },
  { have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n',
    exact dvd_gcd hn'k hn' }
end

theorem coprime.gcd_mul (k : ℕ) {m n : ℕ} (h : coprime m n) : gcd k (m * n) = gcd k m * gcd k n :=
dvd_antisymm
  (gcd_mul_dvd_mul_gcd k m n)
  ((h.gcd_both k k).mul_dvd_of_dvd_of_dvd
    (gcd_dvd_gcd_mul_right_right _ _ _)
    (gcd_dvd_gcd_mul_left_right _ _ _))

theorem pow_dvd_pow_iff {a b n : ℕ} (n0 : 0 < n) : a ^ n ∣ b ^ n ↔ a ∣ b :=
begin
  refine ⟨λ h, _, λ h, pow_dvd_pow_of_dvd h _⟩,
  cases nat.eq_zero_or_pos (gcd a b) with g0 g0,
  { simp [eq_zero_of_gcd_eq_zero_right g0] },
  rcases exists_coprime' g0 with ⟨g, a', b', g0', co, rfl, rfl⟩,
  rw [mul_pow, mul_pow] at h,
  replace h := dvd_of_mul_dvd_mul_right (pow_pos g0' _) h,
  have := pow_dvd_pow a' n0,
  rw [pow_one, (co.pow n n).eq_one_of_dvd h] at this,
  simp [eq_one_of_dvd_one this]
end

lemma gcd_mul_gcd_of_coprime_of_mul_eq_mul {a b c d : ℕ} (cop : c.coprime d) (h : a * b = c * d) :
  a.gcd c * b.gcd c = c :=
begin
  apply dvd_antisymm,
  { apply nat.coprime.dvd_of_dvd_mul_right (nat.coprime.mul (cop.gcd_left _) (cop.gcd_left _)),
    rw ← h,
    apply mul_dvd_mul (gcd_dvd _ _).1 (gcd_dvd _ _).1 },
  { rw [gcd_comm a _, gcd_comm b _],
    transitivity c.gcd (a * b),
    rw [h, gcd_mul_right_right d c],
    apply gcd_mul_dvd_mul_gcd }
end

/-- If `k:ℕ` divides coprime `a` and `b` then `k = 1` -/
lemma eq_one_of_dvd_coprimes {a b k : ℕ} (h_ab_coprime : coprime a b)
  (hka : k ∣ a) (hkb : k ∣ b) : k = 1  :=
begin
  rw coprime_iff_gcd_eq_one at h_ab_coprime,
  have h1 := dvd_gcd hka hkb,
  rw h_ab_coprime at h1,
  exact nat.dvd_one.mp h1,
end

lemma coprime.mul_add_mul_ne_mul {m n a b : ℕ} (cop : coprime m n) (ha : a ≠ 0) (hb : b ≠ 0) :
  a * m + b * n ≠ m * n :=
begin
  intro h,
  obtain ⟨x, rfl⟩ : n ∣ a := cop.symm.dvd_of_dvd_mul_right
    ((nat.dvd_add_iff_left (dvd_mul_left n b)).mpr ((congr_arg _ h).mpr (dvd_mul_left n m))),
  obtain ⟨y, rfl⟩ : m ∣ b := cop.dvd_of_dvd_mul_right
    ((nat.dvd_add_iff_right (dvd_mul_left m (n*x))).mpr ((congr_arg _ h).mpr (dvd_mul_right m n))),
  rw [mul_comm, mul_ne_zero_iff, ←one_le_iff_ne_zero] at ha hb,
  refine mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) _),
  rw [← mul_assoc, ← h, add_mul, add_mul, mul_comm _ n, ←mul_assoc, mul_comm y]
end

end nat

subset_name: curated


TITLE: Evaluate the integral using partial fractions $\oint_\gamma\frac{z}{z^4 − 1}\mathrm dz$
QUESTION [2 upvotes]: Evaluate the integral
$\oint_\gamma\frac{z}{z^4 − 1}\mathrm dz$,
where $\gamma = \{z : |z − a| = a\}$, $a > 1$.
So without using residue theorem and considering that $z = a + ae^{i*\omega}$ gives usa very hard integral formula (at least idk how to solve it) the proper solution includes partial fractions: $\frac{z}{z^4 − 1} = \frac{1}{4}*(\frac{1}{z+1}+\frac{1}{z-1}-\frac{1}{z+i}-\frac{1}{z-i})$, from here we get that the only point which lies in the circle $|z-a|=a$ is $z=1$. Then by Cauchy-Goursat theorem we get that all the other integrals are equal to zero except for $\frac{1}{z-1}$ which is for some reason equal to $2i\pi$.
The question now is: why the other three ointegrals are 0 and why is the last one equal to $2i\pi$ (without deviding it by 4)

REPLY [0 votes]: Alternative way, without using residue theorem, but still using Cauchy's integral formula, stating:
$$f(w)=\frac{1}{2\pi i} \int\limits_{\gamma}\frac{f(z)}{z-w}dz$$
we replace $w=1$ (since you proved that only this point is in the circle) and $f(z)=\frac{z}{z^3+z^2+z+1}$ then we have
$$\frac{1}{4}=f(1)=\frac{1}{2\pi i}\int\limits_{|z-a|=a}\frac{f(z)}{z-1}dz=\\
\frac{1}{2\pi i}\int\limits_{|z-a|=a}\frac{z}{(z-1)(z^3+z^2+z+1)}dz=\\
\frac{1}{2\pi i}\int\limits_{|z-a|=a}\frac{z}{z^4-1}dz$$
and the result follows.
You can also use this theorem to show
$$1=\frac{1}{2\pi i}\int\limits_{|z-a|=a}\frac{1}{z-1}dz$$


TITLE: Differential Equation on a Pointlike Region
QUESTION [0 upvotes]: Lets say we have a region $[-a,a]$ on the real axis. On that region we define some non-trivial differential equation:
$$\left( \frac{\partial}{\partial x}y(x)\right)^2 = f(y(x))$$
with $x\in [-a,a]$. Now, if we take $a \rightarrow 0$ the region will shrink until the only available value for $x$ becomes $x\equiv 0$. How can I evaluate the differential equation at hand in this special case? Should I simply demand $f(y(0))=0$ ? I am looking for the logic behind the math in such cases in general.

REPLY [1 votes]: A differential equation on a region consisting of a single point doesn't make any sense.  You should be looking at the differential equation when $a > 0$, computing whatever you need to there, and then you can study limits of those quantities as
$a \to 0+$.

REPLY [0 votes]: In general you need an open subset of $R$ to talk about derivatives in the classical sense.  An open set needs to have a neighborhood around each point meaning that it is never a single point.


TITLE: A fair die is rolled 5 times resulting in outcomes $X_i$, with $i=1,\dots,5$. Find $P(X_2+X_3<X_3+X_4)$
QUESTION [0 upvotes]: I was looking at the solutions to this problem:
A fair die is rolled 5 times resulting in outcomes  $X_i$, with $i=1,\dots,5$.
Find  $P(X_2+X_3<X_3+X_4)$.
Why does that probability equate to $P(X_3<X_4)$? Shouldn't it be $P(X_2<X_4)$?

REPLY [1 votes]: $\newcommand{\braces}[1]{\left\lbrace\,{#1}\,\right\rbrace}
 \newcommand{\bracks}[1]{\left\lbrack\,{#1}\,\right\rbrack}
 \newcommand{\dd}{\mathrm{d}}
 \newcommand{\ds}[1]{\displaystyle{#1}}
 \newcommand{\expo}[1]{\,\mathrm{e}^{#1}\,}
 \newcommand{\ic}{\mathrm{i}}
 \newcommand{\mc}[1]{\mathcal{#1}}
 \newcommand{\mrm}[1]{\mathrm{#1}}
 \newcommand{\pars}[1]{\left(\,{#1}\,\right)}
 \newcommand{\partiald}[3][]{\frac{\partial^{#1} #2}{\partial #3^{#1}}}
 \newcommand{\root}[2][]{\,\sqrt[#1]{\,{#2}\,}\,}
 \newcommand{\totald}[3][]{\frac{\mathrm{d}^{#1} #2}{\mathrm{d} #3^{#1}}}
 \newcommand{\verts}[1]{\left\vert\,{#1}\,\right\vert}$
\begin{align}
\mrm{P}\pars{X_{2} + X_{3} < X_{3} + X_{4}} & =
{1 \over 6}\sum_{x_{1} = 1}^{6}{1 \over 6}\sum_{x_{2} = 1}^{6}
{1 \over 6}\sum_{x_{3} = 1}^{6}{1 \over 6}\sum_{x_{4} = 1}^{6}
{1 \over 6}\sum_{x_{5} = 1}^{6}\bracks{x_{2} + x_{3} < x_{3} + x_{4}}
\\[5mm] & =
{1 \over 6^{2}}\sum_{x_{2} = 1}^{6}\sum_{x_{4} = 1}^{6}\bracks{x_{2} < x_{4}} =
{1 \over 6^{2}}\sum_{x_{2} = 1}^{6}\sum_{x_{4} = x_{2} + 1}^{6}1 =
{1 \over 6^{2}}\sum_{x_{2} = 1}^{6}\pars{6 - x_{2}}
\\[5mm] & =
{1 \over 6^{2}}\bracks{6 \times 6 - {6\pars{6 + 1} \over 2}} =
\bbox[8px,border:1px groove navy]{5 \over 12}
\end{align}


TITLE: Is there a quadruple product rule?
QUESTION [5 upvotes]: The triple product rule in multivariable calculus is widely used.  Can a quadruple product rule equation be written for an equation f(x,y,z,z2)=0?

REPLY [4 votes]: Actually, there is general product rule for $n$-tuple. It is almost the direct consequence of implicit function theorem. Assume $n$ variables satisfies $F(x_1,\ldots,x_n)=0$, we have
$$\frac{\partial x_i}{\partial x_j}=-{\partial F/\partial x_j\over\partial F/\partial x_i}$$
Then multiply all fractions
$$\frac{\partial x_1}{\partial x_2}\cdots\frac{\partial x_{n-1}}{\partial x_n}\frac{\partial x_n}{\partial x_1}=(-1)^n{\partial F/\partial x_2\over\partial F/\partial x_1}\cdots{\partial F/\partial x_n\over\partial F/\partial x_{n-1}}{\partial F/\partial x_1\over\partial F/\partial x_n}=(-1)^n$$