The short exact sequence 0 → ℤ → ℚ → ℚ/ℤ → 0

The inclusion of the integers into the rationals followed by reduction modulo 1, with ℚ/ℤ realized as the rational circle AddCircle (1 : ℚ), is a short exact sequence of ℤ-modules.

Main definitions

• ModuleCat.ratAddCircleShortComplex: the short complex ℤ → ℚ → ℚ/ℤ of ℤ-modules.

Main results

• ModuleCat.ratAddCircleShortComplex_shortExact: 0 → ℤ → ℚ → ℚ/ℤ → 0 is short exact.

@[reducible, inline]

abbrev ModuleCat.ratAddCircleShortComplex : CategoryTheory.ShortComplex (ModuleCat ℤ)

The short complex ℤ → ℚ → ℚ/ℤ of ℤ-modules, with ℚ/ℤ the rational circle AddCircle (1 : ℚ): the inclusion of the integers followed by reduction modulo 1.

Equations

• One or more equations did not get rendered due to their size.

theorem ModuleCat.ratAddCircleShortComplex_shortExact : ratAddCircleShortComplex.ShortExact

The sequence 0 → ℤ → ℚ → ℚ/ℤ → 0 of ℤ-modules is short exact.