The Brauer group as continuous cohomology, and its finite layers

For a field F with absolute Galois group G_F = Field.absoluteGaloisGroup F, this file defines the coefficient object unitsRep F of the units (Fˢ)ˣ of a separable closure, written additively, and the Brauer group

Br F = H²(G_F, (Fˢ)ˣ)

on Mathlib's continuous cohomology continuousCohomology, the carrier on which the local invariant is to be defined. The group G_F acts on (Fˢ)ˣ through the restriction isomorphism TauCeti.absoluteGaloisGroupRestrictEquiv : G_F ≃ₜ* Gal(Fˢ/F), exactly as for the roots of unity TauCeti.ClassFieldTheory.muNRep, and unitsRepH2Equiv identifies Br F with the explicit H²(Gal(Fˢ/F), (Fˢ)ˣ) of TauCeti.UnitsCoeff F, the group whose n-torsion is described by TauCeti.h2KummerToUnits_range.

The Brauer group is the union of its finite layers. For an open normal subgroup U of Gal(Fˢ/F), brLevelInfl U is inflation H²(Gal(Fˢ/F) ⧸ U, ((Fˢ)ˣ)^U) → Br F. Every Brauer class is inflated from some level (exists_brLevelInfl_eq), and, by Hilbert 90 for U, each inflation is injective (brLevelInfl_injective). For a finite normal extension L/K embedded in Kˢ by σ, the level of Gal(Kˢ/σ(L)) is identified with Mathlib's group cohomology H²(Gal(L/K), Lˣ) of the relative Brauer group (relBrLevelEquiv), which gives the injection relBrInfl K L σ : H²(Gal(L/K), Lˣ) → Br K; every Brauer class comes from a finite Galois subextension of Kˢ (exists_relBrInfl_eq), and these inflations are compatible with towers K ⊆ L ⊆ M (relBrInfl_map). A class inflated from a finite normal E/K is inflated from another one L/K exactly when its restriction to L vanishes, the restriction being computed in any finite normal M/K in Kˢ containing both (relBrInfl_mem_range_relBrInfl_iff). This finite-layer description is what an invariant defined on the finite layers, such as the unramified invariant TauCeti.ClassFieldTheory.unramifiedInv on H²(Gal(L/K), Lˣ), has to be carried along to reach Br K.

Br F is the cohomological Brauer group. Its comparison with the Brauer group BrauerGroup F of central simple algebras is not made here.

Implementation notes

relBrLevelEquiv compares with Mathlib's groupCohomology, whose comparison with the explicit model, TauCeti.ContCohomology.explicitH2IsoGroupCohomology, asks for the group and the module in Type; the fields K and L of the relative statements therefore live in Type, as do those of TauCeti.ClassFieldTheory.unramifiedInv. The level TauCeti.galoisOpenNormalSubgroup K L σ has underlying subgroup the fixing subgroup of σ(L) by definition, which is what lets relBrLevelEquiv pass between the two descriptions of the same quotient and invariants.

Main definitions

• TauCeti.ClassFieldTheory.unitsRep F: the units (Fˢ)ˣ as a coefficient object for G_F.
• TauCeti.ClassFieldTheory.Br F: the Brauer group H²(G_F, (Fˢ)ˣ).
• TauCeti.ClassFieldTheory.unitsRepH2Equiv: H²(Gal(Fˢ/F), (Fˢ)ˣ) ≃+ Br F.
• TauCeti.ClassFieldTheory.subsingleton_Br_of_isSepClosed: the Brauer group of a separably closed field is trivial.
• TauCeti.ClassFieldTheory.brLevelInfl: inflation from the level of an open normal subgroup.
• TauCeti.ClassFieldTheory.relBrLevelEquiv: H²(Gal(L/K), Lˣ) as the level of the subgroup fixing σ(L).
• TauCeti.ClassFieldTheory.relBrInfl: inflation H²(Gal(L/K), Lˣ) → Br K.
• TauCeti.ClassFieldTheory.relBrCocycle: the cocycle on G_K obtained from a relative Brauer cocycle, with relBrInfl_H2π identifying its class with relBrInfl; conversely, a cocycle on G_K read off Gal(L/K) with values in σ(Lˣ) is one of them (exists_relBrCocycle_eq).

