The multiplicative coefficient modules of Galois cohomology

Galois cohomology takes its coefficients in discrete modules over G_K = AbsoluteGaloisGroup K, the automorphism group of a separable closure Kˢ. This file fixes the two multiplicative coefficient modules once and for all, written additively through Additive as Mathlib's Representation.ofMulDistribMulAction does:

UnitsCoeff K = Additive (Kˢ)ˣ,      KummerCoeff K n = Additive μₙ,

with μₙ = rootsOfUnity n Kˢ. Both are discrete G_K-modules: their point stabilizers are open because every element of Kˢ is separable over K, hence lies in a finite subextension (TauCeti.stabilizer_isOpen_units). The action on μₙ is in general nontrivial, and the Kummer isomorphism is false for the trivial action, so it is the module and not the abstract group that is named here.

The two maps between them assemble the Kummer sequence

1 ⟶ μₙ ⟶ (Kˢ)ˣ ⟶ (Kˢ)ˣ ⟶ 1

as a TauCeti.ContCohomology.DiscreteShortExact, so that the long exact sequence of continuous cohomology applies to it verbatim. Exactness in the middle holds over any field and for any n; surjectivity on the right is where IsUnit (n : K) enters, through the separability of Xⁿ - a and the separable closedness of Kˢ.

Finally TauCeti.baseUnitsEquivInvariants identifies H⁰(G_K, (Kˢ)ˣ) with Kˣ. These are not the same Lean type — the invariants are an additive subgroup of Additive (Kˢ)ˣ — so what is supplied is the canonical isomorphism and not an equality. Using the separable closure is essential: for imperfect K the fixed field of the automorphism group of an algebraic closure is the purely inseparable closure of K and not K itself (TauCeti.mem_perfectClosure_iff_fixed), so the invariants of the units of an algebraic closure are strictly larger than Kˣ.

Main definitions

• TauCeti.UnitsCoeff, TauCeti.KummerCoeff: the two coefficient modules, with their discrete topologies.
• TauCeti.kummerCoeffAddEquivZMod: an additive isomorphism μₙ ≃ ℤ/nℤ, for n invertible in K.
• TauCeti.kummerCoeffIncl, TauCeti.unitsCoeffPow: the inclusion μₙ ↪ (Kˢ)ˣ and the n-th power map, the two maps of the Kummer sequence.
• TauCeti.kummerShortExact: the Kummer sequence as a short exact sequence of discrete G_K-modules.
• TauCeti.baseUnitsEquivInvariants: the isomorphism Kˣ ≅ H⁰(G_K, (Kˢ)ˣ).
• TauCeti.embeddedUnitsInvariants: for a K-embedding σ : L →ₐ[K] Kˢ, a unit b of L as the invariant σ b of (Kˢ)ˣ under the subgroup of G_K fixing σ(L).
• TauCeti.embeddedUnitsEquivInvariants: the isomorphism Lˣ ≅ H⁰(Gal(Kˢ/σ(L)), (Kˢ)ˣ). For normal L/K it intertwines the action of σ.restrictNormalHom g with that of g (TauCeti.embeddedUnitsEquivInvariants_restrictNormalHom_smul, with the simp form TauCeti.coe_embeddedUnitsInvariants_map_restrictNormalHom).

Main results

• TauCeti.unitsCoeff_continuousSMul, TauCeti.kummerCoeff_continuousSMul: the coefficients are discrete modules, that is, the action is continuous.
• TauCeti.natCard_kummerCoeff: μₙ has n elements, for n invertible in K.
• TauCeti.smul_kummerCoeff_eq_self: the action on μₙ is trivial when K contains a primitive nth root of unity.
• TauCeti.mem_H0_unitsCoeff_iff: a unit of Kˢ fixed by G_K comes from Kˣ.
• TauCeti.mem_H0_fixingSubgroup_unitsCoeff_iff: a unit of Kˢ fixed by the subgroup fixing σ(L) comes from Lˣ.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (6.2.1) and the display following it, for the Kummer sequence and the invariants of (Kˢ)ˣ.

The units of the separable closure

@[reducible, inline]

abbrev TauCeti.UnitsCoeff (K : Type u_1) [Field K] : Type u_1

The multiplicative coefficient module of Galois cohomology: the units of a separable closure of K, written additively. This is the module Hilbert 90 and the cohomological Brauer group are stated at, and KummerCoeff K n is its n-torsion submodule.

