The Kummer map Kˣ → H¹(G_K, μₙ) and the Kummer isomorphism

Let K be a field, Kˢ a separable closure, G_K = AbsoluteGaloisGroup K, and n a natural number invertible in K. The Kummer sequence

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

of discrete G_K-modules is TauCeti.kummerShortExact; its degree-zero connecting map, read through the identification TauCeti.baseUnitsEquivInvariants of H⁰(G_K, (Kˢ)ˣ) with Kˣ, is the Kummer map Kˣ → H¹(G_K, μₙ). This file constructs it, computes it on cocycles, identifies its kernel, and proves that it induces the Kummer isomorphism Kˣ ⧸ (Kˣ)ⁿ ≃ H¹(G_K, μₙ).

The computation is the classical one. Choose an nth root α ∈ (Kˢ)ˣ of a ∈ Kˣ; then g ↦ g α / α takes values in μₙ, because raising it to the n gives g a / a = 1, and it is a continuous 1-cocycle, because its image in (Kˢ)ˣ is the coboundary d⁰ α. Its class is the Kummer class of a. The class does not depend on the choice of root: two roots differ by an element ζ of μₙ, and the two cocycles differ by the coboundary d⁰ ζ. That independence is proved directly, with no hypothesis on n, so it is available for any a that happens to have a root.

The kernel is (Kˣ)ⁿ. This is exactness of the long exact sequence at H⁰(G_K, (Kˢ)ˣ) — explicitLongExact_H0C — together with the commuting square TauCeti.explicitCoeff0_baseUnitsEquivInvariants, which says that the nth power map on the invariants of (Kˢ)ˣ is the nth power map of Kˣ. So the Kummer map descends to an injection of the power-class group Kˣ ⧸ (Kˣ)ⁿ into H¹(G_K, μₙ).

The Kummer map is surjective. This is exactness of the same sequence at H¹(G_K, μₙ) — explicitLongExact_H1A — together with Hilbert 90, H¹(G_K, (Kˢ)ˣ) = 0 (TauCeti.subsingleton_H1_unitsCoeff): every class of H¹(G_K, μₙ) dies in H¹(G_K, (Kˢ)ˣ) and so is a connecting image. Injectivity on power classes and surjectivity together give the Kummer isomorphism TauCeti.kummerIso.

The Kummer isomorphism is natural in the field for restriction. A K-embedding σ : L →ₐ[K] Kˢ identifies Lˢ with Kˢ and G_L with the subgroup of G_K fixing σ(L); restricting the Kummer cocycle g ↦ g α / α of a ∈ Kˣ to that subgroup and transporting it to G_L gives the Kummer cocycle of the image of a in Lˣ, with the transported root. So restriction on H¹(·, μₙ) corresponds to the map Kˣ ⧸ (Kˣ)ⁿ → Lˣ ⧸ (Lˣ)ⁿ of power classes. No finiteness of L/K is used.

For a finite L/K the subgroup fixing σ(L) is open of index [L : K], so it carries a corestriction, and the second square of the functoriality says that corestriction H¹(G_L, μₙ) → H¹(G_K, μₙ) corresponds to the norm Lˣ ⧸ (Lˣ)ⁿ → Kˣ ⧸ (Kˣ)ⁿ. In degree zero, corestriction on the invariant σ b of the fixing subgroup is the product of the conjugates of σ b, that is N_{L/K} b.

Main definitions

• TauCeti.kummerCocycle: the cocycle g ↦ g α / α attached to a choice of nth root, and TauCeti.kummerCocycleClass its class in H¹(G_K, μₙ).
• TauCeti.kummerMap: the multiplicative Kummer map Kˣ →* Multiplicative (H¹(G_K, μₙ)).
• TauCeti.kummerClassMap: the induced map on the power classes Kˣ ⧸ (Kˣ)ⁿ.
• TauCeti.kummerIso: the Kummer isomorphism Kˣ ⧸ (Kˣ)ⁿ ≃* H¹(G_K, μₙ).
• TauCeti.kummerIsoTransport: the Kummer isomorphism after an equivariant identification of the roots of unity with another discrete coefficient module.
• TauCeti.kummerCoeffPow: the power map μₙ → μₘ, ζ ↦ ζ ^ (n / m), for m ∣ n.
• TauCeti.kummerRes: restriction H¹(G_K, μₙ) → H¹(G_L, μₙ) along a K-embedding σ : L →ₐ[K] Kˢ, with its coefficient identification TauCeti.kummerCoeffMap.
• TauCeti.kummerCor: corestriction H¹(G_L, μₙ) → H¹(G_K, μₙ) along a K-embedding of a finite extension, with its coefficient identifications TauCeti.kummerCoeffMapSymm and TauCeti.unitsCoeffMapSymm; TauCeti.unitsCoeffMap is the inverse of the latter.

Main results