Main results

• TauCeti.ClassFieldTheory.brLevelInfl_injective, TauCeti.ClassFieldTheory.relBrInfl_injective: inflation into the Brauer group is injective.
• TauCeti.ClassFieldTheory.exists_brLevelInfl_eq, TauCeti.ClassFieldTheory.exists_relBrInfl_eq: every Brauer class is inflated from a finite layer.
• TauCeti.ClassFieldTheory.brLevelInfl_explicitFiniteQuotientTransition2: inflations from different levels are compatible.
• TauCeti.ClassFieldTheory.relBrInfl_map: inflation from H²(Gal(L/K), Lˣ) into Br K factors through inflation to H²(Gal(M/K), Mˣ) for every finite normal M ⊇ L.
• TauCeti.ClassFieldTheory.relBrInfl_mem_range_relBrInfl_iff: a Brauer class split by E is split by L exactly when its restriction to L vanishes.

References

• J.-P. Serre, Local Fields, Chapter X, §4 and §5.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (6.3.4).

The coefficient object (Fˢ)ˣ and the Brauer group

noncomputable def TauCeti.ClassFieldTheory.unitsRep (F : Type u) [Field F] : TopRep ℤ (Field.absoluteGaloisGroup F)

The units (Fˢ)ˣ of a separable closure, written additively, as a coefficient object. An automorphism of the algebraic closure acts through its restriction to the separable closure, TauCeti.absoluteGaloisGroupRestrictEquiv; unitsCoeffEquivUnitsRep identifies the underlying module with TauCeti.UnitsCoeff F.

instance TauCeti.ClassFieldTheory.instDiscreteTopologyVIntAbsoluteGaloisGroupUnitsRep (F : Type u) [Field F] : DiscreteTopology ↑(unitsRep F)

(Fˢ)ˣ carries the discrete topology.

noncomputable def TauCeti.ClassFieldTheory.unitsCoeffEquivUnitsRep (F : Type u) [Field F] : UnitsCoeff F ≃+ ↑(unitsRep F)

The coefficient dictionary between TauCeti.UnitsCoeff F, a module for Gal(Fˢ/F), and the underlying module of unitsRep F. It is equivariant along the restriction isomorphism by unitsCoeffEquivUnitsRep_smul.

@[simp]

theorem TauCeti.ClassFieldTheory.unitsCoeffEquivUnitsRep_smul (F : Type u) [Field F] (g : Field.absoluteGaloisGroup F) (x : UnitsCoeff F) : (unitsCoeffEquivUnitsRep F) ((absoluteGaloisGroupRestrictEquiv F) g • x) = ((unitsRep F).ρ g) ((unitsCoeffEquivUnitsRep F) x)

The coefficient dictionary is equivariant: σ ∈ G_F acts on unitsRep F as its restriction to the separable closure acts on TauCeti.UnitsCoeff F.

theorem TauCeti.ClassFieldTheory.isSmoothDiscrete_unitsRep (F : Type u) [Field F] : IsSmoothDiscrete ℤ (unitsRep F)

(Fˢ)ˣ is a smooth discrete coefficient object: the stabilizer of a unit is the preimage, under the restriction isomorphism, of its open stabilizer in Gal(Fˢ/F).

instance TauCeti.ClassFieldTheory.instContinuousSMulAbsoluteGaloisGroupVIntUnitsRep (F : Type u) [Field F] : ContinuousSMul (Field.absoluteGaloisGroup F) ↑(unitsRep F)

The action of G_F on (Fˢ)ˣ is continuous, (Fˢ)ˣ being smooth discrete.

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.Br (F : Type u) [Field F] : Type u

The Brauer group Br F = H²(G_F, (Fˢ)ˣ), on Mathlib's continuous cohomology.

