The local invariant of an unramified layer

Let L/K be a finite unramified Galois extension of nonarchimedean local fields, of degree n, and let φ ∈ Gal(L/K) be its arithmetic Frobenius TauCeti.frobeniusAlgEquiv, which generates the cyclic group Gal(L/K). This file constructs the local invariant

inv_{L/K} : H²(Gal(L/K), Lˣ) → ℚ/ℤ

of the relative Brauer group of the layer, and proves that it is injective with image the subgroup of ℚ/ℤ of order n.

For a cyclic group generated by φ, the periodic resolution identifies H²(Gal(L/K), Lˣ) with the norm quotient Kˣ / N_{L/K}(Lˣ) (TauCeti.cyclicNormQuotientEquiv). Write TauCeti.ClassFieldTheory.unramifiedClass K L a for the class of a ∈ Kˣ under this identification at φ (TauCeti.cyclicClass). Classically, this is the cup product a ∪ δχ of a with the image under the connecting map δ : H¹(Gal(L/K), ℚ/ℤ) → H²(Gal(L/K), ℤ) of the character χ with χ(φ) = 1/n. The invariant is normalized by

inv_{L/K}(unramifiedClass a) = v_K(a) / n,

where v_K is the normalized valuation of K. This is well defined and injective exactly because, in an unramified extension, a is a norm if and only if n ∣ v_K(a) (TauCeti.mem_normGroup_iff_dvd_normalizedValuation). With this normalization a uniformizer of K has invariant 1/n, so its class is the fundamental class of the layer; replacing arithmetic by geometric Frobenius would negate every invariant.

The invariants of different unramified layers are compatible. For unramified layers K ⊆ L ⊆ M, arithmetic Frobenius of M/K restricts to that of L/K, and inflation H²(Gal(L/K), Lˣ) → H²(Gal(M/K), Mˣ) sends the class of a to the class of a ^ [M : L] (TauCeti.map_cyclicClass), whose invariant is again v_K(a) / n. So inflation preserves the invariant: this is the compatibility the invariants of the unramified layers need in order to glue to one invariant on the union of their images in the Brauer group of K.

The invariant also transforms along a change of ground field. Let K'/K be an extension of nonarchimedean local fields, and let L'/K' be an unramified layer containing L. The arithmetic Frobenius of L'/K' restricts to the f(K'/K)-th power of that of L/K, where f(K'/K) is the residue degree. The map H²(Gal(L/K), Lˣ) → H²(Gal(L'/K'), L'ˣ) induced by restriction Gal(L'/K') → Gal(L/K) therefore sends the class of a to the class of a ^ (f(K'/K) · [L' : K'] / [L : K]) (TauCeti.map_cyclicClass_baseChange). Its invariant is e(K'/K) f(K'/K) · v_K(a) / [L : K], because v_{K'}(a) = e(K'/K) · v_K(a). So this map multiplies the invariant by e(K'/K) f(K'/K) = [K' : K]: this is the formula inv_{K'} ∘ res = [K' : K] · inv_K for restriction of classes inflated from unramified layers.

Restriction to an intermediate ground field E in K ⊆ E ⊆ L is the specialization K' := E, L' := L of map_unramifiedClass_baseChange and unramifiedInv_map_baseChange. Here unitsBaseChangeHom K L E L is the identity on units, and f(E/K) · [L : E] / [L : K] = 1 by unramifiedness and the tower degree formula. Thus restriction preserves the representing unit and multiplies the invariant by [E : K].

Main definitions

• TauCeti.ClassFieldTheory.unramifiedClass: the class in H²(Gal(L/K), Lˣ) of an element of Kˣ, by two-periodicity at arithmetic Frobenius.
• TauCeti.ClassFieldTheory.unramifiedInvEquiv: the identification H²(Gal(L/K), Lˣ) ≃ ℤ/n sending the class of a to v_K(a) mod n.
• TauCeti.ClassFieldTheory.unramifiedInv: the invariant H²(Gal(L/K), Lˣ) → ℚ/ℤ.

Main results

• TauCeti.ClassFieldTheory.unramifiedClass_eq_cyclicClass: the unramified class is the cyclic class TauCeti.cyclicClass at arithmetic Frobenius.
• TauCeti.ClassFieldTheory.unramifiedClass_apply: the unramified class is the explicit Frobenius-periodicity class of the embedded ground-field unit.
• TauCeti.ClassFieldTheory.unramifiedClass_eq_zero_iff: the class of a vanishes exactly when a is a norm from L.
• TauCeti.ClassFieldTheory.unramifiedInv_unramifiedClass: the normalization inv_{L/K}(unramifiedClass a) = v_K(a) / n.
• TauCeti.ClassFieldTheory.unramifiedInv_injective and TauCeti.ClassFieldTheory.range_unramifiedInv: the invariant is injective with image the subgroup of ℚ/ℤ of order n.
• TauCeti.ClassFieldTheory.map_unramifiedClass: inflation along unramified layers K ⊆ L ⊆ M sends the class of a to the class of a ^ [M : L].
• TauCeti.ClassFieldTheory.unramifiedInv_map: inflation along unramified layers preserves the invariant.
• TauCeti.ClassFieldTheory.map_unramifiedClass_baseChange: base change along an extension K'/K sends the class of a to the class of a ^ (f(K'/K) · [L' : K'] / [L : K]).
• TauCeti.ClassFieldTheory.unramifiedInv_map_baseChange: base change along an extension K'/K multiplies the invariant by [K' : K].
• TauCeti.ClassFieldTheory.map_baseChange_eq_zero_of_finrank_dvd: base change along an extension K'/K of degree a multiple of [L : K] kills H²(Gal(L/K), Lˣ).
• TauCeti.ClassFieldTheory.H2π_eq_zero_of_forall_mem_unitFiltration_zero: a 2-cocycle with values in the units U(L,0) of valuation one represents the zero class of H²(Gal(L/K), Lˣ), since U(L,0) has no Tate cohomology.
• TauCeti.ClassFieldTheory.mk_eq_zero_of_forall_mem_unitFiltration_zero: the same for a continuous 2-cocycle on G_K read off Gal(L/K) with values in U(L,0).
• TauCeti.ClassFieldTheory.brBaseChange_relBrInfl_eq_zero: a Brauer class inflated from a cocycle whose values are units of an unramified layer L/K vanishes after base change to K.