Equations

• TauCeti.UnitsCoeff K = Additive (SeparableClosure K)ˣ

@[instance_reducible]

instance TauCeti.instTopologicalSpaceUnitsCoeff (K : Type u_1) [Field K] : TopologicalSpace (UnitsCoeff K)

Equations

• TauCeti.instTopologicalSpaceUnitsCoeff K = ⊥

instance TauCeti.instDiscreteTopologyUnitsCoeff (K : Type u_1) [Field K] : DiscreteTopology (UnitsCoeff K)

instance TauCeti.unitsCoeff_continuousSMul (K : Type u_1) [Field K] : ContinuousSMul (AbsoluteGaloisGroup K) (UnitsCoeff K)

(Kˢ)ˣ is a discrete G_K-module: every unit of Kˢ is separable over K, so it lies in a finite subextension and its stabilizer is open.

The roots of unity

@[reducible, inline]

abbrev TauCeti.KummerCoeff (K : Type u_1) [Field K] (n : ℕ) : Type u_1

The Kummer coefficient module: the n-th roots of unity in a separable closure of K, written additively. The G_K-action on μₙ is in general nontrivial and the Kummer isomorphism depends on it, so the coefficients are fixed as this module rather than as an abstract cyclic group.

Equations

• TauCeti.KummerCoeff K n = Additive ↥(rootsOfUnity n (SeparableClosure K))

@[instance_reducible]

instance TauCeti.instTopologicalSpaceKummerCoeff (K : Type u_1) [Field K] (n : ℕ) : TopologicalSpace (KummerCoeff K n)

Equations

• TauCeti.instTopologicalSpaceKummerCoeff K n = ⊥

instance TauCeti.instDiscreteTopologyKummerCoeff (K : Type u_1) [Field K] (n : ℕ) : DiscreteTopology (KummerCoeff K n)

instance TauCeti.kummerCoeff_continuousSMul (K : Type u_1) [Field K] (n : ℕ) : ContinuousSMul (AbsoluteGaloisGroup K) (KummerCoeff K n)

μₙ is a discrete G_K-module: the stabilizer of a root of unity is the stabilizer of the underlying unit of Kˢ, which is open.

