Research proof index

The quotient of a Hausdorff second countable unimodular group by a central normal closed subgroup is still unimodular.

The value of d chosen in proposition 2.6 -/ noncomputable def d (ε : ℝ) : ℕ := ⌊10 * ε⁻¹ ^ 4⌋₊ /- Proposition 2.7. Reformulated slightly in terms of the existence of a Finset whose elements have certain properties. As it stands the statement in the blueprint implicitly assumes that this Finset is nonempty. That might be true, but is rather annoying...

herbrand quotient of Lˣ is [L:K]

Let M be a representation of a finite cyclic group G. Suppose there are even and positive integers e and o with e even and o odd, such that Hᵉ(G,M) and Hᵒ(G,M) are both zero. Then Hⁿ(G,M) is zero for all n > 0.

Let M be a representation of a finite cyclic group G. Then the following square commutes coind₁'.obj M -------> coind₁'.obj M | | | | ↓ ↓ ind₁'.obj M -------> ind₁'.obj M The vertical maps are the canonical isomorphism ind₁'_iso_coind₁ and the horizontal maps are map₁ and map₂.

If σ generates H²(G,M) then the map H²(G,M) ⟶ H²(G,split σ) is zero.