The cohomological Brauer invariant of the reals

This file computes Br ℝ, the continuous-cohomology Brauer group used by class formations, via H²(Gal(ℂ/ℝ), ℂˣ). The cyclic norm quotient for ℂ/ℝ is the real sign quotient, so Br ℝ ≃+ ZMod 2. The real invariant embeds it in ℚ/ℤ, sending its nonzero class to 1/2.

realClass carries a real unit to its cyclic class at complex conjugation. Positive units represent zero, and negative units represent the unique nonzero class. This characterizes the normalization without any choice of a generator beyond complex conjugation.

The comparison with relative cohomology uses an identification of a separable closure of ℝ with ℂ. The invariant itself is independent of that identification: realInv_apply describes it solely by whether a Brauer class is zero. The complex Brauer group is trivial by the general subsingleton_Br_of_isSepClosed instance and Complex.isAlgClosed.

Main definitions and results

• realBrEquivRelative: comparison with the relative cohomology of ℂ/ℝ.
• realInvEquiv: the identification Br ℝ ≃+ ZMod 2.
• realInv: the injective real invariant with two-torsion image in ℚ/ℤ.
• realInv_realClass: the invariant of a real cyclic class, zero or 1/2 according to sign.

References

• J.-P. Serre, Local Fields, Chapter XIII, §1.

noncomputable def TauCeti.ClassFieldTheory.realBrEquivRelative : Br ℝ ≃+ ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(ℂ/ℝ) ℂˣ))

The continuous-cohomology Brauer group of ℝ agrees with the relative cohomology of ℂ/ℝ, using an identification of the separable closure with ℂ.

The group is finite, so its Krull topology is discrete. The coefficient topology on ℂˣ used in the comparison is discrete, as required for Galois cohomology.

noncomputable def TauCeti.ClassFieldTheory.realClass : Additive ℝˣ →+ Br ℝ

The cyclic class of a real unit, at complex conjugation, in the cohomological Brauer group.

@[simp]

theorem TauCeti.ClassFieldTheory.realBrEquivRelative_realClass (a : Additive ℝˣ) : realBrEquivRelative (realClass a) = (cyclicClass ⋯) a

The relative comparison sends a real cyclic class to the class at complex conjugation.

theorem TauCeti.ClassFieldTheory.realClass_surjective : Function.Surjective ⇑realClass

Every real Brauer class is represented by a real unit.

@[simp]

theorem TauCeti.ClassFieldTheory.realClass_eq_zero_iff (a : ℝˣ) : realClass (Additive.ofMul a) = 0 ↔ 0 < ↑a

A real cyclic class vanishes exactly when its representing unit is positive.

noncomputable def TauCeti.ClassFieldTheory.realInvEquiv : Br ℝ ≃+ ZMod 2

The real cohomological Brauer group is the two-element sign group.

noncomputable def TauCeti.ClassFieldTheory.realInv : Br ℝ →+ AddCircle 1

The real Brauer invariant, normalized to send the nonzero class to 1/2.

theorem TauCeti.ClassFieldTheory.realInv_injective : Function.Injective ⇑realInv

The real invariant detects every Brauer class.

theorem TauCeti.ClassFieldTheory.range_realInv : Set.range ⇑realInv = ↑(AddSubgroup.torsionBy (AddCircle 1) 2)

The image of the real invariant is exactly the two-torsion of ℚ/ℤ.

theorem TauCeti.ClassFieldTheory.realInv_apply (x : Br ℝ) : realInv x = if x = 0 then 0 else ↑(1 / 2)

The real invariant is intrinsically determined by whether the class vanishes.

@[simp]

theorem TauCeti.ClassFieldTheory.realInv_realClass (a : ℝˣ) : realInv (realClass (Additive.ofMul a)) = if 0 < ↑a then 0 else ↑(1 / 2)

Positive real cyclic classes have invariant zero, and negative ones have invariant 1/2.

@[simp]

theorem TauCeti.ClassFieldTheory.realInvEquiv_realClass (a : ℝˣ) : realInvEquiv (realClass (Additive.ofMul a)) = if 0 < ↑a then 0 else 1

The real invariant coordinates send a positive cyclic class to zero and a negative one to one.