noncomputable def TauCeti.ClassFieldTheory.unitsRepH2Equiv (F : Type u) [Field F] : ContCohomology.H2 (AbsoluteGaloisGroup F) (UnitsCoeff F) ≃+ Br F

H² of (Fˢ)ˣ over Gal(Fˢ/F) is the Brauer group: pullback along the restriction isomorphism G_F ≃ Gal(Fˢ/F) and the coefficient dictionary, followed by the degree-two comparison of explicit and canonical continuous cohomology for the discrete object unitsRep F.

instance TauCeti.ClassFieldTheory.subsingleton_Br_of_isSepClosed (F : Type u) [Field F] [IsSepClosed F] : Subsingleton (Br F)

A separably closed field has trivial cohomological Brauer group.

theorem TauCeti.ClassFieldTheory.unitsRepH2Equiv_apply (F : Type u) [Field F] (x : ContCohomology.H2 (AbsoluteGaloisGroup F) (UnitsCoeff F)) : (unitsRepH2Equiv F) x = (unitsRep F).explicitH2AddEquivContinuousCohomologyOfDiscrete ((ContCohomology.explicitMap2 (AbsoluteGaloisGroup F) (UnitsCoeff F) (Field.absoluteGaloisGroup F) (↑(unitsRep F)) (↑(absoluteGaloisGroupRestrictEquiv F)) (unitsCoeffEquivUnitsRep F).toAddMonoidHom ⋯ ⋯) x)

unitsRepH2Equiv is the pullback along the restriction isomorphism and the coefficient dictionary, followed by the degree-two comparison for the discrete object unitsRep F.

Inflation from the finite levels

noncomputable def TauCeti.ClassFieldTheory.brLevelInfl {F : Type u} [Field F] (U : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : ContCohomology.H2 (AbsoluteGaloisGroup F ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) (UnitsCoeff F)) →+ Br F

Inflation from a finite level into the Brauer group: for an open normal subgroup U of Gal(Fˢ/F), inflation H²(Gal(Fˢ/F) ⧸ U, ((Fˢ)ˣ)^U) → H²(Gal(Fˢ/F), (Fˢ)ˣ) followed by unitsRepH2Equiv. It is injective (brLevelInfl_injective) and every Brauer class lies in the image of some level (exists_brLevelInfl_eq).

theorem TauCeti.ClassFieldTheory.brLevelInfl_apply {F : Type u} [Field F] (U : OpenNormalSubgroup (AbsoluteGaloisGroup F)) (y : ContCohomology.H2 (AbsoluteGaloisGroup F ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) (UnitsCoeff F))) : (brLevelInfl U) y = (unitsRepH2Equiv F) ((ContCohomology.explicitInfl2 (AbsoluteGaloisGroup F) (UnitsCoeff F) ↑U.toOpenSubgroup) y)

brLevelInfl U is explicit inflation followed by unitsRepH2Equiv.

theorem TauCeti.ClassFieldTheory.brLevelInfl_injective {F : Type u} [Field F] (U : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : Function.Injective ⇑(brLevelInfl U)

Inflation from a finite level into the Brauer group is injective, by Hilbert 90 for the open subgroup U (TauCeti.explicitInfl2_unitsCoeff_injective).

theorem TauCeti.ClassFieldTheory.exists_brLevelInfl_eq {F : Type u} [Field F] (x : Br F) : ∃ (U : OpenNormalSubgroup (AbsoluteGaloisGroup F)) (y : ContCohomology.H2 (AbsoluteGaloisGroup F ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) (UnitsCoeff F))), (brLevelInfl U) y = x

Every Brauer class is inflated from a finite level, by strict descent of continuous 2-cocycles to a finite quotient (TauCeti.ContCohomology.exists_explicitInfl2_eq).

theorem TauCeti.ClassFieldTheory.brLevelInfl_explicitFiniteQuotientTransition2 {F : Type u} [Field F] {U V : OpenNormalSubgroup (AbsoluteGaloisGroup F)} (hVU : V ≤ U) (y : ContCohomology.H2 (AbsoluteGaloisGroup F ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) (UnitsCoeff F))) : (brLevelInfl V) ((ContCohomology.explicitFiniteQuotientTransition2 (AbsoluteGaloisGroup F) (UnitsCoeff F) U V hVU) y) = (brLevelInfl U) y

