Class formations at archimedean places

At a real place, the absolute Galois group of the completion has order two. Hence its finite normal layers are either trivial or the unique quadratic layer. Inflation identifies the second cohomology of that layer with the real Brauer group, and the normalized invariant takes its nonzero class to 1/2. At a complex place, the absolute Galois group is trivial and every finite normal layer is trivial.

In both cases, the resulting invariant agrees with infiniteInvMap after inflation into the Brauer group. Thus the constructions have the normalization required by the global sum of local invariants, rather than merely providing abstract class formations on the same coefficient module.

Main definitions

• TauCeti.ClassFieldTheory.infiniteClassFormationOfIsReal: the units class formation at a real infinite place.
• TauCeti.ClassFieldTheory.infiniteClassFormationOfIsComplex: the units class formation at a complex infinite place.
• TauCeti.ClassFieldTheory.infiniteClassFormation: the units class formation at any infinite place.

Main results

• TauCeti.ClassFieldTheory.infiniteClassFormationOfIsReal_inv: the real-place invariant agrees with the archimedean Brauer invariant after inflation.
• TauCeti.ClassFieldTheory.infiniteClassFormationOfIsComplex_inv: its invariant agrees with the archimedean Brauer invariant after inflation.
• TauCeti.ClassFieldTheory.infiniteClassFormationOfIsComplex_artinMap: every finite-layer Artin map at a complex place is zero.
• TauCeti.ClassFieldTheory.finite_absoluteGaloisGroup: the absolute Galois group of every infinite completion is finite.
• TauCeti.ClassFieldTheory.subsingleton_fieldAbsoluteGaloisGroup_of_isComplex, TauCeti.ClassFieldTheory.natCard_fieldAbsoluteGaloisGroup_of_isReal: Mathlib's absolute Galois group Gal(AlgebraicClosure K_w/K_w) is trivial at a complex place and of order two at a real place.
• TauCeti.ClassFieldTheory.sq_eq_one_fieldAbsoluteGaloisGroupAbelianization_of_isReal, TauCeti.ClassFieldTheory.eq_of_ne_one_fieldAbsoluteGaloisGroupAbelianization_of_isReal: at a real place every element of G_{K_w}^ab squares to 1, and any two nontrivial elements of it are equal.
• TauCeti.ClassFieldTheory.fieldAbsoluteGaloisGroup_apply_eq_inv_of_isReal: at a real place the nontrivial automorphism of AlgebraicClosure K_w inverts every root of unity.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §§1–4.
• J. S. Milne, Class Field Theory, Chapter VIII, §4.

theorem NumberField.InfinitePlace.natCard_absoluteGaloisGroup_of_isReal {K : Type u_1} [Field K] (w : InfinitePlace K) (hw : w.IsReal) : Nat.card (TauCeti.AbsoluteGaloisGroup w.Completion) = 2

The absolute Galois group of a real infinite completion has order two.

theorem TauCeti.ClassFieldTheory.subgroup_eq_bot_or_eq_top_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (U : Subgroup (AbsoluteGaloisGroup w.Completion)) : U = ⊥ ∨ U = ⊤

Every subgroup of the absolute Galois group of a real infinite completion is either trivial or the whole group.

noncomputable def TauCeti.ClassFieldTheory.realOpenNormalSubgroup {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : OpenNormalSubgroup (AbsoluteGaloisGroup w.Completion)

The trivial open normal subgroup of the two-element absolute Galois group at a real place.

@[simp]

theorem TauCeti.ClassFieldTheory.realOpenNormalSubgroup_toSubgroup {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : ↑(realOpenNormalSubgroup w hw).toOpenSubgroup = ⊥

theorem TauCeti.ClassFieldTheory.NormalLayer.top_eq_ground_or_eq_realLayer_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) : L.top = L.ground ∨ L = ofOpenNormal (realOpenNormalSubgroup w hw)

A finite normal layer over a real infinite completion is either trivial or the unique quadratic layer from the trivial subgroup to the full absolute Galois group.

theorem TauCeti.ClassFieldTheory.degree_realLayer {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : (NormalLayer.ofOpenNormal (realOpenNormalSubgroup w hw)).degree = 2

The unique nontrivial layer at a real place has degree two.

noncomputable def TauCeti.ClassFieldTheory.realLayerInv {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) : ↑(L.H (unitsFormation w.Completion) 2) →+ AddCircle 1

The invariant of a finite normal layer at a real place. It is zero on a trivial layer; on the unique quadratic layer it is the archimedean invariant after inflation into the Brauer group.

@[simp]

theorem TauCeti.ClassFieldTheory.realLayerInv_of_top_eq_ground {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) (hL : L.top = L.ground) : realLayerInv w hw L = 0

The invariant of a trivial real-place layer is zero.

@[simp]

theorem TauCeti.ClassFieldTheory.realLayerInv_realLayer {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : realLayerInv w hw (NormalLayer.ofOpenNormal (realOpenNormalSubgroup w hw)) = (infiniteInvMap w).comp (brInfl (realOpenNormalSubgroup w hw))

On the unique quadratic layer, realLayerInv is the archimedean Brauer invariant after inflation.

theorem TauCeti.ClassFieldTheory.realLayerInv_injective {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) : Function.Injective ⇑(realLayerInv w hw L)

The invariant on every finite normal layer at a real place is injective.

theorem TauCeti.ClassFieldTheory.range_realLayerInv {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) : Set.range ⇑(realLayerInv w hw L) = ↑(AddSubgroup.torsionBy (AddCircle 1) ↑L.degree)

The range of the invariant on a real-place layer is the torsion subgroup of order equal to the degree of that layer.

theorem TauCeti.ClassFieldTheory.realLayerInv_cohomologyRes {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) {small big : NormalLayer (AbsoluteGaloisGroup w.Completion)} (T : LayerRestriction small big) (x : ↑(big.H (unitsFormation w.Completion) 2)) : (realLayerInv w hw small) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes (unitsFormation w.Completion) 2)) x) = T.relativeDegree • (realLayerInv w hw big) x

