## A short tutorial on Tietze transformations

Here is a little tutorial on how to use Tietze transformations. They were named after Austrian mathematician Heinrich Franz Friedrich Tietze.

A presentation is a set of generators and relations given by the notation
$$\langle~ S~|~W~\rangle$$ where $S$ is set and $W$ is a set of words in the symbols of $S$. $S$ is called the set of generators and $W$ is called the set of relations or relators. For example,
$$\langle~ r,s~|~rsr^{-1}s^{-1}~\rangle.$$ The group $G$ given by such a presentation is the quotient of the free group $F$ on $S$ by the normal closure of the set $W$ in $F$. In our example, $G\cong \Z\times\Z$. Sometimes we may abuse notation and write something like $xy = x^2$ instead of $xyx^{-2}$ in the set $W$.

We may be given two presentations such as:
$$\langle~ x,y~|~xyx=yxy~\rangle\\ \langle~ a,b~|~a^3 = b^2~\rangle$$ and we need to know whether the corresponding groups are isomorphic. To do this, we can perform a set of moves or steps, transforming each presentation into a new presentation whose group is isomorphic to the group of the previous.

There are two basic types of transformation: adding or removing generators, and adding or removing relations:
…read the rest of this post!

## On the Lean proof assistant, Part 1

A long time ago I became interested in proof assistants. I tried Isabelle and Coq for sure and I might have tried Mizar. Here, ‘try’ could mean tried to install and failed. Some of them worked, but I quickly gave up using them. In all of them the documentation was bad and I couldn’t figure out out to prove anything.

A while ago I heard about Lean. According to the official website,

Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.

A proof assistant is a program in which you type mathematics in a formal language and the computer checks every step using basic rules. Theoretically, such assistants may also aid in proving things, rather than just checking for correctness.
…read the rest of this post!

## List: groups up to order 15 with proofs

One of the prime goals after any mathematical structure is defined is to classify all possible structures up to isomorphism. Here, we will do something a little more modest: classify all finite groups up to order fifteen. Despite spending a great amount of time with groups, I’ve never actually done this formally, although I’ve certainly worked with many of them in random examples. So, I thought it might be fun to actually write them down.…read the rest of this post!

## Is Aut(GxH) = Aut(G)xAut(H) for groups G, H?

Let $G$ be a group. The automorphism group of $G$ is the group of all isomorphisms $G\to G$. We denote this group by ${\rm Aut}(G)$. Is it necessarily true that ${\rm Aut}(G\times H) \cong {\rm Aut}(G)\times {\rm Aut}(H)$?

Suppose $G$ and $H$ are finite groups whose orders are coprime. Then any homomorphism $f:G\to H$ must be trivial because for any $g\in G$, the element $f(g)$ has order dividing the order of $H$, but also dividing the order of $G$. Thus $f(g) = 1\in H$ where $1\in H$ is the group identity.

That means that any homomorphism $G\times H\to G\times H$ can be factored as a homomorphism $(f_G,f_H)$ where $f_G:G\to G$ and $f_H:H\to H$ are homomorphisms. Thus, if $G$ and $H$ are finite groups of coprime order, then ${\rm Aut}(G\times H) \cong {\rm Aut}(G)\times{\rm Aut}(H)$. Try working this out directly with $\Z/6\cong\Z/2\times\Z/3$.

Of course, this result does not hold in general. For example, an automorphism $\Z/2\times\Z/2\to\Z/2\times\Z/2$ is just a linear isomorphism of vector spaces, and so ${\rm Aut}(\Z/2\times\Z/2)\cong {\rm GL}_2(\Z/2)$. Incidentally, the latter is actually isomorphic to the symmetric group $S_3$ of permutations on three symbols.

## The nonvanishing K_2(Z/4)

We saw previously that $K_2(F) = 0$ for a finite field $F$, where $K_2$ is the second $K$-group of $F$. It may be helpful to refer to that post for the definitions of this functor.

I thought that it might be disappointing because we did all that work to compute the second $K$-group of a finite field and it turned out to be zero! But now we will see something a little more interesting: a ring with nonzero $K_2$.…read the rest of this post!

