Haar measure in different settings

I recently learned how to build a Haar measure on every locally compact group. It's a fact there is only one (up to positive scalar multiple) Haar measure on a locally compact group, and it's easy to see that Lie groups (which includes algebraic and finite groups) and all compact groups are locally compact, so they have a unique (up to scalar multiple) Haar measure, too.
But the Haar measure can be defined much easier for Lie groups, and it's even simpler for finite groups. I wanted to study the relation more directly than by the uniqueness proof one sees in the literature.
This text is intended to be read by anyone who is familiar with the notion of groups and measures. Maybe you will want to consult Wikipedia along the lines - I have included some links.

I give first a precise definition of Haar measure and a state its uniqueness on locally compact groups, then I compare the different types of topological groups I want to investigate, along with valid definitions of Haar measure.

Definition of Haar measure; Uniqueness

Recall that a (left) Haar measure on a topological group $G$ is a (left-)translation invariant measure $\mu$ that is finite on compact sets and not everywhere zero.
(Left-)Translation invariance means, that for all sets $U \subseteq G$ and elements $g \in G$ we have $\mu(U) = \mu(gU)$. This can of course be defined from the right side, too, but the left and the right Haar measure are not the same, in general. Groups whose left and right Haar measure coincide are called unimodular. Abelian locally compact groups are always unimodular.
A Haar measure is called normalized if it has total measure $\mu(G) = 1$.

Theorem: If there are two Haar measures $\mu,\ \nu$ on a topological group $G$, then $\mu = c\nu$ for some positive real constant $c \in \mathbb{R}$.

This can be proved by fuddling around with double integrals and using left translation invariance multiple times, see the literature referenced at the bottom of this post.

Comparision chart of groups I discuss

The case of arbitrary topological groups is discussed quickly: the example of infinite dimensional Banach space, which is not locally compact, and admits no Haar measure (which would be infinite Lebesgue measure).

Haar measure on a locally compact group

The basic idea is to define a left-translation-invariant content which will then yield, by standard measure theory, the Haar measure. This proof uses Tychonoff's theorem and therefore the Axiom of Choice. There exists a proof which doesn't use Axiom of Choice but it requires more analysis (the Kakutani fixed point theorem or some functional analysis) and can be found in the literature.

Take $A \subset G$ a nonempty compact subset of the group and $B \subset G$ a subset with nonempty interior (so $B$ contains some nonempty open set). Denote by $A : B$ the minimal $n \in \mathbb{N}$ such that there exists $\{g_i\}_{i=1}^n \subseteq G$ with $A \subset \bigcup_{i=1}^n g_i B$. The number $A : B$ is always finite because of $A$'s compactness. Denote by $\mathcal{N}$ the set of all neighbourhoods of the identity of $G$. For some $O \in \mathcal{N}$, define for compact sets $K$:
$! \lambda_O(K) := \dfrac{K : O}{A : O}.$
Then we have $0 \leq \lambda_O(K) \leq K : A$.
This $\lambda_O$ is almost a content, but it lacks additivity.

For each compact set $K \subseteq G$ define the interval $I_K := [0, K : A]$.
Now define the infinite product $\Xi := \prod I_K$, which is compact by Tychonoff's theorem. The elements of $\Xi$ are functions $\phi$ that assign each compact set $K$ a non-negative value below $K : A$. Our previously defined $\lambda_O$ are elements of $\Xi$ for all $O\in \mathcal{N}$.