Real-place invariants have the class-formation restriction law.

theorem TauCeti.ClassFieldTheory.realLayerInv_cohomologyInfl {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) {old new : NormalLayer (AbsoluteGaloisGroup w.Completion)} (T : LayerRefinement old new) (x : ↑(old.H (unitsFormation w.Completion) 2)) : (realLayerInv w hw new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (unitsFormation w.Completion) 2)) x) = (realLayerInv w hw old) x

Real-place invariants have the class-formation inflation law.

theorem TauCeti.ClassFieldTheory.realLayerInv_apply {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) (x : ↑(L.H (unitsFormation w.Completion) 2)) : (realLayerInv w hw L) x = if x = 0 then 0 else ↑(1 / 2)

The invariant at a real place is zero on zero and 1/2 on every nonzero finite-layer cohomology class.

theorem TauCeti.ClassFieldTheory.realLayerInv_conjugateCohomologyIso {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) (g : AbsoluteGaloisGroup w.Completion) (x : ↑(L.H (unitsFormation w.Completion) 2)) : (realLayerInv w hw (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso (unitsFormation w.Completion) g 2).hom) x) = (realLayerInv w hw L) x

Real-place invariants are unchanged by conjugating a finite normal layer.

noncomputable def TauCeti.ClassFieldTheory.infiniteClassFormationOfIsReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : ClassFormation (unitsFormation w.Completion)

The class formation at a real place. Its invariant on the unique nontrivial layer is the archimedean Brauer invariant after inflation, and it is zero on every trivial layer.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteClassFormationOfIsReal_inv_apply {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) (x : ↑(L.H (unitsFormation w.Completion) 2)) : ((infiniteClassFormationOfIsReal w hw).inv L) x = (realLayerInv w hw L) x

The invariant of the real-place class formation is realLayerInv.