• TauCeti.kummerCocycle_mem_Z1: g ↦ g α / α is a continuous 1-cocycle.
• TauCeti.kummerCocycleClass_def: the cocycle class is the class of its named cocycle.
• TauCeti.kummerCocycleClass_congr: independence of the choice of nth root.
• TauCeti.kummerMap_eq_kummerCocycleClass: the Kummer class of a is the class of g ↦ g α / α.
• TauCeti.ker_kummerMap: the kernel of the Kummer map is (Kˣ)ⁿ, with TauCeti.kummerMap_eq_one_iff the pointwise form.
• TauCeti.kummerClassMap_injective: Kˣ ⧸ (Kˣ)ⁿ injects into H¹(G_K, μₙ).
• TauCeti.kummerMap_surjective: every class of H¹(G_K, μₙ) is a Kummer class.
• TauCeti.finite_H1_kummerCoeff: H¹(G_K, μₙ) is finite when Kˣ ⧸ (Kˣ)ⁿ is.
• TauCeti.finite_H1_of_isPrimitiveRoot_of_natCard_eq: the same for every cyclic trivial module of order n over a group isomorphic to G_K, when K contains the nth roots of unity.
• TauCeti.explicitCoeff1_kummerCoeffPow_kummerMap: the power map μₙ → μₘ sends the Kummer class of a at level n to its Kummer class at level m, and TauCeti.explicitCoeff1_kummerCoeffPow_surjective: it is surjective on H¹.
• TauCeti.explicitIso_kummerMap: the explicit and canonical Kummer maps agree under the degree-one comparison isomorphism.
• TauCeti.kummerIso_res: the Kummer isomorphism is natural for restriction along a field extension, restriction corresponding to the map of power classes Kˣ ⧸ (Kˣ)ⁿ → Lˣ ⧸ (Lˣ)ⁿ; TauCeti.kummerRes_kummerMap is the same statement on units.
• TauCeti.explicitCor0_embeddedUnitsInvariants: degree-zero corestriction on the invariants of (Kˢ)ˣ is the norm of L/K.
• TauCeti.kummerIso_norm: for a finite L/K, corestriction corresponds to the map of power classes Lˣ ⧸ (Lˣ)ⁿ → Kˣ ⧸ (Kˣ)ⁿ induced by the norm; TauCeti.kummerCor_kummerMap is the same statement on units.

References

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

The cocycle attached to an nth root

Nothing in this section needs n to be invertible in K: the input is a chosen nth root of the given unit, and invertibility of n is only what produces one.

theorem TauCeti.smul_mul_inv_mem_rootsOfUnity {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α : (SeparableClosure K)ˣ} (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) (g : AbsoluteGaloisGroup K) : g • α * α⁻¹ ∈ rootsOfUnity n (SeparableClosure K)

The Kummer ratio is an nth root of unity: if αⁿ = a with a in the base field, then (g α / α)ⁿ = g a / a = 1.

noncomputable def TauCeti.kummerCocycle {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α : (SeparableClosure K)ˣ} (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) : AbsoluteGaloisGroup K → KummerCoeff K n

The Kummer cocycle g ↦ g α / α of a unit a of K and a choice of nth root α of a in Kˢ. Its class is the Kummer class of a (TauCeti.kummerMap_eq_kummerCocycleClass) and is independent of the choice of α (TauCeti.kummerCocycleClass_congr).

Equations

• TauCeti.kummerCocycle hα g = Additive.ofMul ⟨g • α * α⁻¹, ⋯⟩

@[simp]

theorem TauCeti.toMul_kummerCocycle {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α : (SeparableClosure K)ˣ} (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) (g : AbsoluteGaloisGroup K) : ↑(Additive.toMul (kummerCocycle hα g)) = g • α * α⁻¹

theorem TauCeti.kummerCoeffIncl_kummerCocycle {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α : (SeparableClosure K)ˣ} (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) (g : AbsoluteGaloisGroup K) : (kummerCoeffIncl K n) (kummerCocycle hα g) = g • Additive.ofMul α - Additive.ofMul α

The coefficient inclusion of the Kummer cocycle is the coboundary ratio g • α - α in the units of Kˢ.

theorem TauCeti.kummerCocycle_mem_Z1 {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α : (SeparableClosure K)ˣ} (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) : kummerCocycle hα ∈ ContCohomology.Z1 (AbsoluteGaloisGroup K) (KummerCoeff K n)

The Kummer ratio g ↦ g α / α is a continuous 1-cocycle with values in μₙ.

noncomputable def TauCeti.kummerCocycleClass {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α : (SeparableClosure K)ˣ} (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) : ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n)

The class in H¹(G_K, μₙ) of the Kummer cocycle of a chosen nth root.

Equations

• TauCeti.kummerCocycleClass hα = (TauCeti.ContCohomology.H1pi (TauCeti.AbsoluteGaloisGroup K) (TauCeti.KummerCoeff K n)) ⟨TauCeti.kummerCocycle hα, ⋯⟩

theorem TauCeti.kummerCocycleClass_def {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α : (SeparableClosure K)ˣ} (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) : kummerCocycleClass hα = (ContCohomology.H1pi (AbsoluteGaloisGroup K) (KummerCoeff K n)) ⟨kummerCocycle hα, ⋯⟩