References

• J.-P. Serre, Local Fields, Chapter XII, §1 and Chapter XIII, §3.
• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI (Serre, Local Class Field Theory), §1.
• J. S. Milne, Class Field Theory, Chapter III, §2.

noncomputable def TauCeti.ClassFieldTheory.unramifiedClass (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Additive Kˣ →+ ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))

The class in H²(Gal(L/K), Lˣ) of an element a ∈ Kˣ: the image of a, which is fixed by Frobenius, under two-periodicity of the cohomology of the cyclic group Gal(L/K) at its generator, arithmetic Frobenius.

theorem TauCeti.ClassFieldTheory.unramifiedClass_eq_cyclicClass (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers frobeniusAlgEquiv) : unramifiedClass K L = cyclicClass hg

The unramified class is the cyclic class at arithmetic Frobenius, for any proof that Frobenius generates Gal(L/K).

theorem TauCeti.ClassFieldTheory.unramifiedClass_apply (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (a : Kˣ) : have x := ⋯; let x := IsCyclic.commGroup; (unramifiedClass K L) (Additive.ofMul a) = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) frobeniusAlgEquiv ⋯ 2 ⋯)) ⟨Rep.toAdditive.symm (Additive.ofMul ((Units.map ↑(algebraMap K L)) a)), ⋯⟩

The unramified class of a ground-field unit is its image under Frobenius periodicity.

theorem TauCeti.ClassFieldTheory.unramifiedClass_surjective (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Function.Surjective ⇑(unramifiedClass K L)

Every class in H²(Gal(L/K), Lˣ) is the class of an element of Kˣ.

@[simp]

theorem TauCeti.ClassFieldTheory.unramifiedClass_eq_zero_iff {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] {a : Kˣ} : (unramifiedClass K L) (Additive.ofMul a) = 0 ↔ a ∈ normGroup K L

The class of a ∈ Kˣ in H²(Gal(L/K), Lˣ) vanishes exactly when a is a norm from L.

noncomputable def TauCeti.ClassFieldTheory.unramifiedInvEquiv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ)) ≃+ ZMod (Module.finrank K L)

The identification H²(Gal(L/K), Lˣ) ≃ ℤ/[L : K] of an unramified layer, normalized by arithmetic Frobenius: it sends the class of a ∈ Kˣ to v_K(a) modulo [L : K] (unramifiedInvEquiv_unramifiedClass).

@[simp]

theorem TauCeti.ClassFieldTheory.unramifiedInvEquiv_unramifiedClass {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (a : Kˣ) : (unramifiedInvEquiv K L) ((unramifiedClass K L) (Additive.ofMul a)) = ↑(Multiplicative.toAdd ((normalizedValuation K) a))

The class of a ∈ Kˣ corresponds to the normalized valuation v_K(a) modulo [L : K].

theorem TauCeti.ClassFieldTheory.natCard_H2_unramified (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Nat.card ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ)) = Module.finrank K L

H²(Gal(L/K), Lˣ) of an unramified layer has exactly [L : K] elements.

noncomputable def TauCeti.ClassFieldTheory.unramifiedInv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ)) →+ AddCircle 1