Look at
$! \Lambda(O) := \{\lambda_{O'} \mid O' \subseteq O,\ O' \in\mathcal{N}\}$
for some $O \in \mathcal{N}$. For some family $\{O_i\}_{i=1}^n \subset \mathcal{N}$, we have
$! \Lambda\left( \bigcap_{i=1}^n O_i\right) \subset \bigcap_{i=1}^n \Lambda(O_i).$
where the left hand side is nonempty, therefore is the right hand side nonempty. Compactness of $\Xi$ tells us now that there exists some point in the intersection of the closures of the $\Lambda(O)$:
$! \exists \lambda \in \bigcap\{\overline{\Lambda(O)} \mid O \in \mathcal{N}\}.$
And I claim that this $\lambda$ is the left-invariant content we're looking for. Again, for the full proof I refer to the literature.

Haar measure on a compact group

Compact groups are all unimodular:
Define the modulus to be $\Delta_\mu(h) := \int_G gh^{-1} \mu(g)$. Then $G$ is unimodular iff $\Delta(G)=1$. For a compact group $G$, the continuous group homomorphism $\Delta_\mu$ has values in the additive group $\mathbb{R}_+^\times$, whose only compact subgroup is $1$.

More directly, one could, in analogy to finite groups, do this:
Take a left Haar measure $\mu$ and some open set $U \subset G$. Then, via compactness, there is a family $\{g_i\}_{i=1}^n \subseteq G$ such that $\bigcup_{i=1}^n Ug_i = G$. Define a measure $\nu(U):=\frac{1}{n} \sum_{i=1}^n \mu(Ug_i)$. This is clearly right-invariant and it's not hard to see that it coincides with $\mu$. The hard part is to check that $\nu$ is a well-defined measure.

One can prove existence of a Haar measure on a compact group with less effort than for an arbitrary locally compact group. A nice fact is, that there always exists a normalized Haar measure, since the volume of a compactum is finite and $\nu(U) := \frac{\mu(U)}{\mu(G)}$ defines a normalized Haar measure for every Haar measure $\mu$.

Haar measure on a Lie group

Lie groups are differential manifolds, so there is a top outer form $\omega \in \det(G) := \Omega^n(G) = \Lambda^n(\mathfrak{g}^\ast)$ for $\mathfrak{g}$ the Lie algebra of $G$ (the tangent space at the identity element; $n = dim_{\mathbb{R}}G$). You might call this form a scalar multiple of the determinant, since it's exactly that for the Lie groups $(\mathbb{R}^n,+)$. The determinant form can be integrated and this is the Haar measure for Lie groups.
The special case of $(\mathbb{R}^n,+)$ is just the Lebesgue measure.
The special case of $(Mat^{n\times n}(\mathbb{R}),+)$ is the Lebesgue measure divided by the absolute value of the determinant, so $\int f(A) d\mu(A) = \int f(A) \frac{1}{|\det(A)|} d \lambda(A)$ with $\lambda$ being the Lebesgue measure in $\mathbb{R}^{n^2}$.

Haar measure on a linear complex algebraic group

Linear complex algebraic groups are compact Lie groups, so the Haar measure is given explicitely by a differential form, it's unimodular and there is always a normalized Haar measure.

I included this case only to show how nice it behaves - almost like finite groups.

Of course, finite groups are linear complex algebraic groups, since finite sets are just a finite number of copies of $\mathbb{C}^0$, and linearity is no condition in this case. There are no chart intersections, thus no chart transformation condition has to be satisfied. But I think this is a rather counter-intuitive way to think of finite groups, and it's still amazing to see how many properties all linear complex algebraic groups share with them.

Haar measure on a finite group

Here we can just give every group element the weight $1/|G|$, since $|G|$ is finite. The formula $\mu(U) := \sum_{g \in U} 1/|G| = |U|/|G|$ for every subset $U \subset G$ defines a Haar measure.

The number $A : K$ for locally compact groups, defined above, corresponds to the smallest integer greater than $|A|/|K| = \mu(A)/\mu(K)$. Now one might understand the proof above a little bit better.

The "why"

So, whenever we have a formula for finite groups, where some averaging over the group is done, we can try to lift this formula to compact groups, Lie groups or even locally compact groups, using the integral instead the sum. One particular application is the definition of a translation-invariant hermitian form on the class functions, which is very useful in representation theory.

References

Simon Rubinstein-Salzedo : "On the Existence and Uniqueness of Invariant Measures on Locally Compact Groups" (2004) (where I have stolen the proof sketch parts in the general case)Dieudonné: Treatise on analysis II, where you can find another nice proof of existence & uniqueness of Haar measure on locally compact (sepeable, metrizable) groups. This can be found as DjVu in the 'net, but that requires some searching.