The defining equation of TauCeti.kummerCocycleClass: it is the class in H¹ represented by the cocycle TauCeti.kummerCocycle.

theorem TauCeti.kummerCocycleClass_congr {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α β : (SeparableClosure K)ˣ} (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) (hβ : β ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) : kummerCocycleClass hα = kummerCocycleClass hβ

The Kummer class is independent of the chosen nth root. Two nth roots of the same a differ by an element ζ of μₙ, and g (α ζ) / (α ζ) = (g α / α) · (g ζ / ζ) differs from g α / α by the coboundary of ζ.

The Kummer map and its kernel

noncomputable def TauCeti.kummerMap (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) : Kˣ →* Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n))

The Kummer map Kˣ →* Multiplicative (H¹(G_K, μₙ)): the degree-zero connecting homomorphism of the Kummer sequence, written multiplicatively on the units of K.

Equations

• TauCeti.kummerMap K n hn = AddMonoidHom.toMultiplicativeRight (TauCeti.kummerMapAdd✝ K n hn)

@[simp]

theorem TauCeti.kummerMap_apply (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) (a : Kˣ) : (kummerMap K n hn) a = Multiplicative.ofAdd ((kummerShortExact K n hn).explicitDelta0 ((baseUnitsEquivInvariants K) (Additive.ofMul a)))

The Kummer map is the degree-zero connecting homomorphism of the Kummer sequence, read on the unit a through the identification of Kˣ with the invariants of (Kˢ)ˣ.

theorem TauCeti.exists_pow_eq_units_map {K : Type u_1} [Field K] {n : ℕ} (hn : IsUnit ↑n) (a : Kˣ) : ∃ (α : (SeparableClosure K)ˣ), α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a

Every unit of K has an nth root in Kˢ when n is invertible in K; this is TauCeti.unitsCoeffPow_surjective read on units.

theorem TauCeti.kummerMap_eq_kummerCocycleClass {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α : (SeparableClosure K)ˣ} (hn : IsUnit ↑n) (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) : Multiplicative.toAdd ((kummerMap K n hn) a) = kummerCocycleClass hα

The Kummer class of a is represented by g ↦ g α / α, for any nth root α of a in Kˢ (NSW (6.2.1)). Together with TauCeti.exists_pow_eq_units_map this computes the Kummer map on every unit.

theorem TauCeti.explicitCoeff0_baseUnitsEquivInvariants {K : Type u_1} [Field K] {n : ℕ} (hn : IsUnit ↑n) (c : Additive Kˣ) : (ContCohomology.explicitCoeff0 (AbsoluteGaloisGroup K) (UnitsCoeff K) (kummerShortExact K n hn).projDistribMulActionHom) ((baseUnitsEquivInvariants K) c) = (baseUnitsEquivInvariants K) (Additive.ofMul (Additive.toMul c ^ n))

The nth power map on invariants is the nth power map of Kˣ. This is the commuting square that turns exactness of the long exact sequence at H⁰(G_K, (Kˢ)ˣ) into the computation of the kernel of the Kummer map.

theorem TauCeti.ker_kummerMap {K : Type u_1} [Field K] {n : ℕ} (hn : IsUnit ↑n) : (kummerMap K n hn).ker = powerSubgroup Kˣ n

The kernel of the multiplicative Kummer map is (Kˣ)ⁿ.

theorem TauCeti.kummerMap_eq_one_iff {K : Type u_1} [Field K] {n : ℕ} (hn : IsUnit ↑n) (a : Kˣ) : (kummerMap K n hn) a = 1 ↔ ∃ (b : Kˣ), b ^ n = a

A unit has trivial Kummer class exactly when it is an nth power in K.

The Kummer map on power classes

noncomputable def TauCeti.kummerClassMap (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) : powerClassQuotient Kˣ n →* Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n))

The Kummer map on power classes, Kˣ ⧸ (Kˣ)ⁿ → H¹(G_K, μₙ). It is injective (TauCeti.kummerClassMap_injective) and surjective, and TauCeti.kummerIso is the resulting isomorphism.

Equations

• TauCeti.kummerClassMap K n hn = QuotientGroup.lift (TauCeti.powerSubgroup Kˣ n) (TauCeti.kummerMap K n hn) ⋯

@[simp]

theorem TauCeti.kummerClassMap_mk (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) (a : Kˣ) : (kummerClassMap K n hn) ↑a = (kummerMap K n hn) a

The quotient Kummer map agrees with kummerMap on representatives.

theorem TauCeti.kummerClassMap_powerClassHom (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) (a : Kˣ) : (kummerClassMap K n hn) ((powerClassHom Kˣ n) a) = (kummerMap K n hn) a

The quotient Kummer map sends the named power class of a to its Kummer class.

theorem TauCeti.kummerClassMap_injective (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) : Function.Injective ⇑(kummerClassMap K n hn)

Kˣ ⧸ (Kˣ)ⁿ injects into H¹(G_K, μₙ), the kernel of the Kummer map being exactly the nth powers.

Surjectivity and the Kummer isomorphism

