Merge pull request #24 from pitmonticone/main

Fix typos in blueprint, docstrings and notes

Author: kbuzzard

FLT/GlobalLanglandsConjectures/notes.tex

@@ -92,7 +92,7 @@ \section{Connected reductive groups}
 
 \subsection{Project: the theory of bialgebras.}
 
-A \emph{monoid} is a slighly simpler thing than a group. It has multiplication and identity, but it might not have inverses. This means that there are loads more monoids than groups, and that monoids are (a) simpler to work with but (b) much harder to classify (but this is OK, we don't want to classify them). The axioms for a monoid are the axioms for a group which don't mention inverses: they are $a\times(b\times c)=(a\times b)\times c$ and $1\times a=a\times 1=a$. The inverse axioms aren't there because they don't make sense. The naturals, integers, rationals, reals and complexes are all monoids under multiplication; they all have a 0 and 0 doesn't have an inverse, but this doesn't matter because monoids don't need inverses. A group is a monoid with some extra stuff (inverses), so a group variety is a monoid variety with extra stuff, so let's first discuss how to formalise monoid varieties. And this is easier than you think because the hard work (the key definition) has already been done.
+A \emph{monoid} is a slightly simpler thing than a group. It has multiplication and identity, but it might not have inverses. This means that there are loads more monoids than groups, and that monoids are (a) simpler to work with but (b) much harder to classify (but this is OK, we don't want to classify them). The axioms for a monoid are the axioms for a group which don't mention inverses: they are $a\times(b\times c)=(a\times b)\times c$ and $1\times a=a\times 1=a$. The inverse axioms aren't there because they don't make sense. The naturals, integers, rationals, reals and complexes are all monoids under multiplication; they all have a 0 and 0 doesn't have an inverse, but this doesn't matter because monoids don't need inverses. A group is a monoid with some extra stuff (inverses), so a group variety is a monoid variety with extra stuff, so let's first discuss how to formalise monoid varieties. And this is easier than you think because the hard work (the key definition) has already been done.
 
 A \emph{commutative bialgebra} over a field $K$ is a commutative $K$-algebra $A$ (i.e., a commutative ring $A$ equipped with a ring homomorphism from $K$ to $A$) equipped with two $K$-algebra maps called comultiplication $A\to A \otimes_KA$ and counit $A\to K$, satisfying some axioms. You can read these axioms on the \href{https://en.wikipedia.org/wiki/Bialgebra}{Wikipedia page for bialgebras}. The axioms look intimidating, but if you write them down and then look at them backwards then they become the usual axioms for monoids. The idea now is that if $L$ is any field containing $K$, then the set of $K$-algebra maps from $A$ to $L$ naturally becomes a monoid, and putting this monoid structure on this set is a nice challenge.
 
@@ -154,7 +154,7 @@ \subsection{Project: Frobenius elements for number fields}
 
 \subsection{Compatible families of Galois representations}
 
-I defined a family of representations $\rho_\lambda$ of $\Gal(\overline{K}/K)$ above. Let's stick to $K=\Q$ at first. The family is \emph{compatible} if there is a finite set of prime numbers $S$ and, for each prime $p$ \emph{not} in $S$ a monic degree $n$ polynomial $H_p\in E[X]$ with the following property: for every prime $\ell\not=p$ and every $\lambda : E\to\overline{\Q}_\ell$, the associated member $\rho_\lambda$ of the family has the property that the characteristic polynomial of $\rho_{\lambda}(F_p)$ is $H_p$. In words, we're saying that the $\rho_\lambda$ all have the same characteristic polynomials on these random Frobenius elements. You might want to deduce from this that all the $\rho_\lambda$ are isomorphic, but this is not in general the case; they're all continuous with respect to completely different and inompatible topologies, so they can't be.
+I defined a family of representations $\rho_\lambda$ of $\Gal(\overline{K}/K)$ above. Let's stick to $K=\Q$ at first. The family is \emph{compatible} if there is a finite set of prime numbers $S$ and, for each prime $p$ \emph{not} in $S$ a monic degree $n$ polynomial $H_p\in E[X]$ with the following property: for every prime $\ell\not=p$ and every $\lambda : E\to\overline{\Q}_\ell$, the associated member $\rho_\lambda$ of the family has the property that the characteristic polynomial of $\rho_{\lambda}(F_p)$ is $H_p$. In words, we're saying that the $\rho_\lambda$ all have the same characteristic polynomials on these random Frobenius elements. You might want to deduce from this that all the $\rho_\lambda$ are isomorphic, but this is not in general the case; they're all continuous with respect to completely different and incompatible topologies, so they can't be.
 
 All this definition works pretty much verbatim if you change $\Q$ to a general number field $K$; then $S$ becomes a finite set of prime ideals of the integers of $K$.
 

FLT/for_mathlib/Coalgebra/Monoid.lean

@@ -131,9 +131,9 @@ end Coalgebra
 section Bialgebra
 
 /--
-An algebra homomorphism point is an algebra homorphism from `A` to `L` where `A` is an `R`-biagebra
+An algebra homomorphism point is an algebra homomorphism from `A` to `L` where `A` is an `R`-biagebra
 and `L` an `R`-algebra. We introduce this abbreviation is to prevent instance clashing when we put a
-monnoid structure on these algebra homomorphism points with convolution product.
+monoid structure on these algebra homomorphism points with convolution product.
 
 This confusion happens when `A` and `L` are the same where default multiplication is composition.
 -/

FLT/for_mathlib/HopfAlgebra/Basic.lean

@@ -14,10 +14,10 @@ import FLT.for_mathlib.Coalgebra.TensorProduct
 For an `R`-hopf algebra `A`, we prove in this file the following basic properties:
 - the antipodal map is anticommutative;
 - the antipodal map is unique linear map whose convolution inverse is the identity `𝟙 A`.
-  (Note that, confusingly, the indeity linear map `x ↦ x` is not acutally the unit in the monoid
+  (Note that, confusingly, the identity linear map `x ↦ x` is not actually the unit in the monoid
   structure of linear maps. See `for_mathlib/Coalgebra/Monoid.lean`)
 if we further assume `A` is commutative then
-- the `R`-algebra homorphisms from `A` to `L` has a group structure where multiplication is
+- the `R`-algebra homomorphisms from `A` to `L` has a group structure where multiplication is
   convolution, and inverse of `f `is `f ∘ antipode`
 - in particular, `antipode ∘ antipode = 1`
 -/

blueprint/src/chapter/ch02reductions.tex

@@ -1,7 +1,7 @@
 \chapter{First reductions of the problem.}
 
 \section{Overview}
-The proof of Fermat's Last Theorem is by contradiction. We assume that we have a counterexample $a^n+b^n=c^n$, and manipulate it until it satsfies the axioms of a ``Frey package''. From the Frey package we build a Frey curve -- an elliptic curve defined over the rationals. We then look at a certain representation of a Galois group coming from this elliptic curve, and finally using two very deep and independent theorems (one due to Mazur, the other due to Wiles) we show that this representation is neither reducible or irreducible, a contradiction.
+The proof of Fermat's Last Theorem is by contradiction. We assume that we have a counterexample $a^n+b^n=c^n$, and manipulate it until it satisfies the axioms of a ``Frey package''. From the Frey package we build a Frey curve -- an elliptic curve defined over the rationals. We then look at a certain representation of a Galois group coming from this elliptic curve, and finally using two very deep and independent theorems (one due to Mazur, the other due to Wiles) we show that this representation is neither reducible or irreducible, a contradiction.
 
 \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime}
 
@@ -100,7 +100,7 @@ \section{Galois representations and elliptic curves}\label{twopointfour}
   and if $n$ is a natural number, hen the group of $k$-automorphisms of $K$ acts on the additive abelian group $E(K)[n]$ of $n$-torsion points on the curve.
 \end{definition}
 
-If furthermore $n=p$ is prime, then $A[p]$ is naturally a vector space over the field $\Z/p\Z$, and thus it inherits the stucture of a mod $p$ representation of $G$. Applying this to the above situation, we deduce that if $E$ is an elliptic curve over $\Q$ then $\GQ$ acts on $E(\Qbar)[p]$ and this is the \emph{mod $p$ Galois representation} attached to the curve $E$.
+If furthermore $n=p$ is prime, then $A[p]$ is naturally a vector space over the field $\Z/p\Z$, and thus it inherits the structure of a mod $p$ representation of $G$. Applying this to the above situation, we deduce that if $E$ is an elliptic curve over $\Q$ then $\GQ$ acts on $E(\Qbar)[p]$ and this is the \emph{mod $p$ Galois representation} attached to the curve $E$.
 
 In the next section we apply this theory to an elliptic curve coming from a counterexample to Fermat's Last theorem.
 

blueprint/src/chapter/ch03frey.tex

@@ -8,7 +8,7 @@ \section{Overview}
 \section{The arithmetic of elliptic curves}
 
 We give an overview of the results we need, citing the literature for proofs. Everything here is
- standard, and mostof it dates back to the 1970s or before.
+ standard, and most of it dates back to the 1970s or before.
 
 \begin{theorem}\label{EllipticCurve.n_torsion_card}\lean{EllipticCurve.n_torsion_card}\notready
   Let $n$ be a positive integer, let $F$ be a separably closed

blueprint/src/chapter/ch04overview.tex

@@ -31,7 +31,7 @@ \section{Potential modularity.}
     \item A modularity lifting theorem.
 \end{itemize}
 
-Almost verything here dates back to the the 1980s or before.
+Almost everything here dates back to the the 1980s or before.
 The exception is the modularity lifting theorem, which we now state explicitly.
 
 \section{A modularity lifting theorem}
@@ -82,7 +82,7 @@ \section{A modularity lifting theorem}
 In the minimal case, the argument is the usual Taylor--Wiles trick, using refinements due to Kisin and others.
 \end{proof}
 
-Given this modularity lifting theorem, the strategy to show potential modularity of $\rho$ is to use Moret--Bailly to find an appropriate totally real field $F$, an auxilary prime $p$, and an auxiliary elliptic curve over $F$ whose mod $\ell$ Galois representation is $\rho$ and whose
+Given this modularity lifting theorem, the strategy to show potential modularity of $\rho$ is to use Moret--Bailly to find an appropriate totally real field $F$, an auxiliary prime $p$, and an auxiliary elliptic curve over $F$ whose mod $\ell$ Galois representation is $\rho$ and whose
 mod $p$ Galois representation is induced from a character. By converse theorems (for example)
 the mod $p$ Galois representation is associated to an automorphic representation of
 $\GL_2/F$ and hence by Jacquet--Langlands it is modular. Now we use the

blueprint/src/chapter/chtopbestiary.tex

@@ -9,7 +9,7 @@ \section{Results from class field theory}
 Let $K$ be a finite extension of $\Q_p$. We write $\widehat{\Z}$ for the profinite completion of $\Z$; it is isomorphic to $\prod_p\Z_p$ where $\Z_p$ is the $p$-adic integers and the product is over all primes.
 
 \begin{theorem}\label{maximal_unramified_extension_of_p-adic_field}\notready The maximal unramified extension $K^{un}$ in a given algebraic closure of $K$
-    is Galois over $K$ with Galois group ``canonically'' isomorphic to $\widehat{\Z}$ in two ways; one of these two isomorphisms identifies $1\in\widehat{\Z}$ with an arithmetic Frobenius (the endomorphism inducing $x\mapsto x^q$ on the residue field of $K^{un}$, where $q$ is the size of the residue field of $K$). The other identifies 1 with geometric Frobenius (defined to be the inverse of arithematic Frobenius).
+    is Galois over $K$ with Galois group ``canonically'' isomorphic to $\widehat{\Z}$ in two ways; one of these two isomorphisms identifies $1\in\widehat{\Z}$ with an arithmetic Frobenius (the endomorphism inducing $x\mapsto x^q$ on the residue field of $K^{un}$, where $q$ is the size of the residue field of $K$). The other identifies 1 with geometric Frobenius (defined to be the inverse of arithmetic Frobenius).
 \end{theorem}
 
 It is impossible to say which of the two canonical isomorphisms is ``the most canonical''; people working in different areas make different choices in order to locally minimise the number of minus signs in their results.

blueprint/src/chapter/global_langlands.tex

@@ -12,7 +12,7 @@ \section{Statement of the conjecture}
 
   An \emph{affine group scheme over $R$} is a group object in the category of affine schemes over $R$.
 
-  \begin{definition}\label{Hopf_algebra}\lean{TODO}% we have Hopf alegbras in mathlib
+  \begin{definition}\label{Hopf_algebra}\lean{TODO}% we have Hopf algebras in mathlib
 
     %%%%%%%%%%%%%%%%%%%