theorem TauCeti.ClassFieldTheory.infiniteClassFormationOfIsReal_inv {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (V : OpenNormalSubgroup (AbsoluteGaloisGroup w.Completion)) (x : ↑((NormalLayer.ofOpenNormal V).H (unitsFormation w.Completion) 2)) : ((infiniteClassFormationOfIsReal w hw).inv (NormalLayer.ofOpenNormal V)) x = (infiniteInvMap w) ((brInfl V) x)

The invariant of the real-place class formation is the normalized archimedean Brauer invariant of the inflated class.

theorem TauCeti.ClassFieldTheory.subsingleton_absoluteGaloisGroup_of_isComplex {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) : Subsingleton (AbsoluteGaloisGroup w.Completion)

The absolute Galois group of a complex infinite completion is trivial.

instance TauCeti.ClassFieldTheory.finite_absoluteGaloisGroup {K : Type} [Field K] (w : NumberField.InfinitePlace K) : Finite (AbsoluteGaloisGroup w.Completion)

The absolute Galois group of an infinite completion is finite: it has order two at a real place and is trivial at a complex place.

noncomputable def TauCeti.ClassFieldTheory.infiniteClassFormationOfIsComplex {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) : ClassFormation (unitsFormation w.Completion)

The class formation at a complex place. The absolute Galois group of the completion is trivial, so the units formation carries the canonical class formation with zero invariant maps.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteClassFormationOfIsComplex_inv_apply {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) (x : ↑(L.H (unitsFormation w.Completion) 2)) : ((infiniteClassFormationOfIsComplex w hw).inv L) x = 0

The invariant of the complex-place class formation is zero on every layer.

theorem TauCeti.ClassFieldTheory.infiniteClassFormationOfIsComplex_inv {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) (V : OpenNormalSubgroup (AbsoluteGaloisGroup w.Completion)) (x : ↑((NormalLayer.ofOpenNormal V).H (unitsFormation w.Completion) 2)) : ((infiniteClassFormationOfIsComplex w hw).inv (NormalLayer.ofOpenNormal V)) x = (infiniteInvMap w) ((brInfl V) x)

The invariant of the complex-place class formation is the archimedean Brauer invariant of the inflated class. This is the complex-place specialization of the normalization required of infiniteClassFormation.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteClassFormationOfIsComplex_artinMap {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) (L : NormalLayer (AbsoluteGaloisGroup w.Completion)) : (infiniteClassFormationOfIsComplex w hw).artinMap L = 0

Every finite-layer Artin map of the complex-place class formation is zero.

noncomputable def TauCeti.ClassFieldTheory.infiniteClassFormation {K : Type} [Field K] (w : NumberField.InfinitePlace K) : ClassFormation (unitsFormation w.Completion)

The class formation at an infinite place. This selects the real or complex construction according to the type of the place.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteClassFormation_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : infiniteClassFormation w = infiniteClassFormationOfIsReal w hw

At a real place, infiniteClassFormation is the real-place construction.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteClassFormation_of_isComplex {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) : infiniteClassFormation w = infiniteClassFormationOfIsComplex w hw

At a complex place, infiniteClassFormation is the complex-place construction.

theorem TauCeti.ClassFieldTheory.infiniteClassFormation_inv {K : Type} [Field K] (w : NumberField.InfinitePlace K) (V : OpenNormalSubgroup (AbsoluteGaloisGroup w.Completion)) (x : ↑((NormalLayer.ofOpenNormal V).H (unitsFormation w.Completion) 2)) : ((infiniteClassFormation w).inv (NormalLayer.ofOpenNormal V)) x = (infiniteInvMap w) ((brInfl V) x)

The invariant of the archimedean class formation is the archimedean Brauer invariant after inflation, at both real and complex places.

Mathlib's absolute Galois group at an infinite place

theorem TauCeti.ClassFieldTheory.subsingleton_fieldAbsoluteGaloisGroup_of_isComplex {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) : Subsingleton (Field.absoluteGaloisGroup w.Completion)

At a complex place Gal(AlgebraicClosure K_w/K_w) is trivial.

theorem TauCeti.ClassFieldTheory.natCard_fieldAbsoluteGaloisGroup_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : Nat.card (Field.absoluteGaloisGroup w.Completion) = 2

At a real place Gal(AlgebraicClosure K_w/K_w) has order two.

theorem TauCeti.ClassFieldTheory.eq_one_of_mk_eq_one_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) {σ : Field.absoluteGaloisGroup w.Completion} (hσ : ↑σ = 1) : σ = 1

At a real place an automorphism of AlgebraicClosure K_w with trivial class in G_{K_w}^ab is the identity: G_{K_w} has order two, so its closed commutator subgroup is trivial.

theorem TauCeti.ClassFieldTheory.sq_eq_one_fieldAbsoluteGaloisGroupAbelianization_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (y : Field.absoluteGaloisGroupAbelianization w.Completion) : y ^ 2 = 1

At a real place every element of G_{K_w}^ab squares to 1, since G_{K_w} has order two.

theorem TauCeti.ClassFieldTheory.eq_of_ne_one_fieldAbsoluteGaloisGroupAbelianization_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) {a b : Field.absoluteGaloisGroupAbelianization w.Completion} (ha : a ≠ 1) (hb : b ≠ 1) : a = b

At a real place any two nontrivial elements of G_{K_w}^ab are equal, since G_{K_w} has order two.

theorem TauCeti.ClassFieldTheory.mem_range_algebraMap_of_fieldAbsoluteGaloisGroup_apply_eq_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) {σ : Gal(AlgebraicClosure w.Completion/w.Completion)} (hσ : σ ≠ 1) {y : AlgebraicClosure w.Completion} (hy : σ y = y) : y ∈ Set.range ⇑(algebraMap w.Completion (AlgebraicClosure w.Completion))

At a real place an element of AlgebraicClosure K_w fixed by a nontrivial automorphism lies in K_w: that automorphism and the identity are all of G_{K_w}, which has order two.

theorem TauCeti.ClassFieldTheory.fieldAbsoluteGaloisGroup_apply_eq_inv_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) {σ : Gal(AlgebraicClosure w.Completion/w.Completion)} (hσ : σ ≠ 1) {m : ℕ} (hm : m ≠ 0) {z : AlgebraicClosure w.Completion} (hz : z ^ m = 1) : σ z = z⁻¹

At a real place a nontrivial automorphism of AlgebraicClosure K_w inverts every root of unity: writing z = a + b i with a, b ∈ K_w, the product z σ(z) = a² + b² is a nonnegative root of unity in K_w ≅ ℝ, hence 1.