theorem TauCeti.smul_kummerCoeff_eq_self {K : Type u_1} [Field K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (g : AbsoluteGaloisGroup K) (x : KummerCoeff K n) : g • x = x

G_K acts trivially on μₙ when K contains a primitive nth root of unity ζ: every nth root of unity of Kˢ is then a power of ζ, which G_K fixes.

theorem TauCeti.natCard_kummerCoeff {K : Type u_1} [Field K] {n : ℕ} (hn : IsUnit ↑n) : Nat.card (KummerCoeff K n) = n

μₙ has n elements for n invertible in K.

noncomputable def TauCeti.kummerCoeffAddEquivZMod {K : Type u_1} [Field K] {n : ℕ} (hn : IsUnit ↑n) : KummerCoeff K n ≃+ ZMod n

μₙ is cyclic of order n for n invertible in K: the nth roots of unity of Kˢ are additively isomorphic to ℤ/nℤ. The isomorphism is not canonical; it amounts to a choice of primitive nth root of unity in Kˢ.

Equations

• TauCeti.kummerCoeffAddEquivZMod hn = addEquivOfAddCyclicCardEq ⋯

The two maps of the Kummer sequence

noncomputable def TauCeti.kummerCoeffIncl (K : Type u_1) [Field K] (n : ℕ) : KummerCoeff K n →+ UnitsCoeff K

The inclusion μₙ ↪ (Kˢ)ˣ, the left-hand map of the Kummer sequence.

Equations

• TauCeti.kummerCoeffIncl K n = MonoidHom.toAdditive (rootsOfUnity n (SeparableClosure K)).subtype

@[simp]

theorem TauCeti.toMul_kummerCoeffIncl (K : Type u_1) [Field K] (n : ℕ) (x : KummerCoeff K n) : Additive.toMul ((kummerCoeffIncl K n) x) = ↑(Additive.toMul x)

@[simp]

theorem TauCeti.kummerCoeffIncl_equivariant (K : Type u_1) [Field K] (n : ℕ) (g : AbsoluteGaloisGroup K) (x : KummerCoeff K n) : (kummerCoeffIncl K n) (g • x) = g • (kummerCoeffIncl K n) x

theorem TauCeti.kummerCoeffIncl_injective (K : Type u_1) [Field K] (n : ℕ) : Function.Injective ⇑(kummerCoeffIncl K n)

noncomputable def TauCeti.unitsCoeffPow (K : Type u_1) [Field K] (n : ℕ) : UnitsCoeff K →+ UnitsCoeff K

The n-th power map on (Kˢ)ˣ, the right-hand map of the Kummer sequence. In additive notation it is multiplication by n, which is TauCeti.unitsCoeffPow_eq_nsmul.

Equations

• TauCeti.unitsCoeffPow K n = MonoidHom.toAdditive (powMonoidHom n)

@[simp]

theorem TauCeti.toMul_unitsCoeffPow (K : Type u_1) [Field K] (n : ℕ) (x : UnitsCoeff K) : Additive.toMul ((unitsCoeffPow K n) x) = Additive.toMul x ^ n

theorem TauCeti.unitsCoeffPow_eq_nsmul (K : Type u_1) [Field K] (n : ℕ) (x : UnitsCoeff K) : (unitsCoeffPow K n) x = n • x

@[simp]

theorem TauCeti.unitsCoeffPow_equivariant (K : Type u_1) [Field K] (n : ℕ) (g : AbsoluteGaloisGroup K) (x : UnitsCoeff K) : (unitsCoeffPow K n) (g • x) = g • (unitsCoeffPow K n) x

theorem TauCeti.kummerSequence_exact (K : Type u_1) [Field K] (n : ℕ) : Function.Exact ⇑(kummerCoeffIncl K n) ⇑(unitsCoeffPow K n)

Exactness of the Kummer sequence in the middle: a unit of Kˢ has trivial n-th power exactly when it is an n-th root of unity. This holds over any field and for every n.

theorem TauCeti.unitsCoeffPow_surjective (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) : Function.Surjective ⇑(unitsCoeffPow K n)

The n-th power map on the units of a separable closure is surjective when n is invertible in K: Xⁿ - a is then separable, and Kˢ is separably closed.

noncomputable def TauCeti.kummerShortExact (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) : ContCohomology.DiscreteShortExact (AbsoluteGaloisGroup K) (KummerCoeff K n) (UnitsCoeff K) (UnitsCoeff K)

The Kummer sequence 1 → μₙ → (Kˢ)ˣ → (Kˢ)ˣ → 1 of discrete G_K-modules, for n invertible in K (NSW (6.2.1)). It is the datum the long exact sequence of continuous cohomology is applied to, and its degree-zero connecting map is the Kummer map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.kummerShortExact_incl (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) : (kummerShortExact K n hn).incl = kummerCoeffIncl K n

@[simp]

theorem TauCeti.kummerShortExact_proj (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) : (kummerShortExact K n hn).proj = unitsCoeffPow K n

The invariants of the units

theorem TauCeti.smul_units_map_algebraMap {K : Type u_1} [Field K] (g : AbsoluteGaloisGroup K) (a : Kˣ) : g • (Units.map ↑(algebraMap K (SeparableClosure K))) a = (Units.map ↑(algebraMap K (SeparableClosure K))) a

A unit of the base field is fixed by the absolute Galois group after mapping into the separable closure.

theorem TauCeti.mem_H0_unitsCoeff_iff {K : Type u_1} [Field K] {u : UnitsCoeff K} : u ∈ ContCohomology.H0 (AbsoluteGaloisGroup K) (UnitsCoeff K) ↔ ∃ (a : Kˣ), (Units.map ↑(algebraMap K (SeparableClosure K))) a = Additive.toMul u

A unit of Kˢ fixed by the whole Galois group comes from Kˣ. This is the fixed-field theorem for the separable closure read on units: InfiniteGalois.mem_range_algebraMap_iff_fixed supplies a base-field preimage of the unit, and TauCeti.mem_range_iff_exists_units_map_eq promotes it to a unit of K.

noncomputable def TauCeti.baseUnitsEquivInvariants (K : Type u_1) [Field K] : Additive Kˣ ≃+ ↥(ContCohomology.H0 (AbsoluteGaloisGroup K) (UnitsCoeff K))

The invariants of (Kˢ)ˣ are the units of K, that is H⁰(G_K, (Kˢ)ˣ) ≅ Kˣ. The two sides are different Lean types, so this canonical isomorphism — and not an equality — is what a cohomological construction starting from Kˣ goes through, the Kummer map among them.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.toMul_coe_baseUnitsEquivInvariants (K : Type u_1) [Field K] (a : Additive Kˣ) : Additive.toMul ↑((baseUnitsEquivInvariants K) a) = (Units.map ↑(algebraMap K (SeparableClosure K))) (Additive.toMul a)

noncomputable def TauCeti.embeddedUnitsInvariants (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (b : Lˣ) : ↥(ContCohomology.H0 (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K))

A unit of L as an invariant of (Kˢ)ˣ under Gal(Kˢ/σ(L)): every automorphism of Kˢ fixing σ(L) fixes σ b. For the subgroup cut out by σ this is what TauCeti.baseUnitsEquivInvariants is for the whole of G_K.

Equations

• TauCeti.embeddedUnitsInvariants K L σ b = ⟨Additive.ofMul ((Units.map ↑σ.toRingHom) b), ⋯⟩

@[simp]

theorem TauCeti.toMul_coe_embeddedUnitsInvariants (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (b : Lˣ) : Additive.toMul ↑(embeddedUnitsInvariants K L σ b) = (Units.map ↑σ.toRingHom) b

The invariant attached to a unit of L is the image of that unit in (Kˢ)ˣ.

@[simp]

theorem TauCeti.embeddedUnitsInvariants_one (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : embeddedUnitsInvariants K L σ 1 = 0

The unit 1 of L is the zero invariant.

@[simp]

theorem TauCeti.embeddedUnitsInvariants_mul (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (a b : Lˣ) : embeddedUnitsInvariants K L σ (a * b) = embeddedUnitsInvariants K L σ a + embeddedUnitsInvariants K L σ b

Multiplication of units of L becomes addition of invariants.

theorem TauCeti.mem_H0_fixingSubgroup_unitsCoeff_iff {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] {σ : L →ₐ[K] SeparableClosure K} {u : UnitsCoeff K} : u ∈ ContCohomology.H0 (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K) ↔ ∃ (b : Lˣ), (Units.map ↑σ.toRingHom) b = Additive.toMul u

A unit of Kˢ fixed by Gal(Kˢ/σ(L)) comes from Lˣ. This is the fixed-field theorem InfiniteGalois.fixedField_fixingSubgroup for the intermediate field σ(L), read on units.

noncomputable def TauCeti.embeddedUnitsEquivInvariants (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : Additive Lˣ ≃+ ↥(ContCohomology.H0 (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K))

The invariants of (Kˢ)ˣ under Gal(Kˢ/σ(L)) are the units of L, that is H⁰(Gal(Kˢ/σ(L)), (Kˢ)ˣ) ≅ Lˣ: the additive equivalence whose forward map is embeddedUnitsInvariants. For σ(L) = K this is TauCeti.baseUnitsEquivInvariants.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.embeddedUnitsEquivInvariants_apply (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (b : Additive Lˣ) : (embeddedUnitsEquivInvariants K L σ) b = embeddedUnitsInvariants K L σ (Additive.toMul b)

embeddedUnitsEquivInvariants sends a unit of L to its invariant embeddedUnitsInvariants.

@[simp]

theorem TauCeti.coe_embeddedUnitsInvariants_map_restrictNormalHom (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Normal K L] (g : AbsoluteGaloisGroup K) (b : Lˣ) : ↑(embeddedUnitsInvariants K L σ ((Units.map ↑(σ.restrictNormalHom g)) b)) = g • ↑(embeddedUnitsInvariants K L σ b)

embeddedUnitsInvariants is Galois-equivariant, in simp-normal form: for normal L/K, embedding by σ turns the restriction σ.restrictNormalHom g acting on Lˣ into the action of g on (Kˢ)ˣ.

theorem TauCeti.embeddedUnitsEquivInvariants_restrictNormalHom_smul (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Normal K L] (g : AbsoluteGaloisGroup K) (b : Additive Lˣ) : ↑((embeddedUnitsEquivInvariants K L σ) (Additive.ofMul (σ.restrictNormalHom g • Additive.toMul b))) = g • ↑((embeddedUnitsEquivInvariants K L σ) b)

embeddedUnitsEquivInvariants is Galois-equivariant: for normal L/K, embedding by σ turns the action of the restriction σ.restrictNormalHom g on Lˣ into the action of g on (Kˢ)ˣ.