## The K-theory of finite fields: a synopsis

In my previous post, I proved that if $F$ is a finite field, then multiplicative group $F^\times$ is a cyclic group. This fact will play a small part in our description today of the $K$-theory of $F$. We will start by describing the classical $K$-theory of $F$ and then briefly talk about Quillen’s computation of all the higher $K$-groups of $F$.

Classical here means the first three $K$-functors: $K_0, K_1,$ and $K_2$. These are the functors that can be described algebraically and were studied before Daniel Quillen wrote down the definitions of the higher $K$-functors using topology (technically though, one does not need to use topology to define higher $K$-theory, as one can use acyclic binary multicomplexes due to Nenashev for $K_1$ and due to Dan Grayson in general. See [1]).…read the rest of this post!

## The multiplicative group of a finite field is cyclic

Today, we are going to prove that if $F$ is a finite field, the the multiplicative group $F^\times$ of $F$ is a cyclic group. Let’s start with an example of this phenomenon. Take $\F_5 = \{0,1,2,3,4\}$. Now, if we take powers of $2$ modulo $5$ we get
$$2,2^2=4,2^3 = 3, 2^4 = 1.$$ Therefore, we see that $2$ generates $\F_5^\times$. In other words, $\F_5^\times\cong \Z/4$. In general, we have
$$F_{p^n}^\times\cong\Z/(p^n-1).$$…read the rest of this post!

## Binomial logistic regression models in R

In this post, we will look at a simple logistic binomial regression model in R. First, let’s take a look at the following hypothetical data taken from [1]:

 C = Yes C = No Disease Disease Yes No Yes No Exposure Yes 1200 600 300 400 No 400 100 600 400

It is a contingency table. With this data we want to predict the probability of getting a disease based on exposure. We assume that some people are exposed to something (not necessarily the disease itself), and we count the number of people that get the disease. The exposure could be something good like an experimental treatment of “exercises at least twenty minutes a week on a treadmill” and the disease could be “heart disease”. Notice that there is a second variable, “C” that we could also incorporate into our model. To get this data into R it is easiest to have it in a comma separate file like this:…read the rest of this post!

## Chytrid fungus and logistic regression against temperature

Chytrid fungus refers to the fungus Batrachochytrium dendrobatidis (Bd). In amphibians, it causes a disease known as Chytridiomycosis. It is one of the worst diseases to strike out at multiple species of animals on the planet. This horrible disease degrades the skin, which in amphibians is a sensitive, permeable organ that is part of the respiratory system. Chytridiomycosis eventually leads to death and is a serious threat to many amphibian species in areas such as North America, Central America, Asia, Africa, and even in Australia.

While not necessarily threatened with extinction by Chytrid fungus, even Northern Leopard Frogs may be affected by the widespread organism. Photo by Jason Polak.

As humans, we have contributed to the spread of Chytrid. For example, the bullfrog Lithobates catesbeianus is an excellent reservoir of Bd and has been associated with increased presence of the bacteria in areas where it has become an invasive species due to imports for food. Chytrid fungus has also been responsible for huge losses and declines of frog species in Panama.

Bd grows between 4-25 C°. Therefore, we expect to see a decrease in prevalence in Bd infections in species in the wild as the temperature of the water rises. Matthew Forrest and Martin Schlaepfer tested this and modeled the presence or absence of a Bd infection against water temperature using binomial logistic regression. In their sample of 201 Lowland Leopard frogs, they grouped 10-12 individuals and plotted the proportion of individuals with Bd to illustrate their model:

Logistic equation model reproduced from Forrest and Schlaepfer.

The curve is their logistic regression equation, which is
$$p = \frac{1}{1+e^{4.56-0.226t}}$$ where $t$ is the temperature in Celsius, and $p$ is the proportion of individuals with Bd. This is just one example of the steps we need to take towards better understanding the ecology of the Bd organism so that we can better prevent it from eradicating beautiful species of amphibians that are integral parts of our biosphere.