theorem TauCeti.kummerMap_surjective {K : Type u_1} [Field K] {n : ℕ} (hn : IsUnit ↑n) : Function.Surjective ⇑(kummerMap K n hn)

Every class of H¹(G_K, μₙ) is a Kummer class, by Hilbert 90: the class dies in H¹(G_K, (Kˢ)ˣ) = 0, so it is the image of the connecting map of the Kummer sequence.

noncomputable def TauCeti.kummerIso (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) : powerClassQuotient Kˣ n ≃* Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n))

The Kummer isomorphism Kˣ ⧸ (Kˣ)ⁿ ≃* H¹(G_K, μₙ) (NSW (6.2.1) and the display following it), for n invertible in K. It is TauCeti.kummerClassMap, which is injective since the kernel of the Kummer map is (Kˣ)ⁿ and surjective by Hilbert 90.

Equations

• TauCeti.kummerIso K n hn = MulEquiv.ofBijective (TauCeti.kummerClassMap K n hn) ⋯

@[simp]

theorem TauCeti.kummerIso_apply (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) (x : powerClassQuotient Kˣ n) : (kummerIso K n hn) x = (kummerClassMap K n hn) x

The Kummer isomorphism is the Kummer map on power classes.

theorem TauCeti.kummerIso_mk (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) (a : Kˣ) : (kummerIso K n hn) ↑a = (kummerMap K n hn) a

The Kummer isomorphism sends the power class of a to the Kummer class of a.

theorem TauCeti.finite_H1_kummerCoeff (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) [Finite (powerClassQuotient Kˣ n)] : Finite (ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n))

H¹(G_K, μₙ) is finite as soon as Kˣ ⧸ (Kˣ)ⁿ is, for n invertible in K: the two groups are identified by the Kummer isomorphism.

theorem TauCeti.finite_H1_of_isPrimitiveRoot_of_natCard_eq {K : Type u_1} [Field K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) [Finite (powerClassQuotient Kˣ n)] {H : Type u_2} [Group H] [TopologicalSpace H] (φ : AbsoluteGaloisGroup K ≃ₜ* H) (M : Type u_3) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction H M] [ContinuousSMul H M] [IsAddCyclic M] (hM : Nat.card M = n) (htriv : ∀ (h : H) (m : M), h • m = m) : Finite (ContCohomology.H1 H M)

H¹ of a cyclic trivial module over a field containing the roots of unity. Let K be a field containing a primitive nth root of unity and with Kˣ ⧸ (Kˣ)ⁿ finite, and H a topological group isomorphic to G_K. Then H¹(H, M) is finite for every cyclic discrete H-module M of order n with trivial action: such a module is μₙ(Kˢ) (TauCeti.finite_H1_kummerCoeff).

Changing the level of the roots of unity

For m ∣ n, raising to the power n / m maps μₙ onto μₘ. On Kummer classes it is the change of level: an nth root α of a gives the mth root α ^ (n / m) of the same a, and (g α / α) ^ (n / m) = g α ^ (n / m) / α ^ (n / m). As every class at level m is a Kummer class, the induced map on H¹ is surjective.

noncomputable def TauCeti.kummerCoeffPow (K : Type u_1) [Field K] {n m : ℕ} (h : m ∣ n) : KummerCoeff K n →+[AbsoluteGaloisGroup K] KummerCoeff K m

The power map μₙ → μₘ, ζ ↦ ζ ^ (n / m) for m ∣ n, as an equivariant homomorphism of Kummer coefficients. It carries the Kummer class of a at level n to the Kummer class of a at level m (TauCeti.explicitCoeff1_kummerCoeffPow_kummerMap).

Equations

• TauCeti.kummerCoeffPow K h = { toFun := fun (x : TauCeti.KummerCoeff K n) => Additive.ofMul ⟨↑(Additive.toMul x) ^ (n / m), ⋯⟩, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.coe_toMul_kummerCoeffPow {K : Type u_1} [Field K] {n m : ℕ} (h : m ∣ n) (x : KummerCoeff K n) : ↑(Additive.toMul ((kummerCoeffPow K h) x)) = ↑(Additive.toMul x) ^ (n / m)

The power map μₙ → μₘ raises a root of unity to the power n / m.

theorem TauCeti.explicitCoeff1_kummerCoeffPow_kummerMap {K : Type u_1} [Field K] {n : ℕ} (hn : IsUnit ↑n) {m : ℕ} (h : m ∣ n) (a : Kˣ) : (ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) (KummerCoeff K n) (kummerCoeffPow K h) ⋯) (Multiplicative.toAdd ((kummerMap K n hn) a)) = Multiplicative.toAdd ((kummerMap K m ⋯) a)

The power map μₙ → μₘ changes the level of Kummer classes: for m ∣ n, it sends the Kummer class of a in H¹(G_K, μₙ) to the Kummer class of a in H¹(G_K, μₘ).

theorem TauCeti.explicitCoeff1_kummerCoeffPow_surjective {K : Type u_1} [Field K] {n : ℕ} (hn : IsUnit ↑n) {m : ℕ} (h : m ∣ n) : Function.Surjective ⇑(ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) (KummerCoeff K n) (kummerCoeffPow K h) ⋯)