The local invariant of an unramified layer inv_{L/K} : H²(Gal(L/K), Lˣ) → ℚ/ℤ, normalized by arithmetic Frobenius: the class of a ∈ Kˣ has invariant v_K(a) / [L : K] (unramifiedInv_unramifiedClass).

@[simp]

theorem TauCeti.ClassFieldTheory.unramifiedInv_unramifiedClass {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (a : Kˣ) : (unramifiedInv K L) ((unramifiedClass K L) (Additive.ofMul a)) = ↑(↑(Multiplicative.toAdd ((normalizedValuation K) a)) / ↑(Module.finrank K L))

The normalization of the unramified invariant. The class of a ∈ Kˣ has invariant v_K(a) / [L : K].

theorem TauCeti.ClassFieldTheory.unramifiedInv_unramifiedClass_of_isUniformizer {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] {π : Kˣ} (hπ : IsUniformizer K π) : (unramifiedInv K L) ((unramifiedClass K L) (Additive.ofMul π)) = ↑(1 / ↑(Module.finrank K L))

The class of a uniformizer of K has invariant 1 / [L : K], so it is the fundamental class of the unramified layer.

theorem TauCeti.ClassFieldTheory.unramifiedInv_injective (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Function.Injective ⇑(unramifiedInv K L)

The unramified invariant is injective.

theorem TauCeti.ClassFieldTheory.range_unramifiedInv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Set.range ⇑(unramifiedInv K L) = ↑(AddSubgroup.torsionBy (AddCircle 1) ↑(Module.finrank K L))

The image of the unramified invariant is the subgroup of ℚ/ℤ of order [L : K].

Inflation along a tower of unramified layers

@[simp]

theorem TauCeti.ClassFieldTheory.map_unramifiedClass (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (M : Type) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [FiniteDimensional K M] [IsGalois K M] [IsUnramified K M] [Algebra L M] [IsScalarTower K L M] (a : Kˣ) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (AlgEquiv.restrictNormalHom L) (unitsInflationHom K L M) 2)) ((unramifiedClass K L) (Additive.ofMul a)) = (unramifiedClass K M) (Additive.ofMul (a ^ Module.finrank L M))

Inflation of unramified classes. For unramified layers K ⊆ L ⊆ M, inflation H²(Gal(L/K), Lˣ) → H²(Gal(M/K), Mˣ) sends the class of a ∈ Kˣ to the class of a ^ [M : L].

@[simp]

theorem TauCeti.ClassFieldTheory.unramifiedInv_map (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (M : Type) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [FiniteDimensional K M] [IsGalois K M] [IsUnramified K M] [Algebra L M] [IsScalarTower K L M] (x : ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) : (unramifiedInv K M) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (AlgEquiv.restrictNormalHom L) (unitsInflationHom K L M) 2)) x) = (unramifiedInv K L) x

The unramified invariant is compatible with inflation. For unramified layers K ⊆ L ⊆ M, inflation H²(Gal(L/K), Lˣ) → H²(Gal(M/K), Mˣ) preserves the local invariant.

Change of ground field

@[simp]

theorem TauCeti.ClassFieldTheory.map_unramifiedClass_baseChange (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (K' : Type) [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] [Algebra K K'] [ValuativeExtension K K'] (L' : Type) [Field L'] [ValuativeRel L'] [TopologicalSpace L'] [IsNonarchimedeanLocalField L'] [Algebra K' L'] [ValuativeExtension K' L'] [FiniteDimensional K' L'] [IsGalois K' L'] [IsUnramified K' L'] [Algebra K L'] [IsScalarTower K K' L'] [Algebra L L'] [IsScalarTower K L L'] [ValuativeExtension L L'] (a : Kˣ) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map ((AlgEquiv.restrictNormalHom L).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K L K' L') 2)) ((unramifiedClass K L) (Additive.ofMul a)) = (unramifiedClass K' L') (Additive.ofMul ((Units.map ↑(algebraMap K K')) a ^ (inertiaDegree K K' * Module.finrank K' L' / Module.finrank K L)))

Base change of unramified classes. Let K'/K be an extension of nonarchimedean local fields, of residue degree f(K'/K), and let L'/K' be an unramified layer containing L. Then the map H²(Gal(L/K), Lˣ) → H²(Gal(L'/K'), L'ˣ) induced by restriction Gal(L'/K') → Gal(L/K) sends the class of a ∈ Kˣ to the class of a ^ (f(K'/K) · [L' : K'] / [L : K]).

@[simp]