Inflations from different levels are compatible: for open normal subgroups V ≤ U, inflating from the U-level through the V-level is inflating from the U-level directly.

The relative Brauer group of a finite normal extension

noncomputable def TauCeti.ClassFieldTheory.relBrLevelEquiv (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (σ : L →ₐ[K] SeparableClosure K) : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2) ≃+ ContCohomology.H2 (AbsoluteGaloisGroup K ⧸ ↑(galoisOpenNormalSubgroup K L σ).toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑(galoisOpenNormalSubgroup K L σ).toOpenSubgroup) (UnitsCoeff K))

The relative Brauer group H²(Gal(L/K), Lˣ) is the level of Gal(Kˢ/σ(L)): Mathlib's group cohomology of Lˣ is carried by quotientFixingSubgroupFieldRangeEquiv and TauCeti.embeddedUnitsEquivInvariants to that of ((Kˢ)ˣ)^U over Gal(Kˢ/K) ⧸ U, for U = galoisOpenNormalSubgroup K L σ, which is the explicit H² of this discrete finite level by TauCeti.ContCohomology.explicitH2IsoGroupCohomology.

noncomputable def TauCeti.ClassFieldTheory.relBrInfl (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (σ : L →ₐ[K] SeparableClosure K) : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2) →+ Br K

Inflation from the relative Brauer group H²(Gal(L/K), Lˣ) → Br K of a finite normal extension L/K embedded in Kˢ by σ: the identification relBrLevelEquiv of H²(Gal(L/K), Lˣ) with the level of Gal(Kˢ/σ(L)), followed by brLevelInfl.

theorem TauCeti.ClassFieldTheory.relBrInfl_apply (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (σ : L →ₐ[K] SeparableClosure K) (x : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2)) : (relBrInfl K L σ) x = (brLevelInfl (galoisOpenNormalSubgroup K L σ)) ((relBrLevelEquiv K L σ) x)

relBrInfl K L σ is brLevelInfl after the identification relBrLevelEquiv.

theorem TauCeti.ClassFieldTheory.relBrInfl_injective (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (σ : L →ₐ[K] SeparableClosure K) : Function.Injective ⇑(relBrInfl K L σ)

H²(Gal(L/K), Lˣ) injects into the Brauer group of K.

theorem TauCeti.ClassFieldTheory.exists_relBrInfl_eq {K : Type} [Field K] (x : Br K) : ∃ (E : IntermediateField K (SeparableClosure K)) (x_1 : FiniteDimensional K ↥E) (x_2 : Normal K ↥E) (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(↥E/K) (↥E)ˣ) 2)), (relBrInfl K (↥E) E.val) y = x

Every Brauer class splits over a finite Galois subextension of Kˢ: it is inflated from H²(Gal(E/K), Eˣ) for some intermediate field E of Kˢ/K, finite and normal over K.