The power map μₙ → μₘ is surjective on H¹ for m ∣ n and n invertible in K: every class of H¹(G_K, μₘ) is the Kummer class of some a ∈ Kˣ, which is the image of the Kummer class of a at level n.

The Kummer map against canonical continuous cohomology

noncomputable def TauCeti.kummerMapCanonical (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) : Kˣ →* Multiplicative ↑(continuousCohomology 1 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (KummerCoeff K n))).toModuleCat

The canonical Kummer map from units of K to Mathlib's continuous cohomology of the Kummer coefficient module. It is the explicit Kummer map transported through the degree-one comparison isomorphism.

Equations

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

@[simp]

theorem TauCeti.explicitIso_kummerMap (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) (a : Kˣ) : Multiplicative.toAdd ((kummerMapCanonical K n hn) a) = (ContCohomology.explicitH1AddEquivContinuousCohomology (AbsoluteGaloisGroup K) (KummerCoeff K n)) (Multiplicative.toAdd ((kummerMap K n hn) a))

The explicit and canonical Kummer maps agree. The degree-one comparison sends the explicit Kummer class of a unit to its canonical continuous-cohomology class.

Transport to another coefficient model

theorem TauCeti.kummerIsoTransportContinuousSMul (K : Type u_1) [Field K] (n : ℕ) (μ : Type u_2) [AddCommGroup μ] [TopologicalSpace μ] [DiscreteTopology μ] [DistribMulAction (AbsoluteGaloisGroup K) μ] (e : KummerCoeff K n ≃+ μ) (hequiv : ∀ (g : AbsoluteGaloisGroup K) (x : KummerCoeff K n), e (g • x) = g • e x) : ContinuousSMul (AbsoluteGaloisGroup K) μ

An equivariant equivalence from the Kummer coefficients to a discrete additive module transports continuity of the Galois action to that module.

noncomputable def TauCeti.kummerIsoTransport (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) (μ : Type u_2) [AddCommGroup μ] [TopologicalSpace μ] [DiscreteTopology μ] [DistribMulAction (AbsoluteGaloisGroup K) μ] (e : KummerCoeff K n ≃+ μ) (hequiv : ∀ (g : AbsoluteGaloisGroup K) (x : KummerCoeff K n), e (g • x) = g • e x) : powerClassQuotient Kˣ n ≃* Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup K) μ)

The Kummer isomorphism transported to another discrete model of μₙ. The identification of coefficients must be G_K-equivariant; a bare additive equivalence would not determine the same Galois module and hence would not induce an equivalence on cohomology.

Equations

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

@[simp]

theorem TauCeti.kummerIsoTransport_apply (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) (μ : Type u_2) [AddCommGroup μ] [TopologicalSpace μ] [DiscreteTopology μ] [DistribMulAction (AbsoluteGaloisGroup K) μ] (e : KummerCoeff K n ≃+ μ) (hequiv : ∀ (g : AbsoluteGaloisGroup K) (x : KummerCoeff K n), e (g • x) = g • e x) (x : powerClassQuotient Kˣ n) : (kummerIsoTransport K n hn μ e hequiv) x = Multiplicative.ofAdd ((ContCohomology.explicitCoeff1Equiv (AbsoluteGaloisGroup K) (KummerCoeff K n) e ⋯ ⋯ hequiv) (Multiplicative.toAdd ((kummerIso K n hn) x)))

Transporting the Kummer isomorphism applies the original Kummer isomorphism and then the coefficient equivalence on H¹.

Restriction along a field extension

noncomputable def TauCeti.kummerCoeffMap (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : KummerCoeff K n →+ KummerCoeff L n

The Kummer coefficients of K as Kummer coefficients of L, along a K-embedding σ : L →ₐ[K] Kˢ: the chosen identification separableClosureRingEquiv K L σ : Lˢ ≃+* Kˢ extending σ, read backwards on the nth roots of unity. It is equivariant for the action of G_L on μₙ(Lˢ) and its action on μₙ(Kˢ) through G_L ≃ₜ* Gal(Kˢ/σ(L)) ≤ G_K (TauCeti.kummerCoeffMap_smul).

Equations

• TauCeti.kummerCoeffMap K n L σ = MonoidHom.toAdditive (restrictRootsOfUnity (TauCeti.separableClosureRingEquiv K L σ).symm n)

@[simp]

theorem TauCeti.toMul_kummerCoeffMap (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : KummerCoeff K n) : ↑(Additive.toMul ((kummerCoeffMap K n L σ) x)) = (Units.map (separableClosureRingEquiv K L σ).symm.toMonoidHom) ↑(Additive.toMul x)

kummerCoeffMap applies the inverse identification of separable closures to a root of unity.

@[simp]

theorem TauCeti.kummerCoeffMap_smul (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (g : AbsoluteGaloisGroup L) (x : KummerCoeff K n) : (kummerCoeffMap K n L σ) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ) g • x) = g • (kummerCoeffMap K n L σ) x