theorem TauCeti.ClassFieldTheory.unramifiedInv_map_baseChange (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (K' : Type) [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] [Algebra K K'] [ValuativeExtension K K'] (L' : Type) [Field L'] [ValuativeRel L'] [TopologicalSpace L'] [IsNonarchimedeanLocalField L'] [Algebra K' L'] [ValuativeExtension K' L'] [FiniteDimensional K' L'] [IsGalois K' L'] [IsUnramified K' L'] [Algebra K L'] [IsScalarTower K K' L'] [Algebra L L'] [IsScalarTower K L L'] [ValuativeExtension L L'] (x : ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) : (unramifiedInv K' L') ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map ((AlgEquiv.restrictNormalHom L).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K L K' L') 2)) x) = Module.finrank K K' • (unramifiedInv K L) x

The unramified invariant under base change. Let K'/K be an extension of nonarchimedean local fields and let L'/K' be an unramified layer containing L. Then the map H²(Gal(L/K), Lˣ) → H²(Gal(L'/K'), L'ˣ) induced by restriction Gal(L'/K') → Gal(L/K) multiplies the local invariant by [K' : K].

theorem TauCeti.ClassFieldTheory.map_baseChange_eq_zero_of_finrank_dvd (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (K' : Type) [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] [Algebra K K'] [ValuativeExtension K K'] (L' : Type) [Field L'] [ValuativeRel L'] [TopologicalSpace L'] [IsNonarchimedeanLocalField L'] [Algebra K' L'] [ValuativeExtension K' L'] [FiniteDimensional K' L'] [IsGalois K' L'] [IsUnramified K' L'] [Algebra K L'] [IsScalarTower K K' L'] [Algebra L L'] [IsScalarTower K L L'] [ValuativeExtension L L'] (h : Module.finrank K L ∣ Module.finrank K K') (x : ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map ((AlgEquiv.restrictNormalHom L).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K L K' L') 2)) x = 0

Unramified classes split by a ground field of multiple degree. Let K'/K be an extension of nonarchimedean local fields whose degree is a multiple of [L : K], and let L'/K' be an unramified layer containing L. Then the map H²(Gal(L/K), Lˣ) → H²(Gal(L'/K'), L'ˣ) induced by restriction Gal(L'/K') → Gal(L/K) is zero.

Cocycles with unit values

theorem TauCeti.ClassFieldTheory.H2π_eq_zero_of_forall_mem_unitFiltration_zero (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [IsGalois K L] [IsUnramified K L] (c : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) (hc : ∀ (g h : Gal(L/K)), Additive.toMul (Rep.toAdditive (c (g, h))) ∈ unitFiltration L 0) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) c = 0

A unit-valued cocycle of an unramified layer is a coboundary. If a 2-cocycle of Gal(L/K) with values in Lˣ takes all its values in the units U(L,0) of valuation one, its class in H²(Gal(L/K), Lˣ) vanishes.

theorem TauCeti.ClassFieldTheory.mk_eq_zero_of_forall_mem_unitFiltration_zero (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (σ : L →ₐ[K] SeparableClosure K) (z : ↥(ContCohomology.Z2 (AbsoluteGaloisGroup K) (UnitsCoeff K))) (u : Gal(L/K) × Gal(L/K) → Lˣ) (hu : ∀ (p : Gal(L/K) × Gal(L/K)), u p ∈ unitFiltration L 0) (hz : ∀ (g h : AbsoluteGaloisGroup K), ↑z (g, h) = ↑((embeddedUnitsEquivInvariants K L σ) (Additive.ofMul (u (σ.restrictNormalHom g, σ.restrictNormalHom h))))) : ↑z = 0

A continuous cocycle read off an unramified layer with unit values is a coboundary. 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 a function u on Gal(L/K) × Gal(L/K) with values in the units U(L,0) of valuation one, then the class of z in H²(G_K, (Kˢ)ˣ) vanishes.

theorem TauCeti.ClassFieldTheory.brBaseChange_relBrInfl_eq_zero (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (F : Type) [Field F] [Algebra F K] [Algebra F L] [IsScalarTower F K L] (E : Type) [Field E] [Algebra F E] [FiniteDimensional F E] [Normal F E] [Algebra E L] [IsScalarTower F E L] (σ : E →ₐ[F] SeparableClosure F) (c : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(E/F) Eˣ))) (hc : ∀ (g h : Gal(E/F)), (Units.map ↑(algebraMap E L)) (Additive.toMul (Rep.toAdditive (c (g, h)))) ∈ unitFiltration L 0) : (brBaseChange F K) ((relBrInfl F E σ) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofMulDistribMulAction Gal(E/F) Eˣ))) c)) = 0

A class inflated along an unramified layer with unit values vanishes locally. Let E/F be a finite normal extension, embedded in Fˢ by σ, and let K be an F-algebra with a finite unramified Galois extension L/K receiving E. If a 2-cocycle c of Gal(E/F) with values in Eˣ takes all its values in the units U(L,0) of valuation one after the inclusion Eˣ → Lˣ, then the base change to K of the class inflated from c vanishes.