noncomputable def TauCeti.ClassFieldTheory.relBrCocycle (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (σ : L →ₐ[K] SeparableClosure K) (c : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) : ↥(ContCohomology.Z2 (AbsoluteGaloisGroup K) (UnitsCoeff K))

The cocycle on G_K attached to a relative Brauer cocycle. If c : Z²(Gal(L/K), Lˣ), then relBrCocycle K L σ c is the cocycle

(g, h) ↦ σ (c (g|_L, h|_L))

on the absolute Galois group, with multiplicative coefficients written additively. Its class is the inflation relBrInfl K L σ [c] (relBrInfl_H2π).

@[simp]

theorem TauCeti.ClassFieldTheory.relBrCocycle_apply (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (σ : L →ₐ[K] SeparableClosure K) (c : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) (g h : AbsoluteGaloisGroup K) : ↑(relBrCocycle K L σ c) (g, h) = ↑((embeddedUnitsEquivInvariants K L σ) (Rep.toAdditive (c (σ.restrictNormalHom g, σ.restrictNormalHom h))))

The value of the relative Brauer cocycle is the embedded value of the original cocycle at the restrictions of the two absolute Galois elements.

@[simp]

theorem TauCeti.ClassFieldTheory.relBrInfl_H2π (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (σ : L →ₐ[K] SeparableClosure K) (c : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) : (relBrInfl K L σ) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) c) = (unitsRepH2Equiv K) ↑(relBrCocycle K L σ c)

Relative inflation on cocycle classes. The image under relBrInfl of the class of a relative cocycle c is the Brauer class represented by relBrCocycle K L σ c.

theorem TauCeti.ClassFieldTheory.exists_relBrCocycle_eq (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (σ : L →ₐ[K] SeparableClosure K) (z : ↥(ContCohomology.Z2 (AbsoluteGaloisGroup K) (UnitsCoeff K))) (u : Gal(L/K) × Gal(L/K) → Lˣ) (hz : ∀ (g h : AbsoluteGaloisGroup K), ↑z (g, h) = ↑((embeddedUnitsEquivInvariants K L σ) (Additive.ofMul (u (σ.restrictNormalHom g, σ.restrictNormalHom h))))) : ∃ (c : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))), (∀ (p : Gal(L/K) × Gal(L/K)), Additive.toMul (Rep.toAdditive (c p)) = u p) ∧ relBrCocycle K L σ c = z

A cocycle on G_K read off Gal(L/K) is a relative Brauer cocycle. If a continuous 2-cocycle z on G_K with values in (Kˢ)ˣ takes at (g, h) the value σ (u (g|_L, h|_L)) for some function u on Gal(L/K) × Gal(L/K) with values in Lˣ, then u is a 2-cocycle c and z = relBrCocycle K L σ c, so that the class of z is relBrInfl K L σ [c] (relBrInfl_H2π).

@[simp]

theorem TauCeti.ClassFieldTheory.relBrInfl_map (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (M : Type) [Field M] [Algebra K M] [FiniteDimensional K M] [Normal K M] [Algebra L M] [IsScalarTower K L M] (τ : M →ₐ[K] SeparableClosure K) (x : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2)) : (relBrInfl K M τ) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (AlgEquiv.restrictNormalHom L) (unitsInflationHom K L M) 2)) x) = (relBrInfl K L (τ.comp (IsScalarTower.toAlgHom K L M))) x

Inflation into the Brauer group is compatible with towers. For finite normal extensions K ⊆ L ⊆ M with M embedded in Kˢ by τ, inflating a class of H²(Gal(L/K), Lˣ) to H²(Gal(M/K), Mˣ) and then into Br K is inflating it into Br K directly, L being embedded by the restriction of τ.

theorem TauCeti.ClassFieldTheory.relBrInfl_mem_range_relBrInfl_iff (K : Type) [Field K] (E L M : Type) [Field E] [Field L] [Field M] [Algebra K E] [Algebra K L] [Algebra K M] [Algebra E M] [Algebra L M] [IsScalarTower K E M] [IsScalarTower K L M] [FiniteDimensional K E] [FiniteDimensional K L] [FiniteDimensional K M] [Normal K E] [Normal K L] [Normal K M] (ρ : M →ₐ[K] SeparableClosure K) (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(E/K) Eˣ) 2)) : (relBrInfl K E (ρ.comp (IsScalarTower.toAlgHom K E M))) y ∈ (relBrInfl K L (ρ.comp (IsScalarTower.toAlgHom K L M))).range ↔ (CategoryTheory.ConcreteCategory.hom (groupCohomology.map ((AlgEquiv.restrictNormalHom E).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K E L M) 2)) y = 0

A Brauer class is split by L exactly when its restriction to L vanishes. Let E and L be finite normal extensions of K inside a finite normal extension M embedded in Kˢ by ρ. A class of Br K inflated from y ∈ H²(Gal(E/K), Eˣ) is inflated from H²(Gal(L/K), Lˣ) exactly when the base change of y to H²(Gal(M/L), Mˣ) vanishes.