kummerCoeffMap is equivariant along G_L ≃ₜ* Gal(Kˢ/σ(L)): an automorphism g of Lˢ over L acts on μₙ(Kˢ) through its image in the subgroup of G_K fixing σ(L), which is g conjugated by the identification of separable closures. This is the compatibility making (absoluteGaloisGroupEquivFixingSubgroup K L σ, kummerCoeffMap K n L σ) a compatible pair.

noncomputable def TauCeti.kummerRes (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n)) →* Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup L) (KummerCoeff L n))

Restriction on the Kummer H¹ along a K-embedding σ : L →ₐ[K] Kˢ, H¹(G_K, μₙ) → H¹(G_L, μₙ): restriction to the subgroup Gal(Kˢ/σ(L)) ≤ G_K fixing σ(L), followed by the pullback along absoluteGaloisGroupEquivFixingSubgroup K L σ : G_L ≃ₜ* Gal(Kˢ/σ(L)) with the coefficient identification kummerCoeffMap. The embedding is genuine data: without one there is no map G_L → G_K. Written multiplicatively, like TauCeti.kummerIso.

Equations

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

theorem TauCeti.toAdd_kummerRes (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n))) : Multiplicative.toAdd ((kummerRes K n L σ) x) = (ContCohomology.explicitMap1 (↥σ.fieldRange.fixingSubgroup) (KummerCoeff K n) (AbsoluteGaloisGroup L) (KummerCoeff L n) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ)) (kummerCoeffMap K n L σ) ⋯ ⋯) ((ContCohomology.explicitRes1 (AbsoluteGaloisGroup K) (KummerCoeff K n) σ.fieldRange.fixingSubgroup) (Multiplicative.toAdd x))

kummerRes is restriction to the subgroup fixing σ(L) followed by the transport to G_L along absoluteGaloisGroupEquivFixingSubgroup K L σ and kummerCoeffMap.

theorem TauCeti.units_map_separableClosureRingEquiv_symm_pow {K : Type u_1} [Field K] {n : ℕ} {a : Kˣ} {α : (SeparableClosure K)ˣ} {L : Type u_2} [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) : (Units.map (separableClosureRingEquiv K L σ).symm.toMonoidHom) α ^ n = (Units.map ↑(algebraMap L (SeparableClosure L))) ((Units.map ↑(algebraMap K L)) a)

Transporting an nth root to Lˢ: if α ∈ Kˢ is an nth root of a ∈ Kˣ, its image under the identification separableClosureRingEquiv K L σ of separable closures is an nth root of the image of a in Lˣ.

@[simp]

