The maximal pro-p quotient of an absolute Galois group

For a field K, absoluteGaloisGroupProP p K is the maximal pro-p quotient of Mathlib's Field.absoluteGaloisGroup K. Its topology is the quotient topology. The quotient is again profinite and is pro-p, so it is the group on which local pro-p Galois cohomology and presentations are formulated.

@[reducible, inline]

abbrev TauCeti.absoluteGaloisGroupProP (p : ℕ) (K : Type u_1) [Field K] : Type u_1

The maximal pro-p quotient of the absolute Galois group of K.

Equations

• TauCeti.absoluteGaloisGroupProP p K = TauCeti.maximalProPQuotient p (Field.absoluteGaloisGroup K)

@[reducible, inline]

noncomputable abbrev TauCeti.absoluteGaloisGroupProPQuotientMap (p : ℕ) (K : Type u_1) [Field K] : Field.absoluteGaloisGroup K →ₜ* absoluteGaloisGroupProP p K

The canonical continuous quotient map from an absolute Galois group to its maximal pro-p quotient.

Equations

• TauCeti.absoluteGaloisGroupProPQuotientMap p K = TauCeti.ContinuousMonoidHom.quotientMk (TauCeti.proPKernel p (Field.absoluteGaloisGroup K))

theorem TauCeti.isProP_absoluteGaloisGroupProP (p : ℕ) (K : Type u_1) [Field K] : IsProP p (absoluteGaloisGroupProP p K)

The maximal pro-p quotient of an absolute Galois group is pro-p.