theorem TauCeti.kummerRes_kummerCocycleClass (K : Type u_1) [Field K] (n : ℕ) {a : Kˣ} {α : (SeparableClosure K)ˣ} (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (hα : α ^ n = (Units.map ↑(algebraMap K (SeparableClosure K))) a) : (kummerRes K n L σ) (Multiplicative.ofAdd (kummerCocycleClass hα)) = Multiplicative.ofAdd (kummerCocycleClass ⋯)

Restriction of a Kummer cocycle class: restricting the class of g ↦ g α / α to G_L gives the class of h ↦ h β / β for the image β ∈ Lˢ of the root α under the identification of separable closures.

@[simp]

theorem TauCeti.kummerRes_kummerMap (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (hn : IsUnit ↑n) (a : Kˣ) : (kummerRes K n L σ) ((kummerMap K n hn) a) = (kummerMap L n ⋯) ((Units.map ↑(algebraMap K L)) a)

Restriction of Kummer classes along a field extension: for a K-embedding σ : L →ₐ[K] Kˢ, restriction H¹(G_K, μₙ) → H¹(G_L, μₙ) sends the Kummer class of a ∈ Kˣ to the Kummer class of its image in Lˣ.

@[simp]

theorem TauCeti.kummerIso_res (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (hn : IsUnit ↑n) (x : powerClassQuotient Kˣ n) : (kummerRes K n L σ) ((kummerIso K n hn) x) = (kummerIso L n ⋯) ((powerClassMap n (Units.map ↑(algebraMap K L))) x)

The restriction square of the Kummer isomorphism (NSW, the display after (6.2.1)): for a K-embedding σ : L →ₐ[K] Kˢ, restriction H¹(G_K, μₙ) → H¹(G_L, μₙ) corresponds under the Kummer isomorphisms to the map of power classes Kˣ ⧸ (Kˣ)ⁿ → Lˣ ⧸ (Lˣ)ⁿ induced by K → L. No finiteness of L/K is needed.

Corestriction along a finite extension, and the norm

noncomputable def TauCeti.kummerCoeffMapSymm (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : KummerCoeff L n →+ KummerCoeff K n

The Kummer coefficients of L as Kummer coefficients of K, along a K-embedding σ : L →ₐ[K] Kˢ: the chosen identification separableClosureRingEquiv K L σ : Lˢ ≃+* Kˢ read on the nth roots of unity. It inverts TauCeti.kummerCoeffMap (TauCeti.kummerCoeffMapSymm_kummerCoeffMap) and is the coefficient leg of corestriction, as kummerCoeffMap is the coefficient leg of restriction.

Equations

• TauCeti.kummerCoeffMapSymm K n L σ = MonoidHom.toAdditive (restrictRootsOfUnity (TauCeti.separableClosureRingEquiv K L σ) n)

@[simp]

theorem TauCeti.toMul_kummerCoeffMapSymm (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (y : KummerCoeff L n) : ↑(Additive.toMul ((kummerCoeffMapSymm K n L σ) y)) = (Units.map (separableClosureRingEquiv K L σ).toMonoidHom) ↑(Additive.toMul y)

kummerCoeffMapSymm applies the identification of separable closures to a root of unity.

@[simp]

theorem TauCeti.kummerCoeffMapSymm_kummerCoeffMap (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : KummerCoeff K n) : (kummerCoeffMapSymm K n L σ) ((kummerCoeffMap K n L σ) x) = x

The two coefficient identifications of TauCeti.kummerRes and of TauCeti.kummerCor are inverse to each other.

@[simp]

theorem TauCeti.kummerCoeffMap_kummerCoeffMapSymm (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (y : KummerCoeff L n) : (kummerCoeffMap K n L σ) ((kummerCoeffMapSymm K n L σ) y) = y

The two coefficient identifications of TauCeti.kummerRes and of TauCeti.kummerCor are inverse to each other.

@[simp]

theorem TauCeti.kummerCoeffMapSymm_smul (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (h : ↥σ.fieldRange.fixingSubgroup) (y : KummerCoeff L n) : (kummerCoeffMapSymm K n L σ) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ).symm h • y) = h • (kummerCoeffMapSymm K n L σ) y

kummerCoeffMapSymm is equivariant along the inverse of G_L ≃ₜ* Gal(Kˢ/σ(L)): an automorphism h of Kˢ fixing σ(L) acts on μₙ(Lˢ) through its preimage in G_L. This is the compatible pair corestriction along L/K is assembled from.

noncomputable def TauCeti.unitsCoeffMapSymm (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : UnitsCoeff L →+ UnitsCoeff K

The units of Lˢ as units of Kˢ, along the identification of separable closures. It is the ambient coefficient map of the Kummer sequence for which TauCeti.kummerCoeffMapSymm is the map of nth roots of unity.

Equations

• TauCeti.unitsCoeffMapSymm K L σ = MonoidHom.toAdditive (Units.map (TauCeti.separableClosureRingEquiv K L σ).toMonoidHom)

@[simp]

theorem TauCeti.toMul_unitsCoeffMapSymm (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (y : UnitsCoeff L) : Additive.toMul ((unitsCoeffMapSymm K L σ) y) = (Units.map (separableClosureRingEquiv K L σ).toMonoidHom) (Additive.toMul y)

unitsCoeffMapSymm applies the identification of separable closures to a unit.

@[simp]

theorem TauCeti.unitsCoeffMapSymm_smul (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (h : ↥σ.fieldRange.fixingSubgroup) (y : UnitsCoeff L) : (unitsCoeffMapSymm K L σ) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ).symm h • y) = h • (unitsCoeffMapSymm K L σ) y

unitsCoeffMapSymm is equivariant along the inverse of G_L ≃ₜ* Gal(Kˢ/σ(L)).

noncomputable def TauCeti.unitsCoeffMap (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : UnitsCoeff K →+ UnitsCoeff L

The units of Kˢ as units of Lˢ, along the inverse of the identification of separable closures: the inverse of TauCeti.unitsCoeffMapSymm (unitsCoeffMapSymm_unitsCoeffMap), and the coefficient leg of restriction with unit coefficients, as TauCeti.kummerCoeffMap is for the roots of unity.

Equations

• TauCeti.unitsCoeffMap K L σ = MonoidHom.toAdditive (Units.map (TauCeti.separableClosureRingEquiv K L σ).symm.toMonoidHom)

@[simp]

theorem TauCeti.toMul_unitsCoeffMap (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : UnitsCoeff K) : Additive.toMul ((unitsCoeffMap K L σ) x) = (Units.map (separableClosureRingEquiv K L σ).symm.toMonoidHom) (Additive.toMul x)

unitsCoeffMap applies the inverse identification of separable closures to a unit.

@[simp]

theorem TauCeti.unitsCoeffMap_smul (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (g : AbsoluteGaloisGroup L) (x : UnitsCoeff K) : (unitsCoeffMap K L σ) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ) g • x) = g • (unitsCoeffMap K L σ) x

unitsCoeffMap is equivariant along G_L ≃ₜ* Gal(Kˢ/σ(L)): an automorphism g of Lˢ over L acts on (Kˢ)ˣ through its image in the subgroup of G_K fixing σ(L).

@[simp]

theorem TauCeti.unitsCoeffMapSymm_unitsCoeffMap (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : UnitsCoeff K) : (unitsCoeffMapSymm K L σ) ((unitsCoeffMap K L σ) x) = x

The two coefficient identifications of the units are inverse to each other.

@[simp]

theorem TauCeti.unitsCoeffMap_unitsCoeffMapSymm (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (y : UnitsCoeff L) : (unitsCoeffMap K L σ) ((unitsCoeffMapSymm K L σ) y) = y

The two coefficient identifications of the units are inverse to each other.

@[simp]

theorem TauCeti.unitsCoeffMapSymm_kummerCoeffIncl (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (y : KummerCoeff L n) : (unitsCoeffMapSymm K L σ) ((kummerCoeffIncl L n) y) = (kummerCoeffIncl K n) ((kummerCoeffMapSymm K n L σ) y)

The coefficient maps commute with the inclusion μₙ ↪ (Kˢ)ˣ of the Kummer sequence.

@[simp]

theorem TauCeti.unitsCoeffMapSymm_unitsCoeffPow (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (y : UnitsCoeff L) : (unitsCoeffMapSymm K L σ) ((unitsCoeffPow L n) y) = (unitsCoeffPow K n) ((unitsCoeffMapSymm K L σ) y)

The coefficient map commutes with the nth power map of the Kummer sequence.

@[simp]

theorem TauCeti.unitsCoeffMapSymm_coe_baseUnitsEquivInvariants (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (b : Lˣ) : (unitsCoeffMapSymm K L σ) ↑((baseUnitsEquivInvariants L) (Additive.ofMul b)) = ↑(embeddedUnitsInvariants K L σ b)

The coefficient map carries the invariant of G_L attached to b ∈ Lˣ to the invariant of Gal(Kˢ/σ(L)) attached to b.

theorem TauCeti.explicitCor0_embeddedUnitsInvariants (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (b : Lˣ) : (ContCohomology.explicitCor0 (AbsoluteGaloisGroup K) (UnitsCoeff K) σ.fieldRange.fixingSubgroup) (embeddedUnitsInvariants K L σ b) = (baseUnitsEquivInvariants K) (Additive.ofMul ((Algebra.normUnits K) b))

Degree-zero corestriction on the invariants of (Kˢ)ˣ is the norm of L/K (NSW, Ch. I §5): corestriction from Gal(Kˢ/σ(L)) is the sum over a transversal, which on σ b is the product of the conjugates of σ b, that is the image of N_{L/K} b.

noncomputable def TauCeti.kummerCor (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup L) (KummerCoeff L n)) →* Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n))

Corestriction on the Kummer H¹ along a K-embedding σ : L →ₐ[K] Kˢ of a finite extension, H¹(G_L, μₙ) → H¹(G_K, μₙ): the transport along absoluteGaloisGroupEquivFixingSubgroup K L σ : G_L ≃ₜ* Gal(Kˢ/σ(L)) with the coefficient identification kummerCoeffMapSymm, followed by corestriction from the open subgroup Gal(Kˢ/σ(L)), whose index is [L : K]. Finiteness of L/K is what makes that corestriction exist; restriction (TauCeti.kummerRes) needs none. Written multiplicatively, like TauCeti.kummerIso.

Equations

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

theorem TauCeti.toAdd_kummerCor (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (y : Multiplicative (ContCohomology.H1 (AbsoluteGaloisGroup L) (KummerCoeff L n))) : Multiplicative.toAdd ((kummerCor K n L σ) y) = (ContCohomology.explicitCor1 (AbsoluteGaloisGroup K) (KummerCoeff K n) σ.fieldRange.fixingSubgroup ⋯) ((ContCohomology.explicitMap1 (AbsoluteGaloisGroup L) (KummerCoeff L n) (↥σ.fieldRange.fixingSubgroup) (KummerCoeff K n) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ).symm) (kummerCoeffMapSymm K n L σ) ⋯ ⋯) (Multiplicative.toAdd y))

kummerCor transports a class to the subgroup fixing σ(L) and corestricts it to G_K.

@[simp]

theorem TauCeti.kummerCor_kummerMap (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (hn : IsUnit ↑n) (b : Lˣ) : (kummerCor K n L σ) ((kummerMap L n hn) b) = (kummerMap K n ⋯) ((Algebra.normUnits K) b)

Corestriction of a Kummer class along a field extension: for a K-embedding σ : L →ₐ[K] Kˢ of a finite extension, corestriction H¹(G_L, μₙ) → H¹(G_K, μₙ) sends the Kummer class of b ∈ Lˣ to the Kummer class of its norm N_{L/K} b ∈ Kˣ.

@[simp]

theorem TauCeti.kummerIso_norm (K : Type u_1) [Field K] (n : ℕ) (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (hn : IsUnit ↑n) (x : powerClassQuotient Lˣ n) : (kummerCor K n L σ) ((kummerIso L n hn) x) = (kummerIso K n ⋯) ((powerClassMap n (Algebra.normUnits K)) x)

The norm square of the Kummer isomorphism (NSW, the display after (6.2.1)): for a K-embedding σ : L →ₐ[K] Kˢ of a finite extension, corestriction H¹(G_L, μₙ) → H¹(G_K, μₙ) corresponds under the Kummer isomorphisms to the map of power classes Lˣ ⧸ (Lˣ)ⁿ → Kˣ ⧸ (Kˣ)ⁿ induced by the norm N_{L/K}.