The roots of unity as a coefficient object, and the transported Kummer isomorphism

Local class field theory writes its Galois cohomology with ZMod n coefficients on Mathlib's carrier: a coefficient object is an object of TopRep (ZMod n) G_F for G_F = Field.absoluteGaloisGroup F, the automorphism group of an algebraic closure, and its cohomology is Mathlib's continuousCohomology. This file supplies the coefficient object μₙ, the nth roots of unity, and moves the Kummer isomorphism onto it.

The roots of unity themselves are those of the separable closure, μₙ = μₙ(Fˢ), that is the module TauCeti.KummerCoeff F n on which TauCeti.AbsoluteGaloisGroup F = Gal(Fˢ/F) acts and for which the Kummer isomorphism TauCeti.kummerIso is proved. Field.absoluteGaloisGroup F acts on it through the restriction isomorphism TauCeti.absoluteGaloisGroupRestrictEquiv, an isomorphism because the algebraic closure is purely inseparable over Fˢ, and μₙ is a ZMod n-module because it is killed by n. The result is muNRep n F. Its underlying module is related to TauCeti.KummerCoeff F n only through the additive equivalence kummerCoeffEquivMuNRep, whose defining property is that it intertwines the action of σ on muNRep n F with the action of its restriction to Fˢ (kummerCoeffEquivMuNRep_smul); both modules are discrete.

Pullback along the restriction isomorphism, the degree-one comparison of explicit and canonical continuous cohomology, and the fact that continuous cohomology does not see the scalars assemble into muNRepH1Equiv : H¹(Gal(Fˢ/F), μₙ) ≃+ H¹(G_F, muNRep n F). Composing it with the Kummer isomorphism gives kummerEquiv : Fˣ ⧸ (Fˣ)ⁿ ≃+ H¹(G_F, muNRep n F) for n invertible in F, and kummerClass is the Kummer class of a unit in this carrier. It is the transport of the Kummer map TauCeti.kummerMap, not a second Kummer cocycle, and is represented by g ↦ g α / α for any nth root α of the unit (kummerClass_eq_muNRepH1Equiv_kummerCocycleClass). The degree-two comparison gives muNRepH2Equiv : H²(Gal(Fˢ/F), μₙ) ≃+ H²(G_F, muNRep n F) in the same way.

In characteristic zero every n ≠ 0 is invertible, so the Kummer equivalence kummerEquivOfCharZero holds for every n ≠ 0. This covers every finite extension of ℚ_p, including the exponents n divisible by p, which are units of the field but not of its valuation ring.

The name kummerClass here is TauCeti.ClassFieldTheory.kummerClass; it is not the mod-two Kummer class TauCeti.kummerClass, which lives in the trivial 𝔽₂ coefficient object of TauCeti.AbsoluteGaloisGroup.

When F contains a chosen primitive nth root of unity ζ, the action of G_F on μₙ is trivial. The coordinate muNRepEquivZMod sends the chosen generator muNRepGenerator to 1, and muNRepEquivTrivialFp identifies μₙ with the trivial coefficients ℤ/n, sending ζ to 1. As an isomorphism of coefficient objects, muNRepIsoTrivialFp, it induces muNRepCohomologyEquivTrivialFp, comparing the cohomology of μₙ with that of ℤ/n in every degree; in degrees one and two it is the pullback of explicit cocycles. In degree one, kummerEquivTrivialFp identifies nth-power classes with H¹(G_F, ℤ/n) for the trivial action. This works for arbitrary nonzero n, without a finiteness assumption, and yields the corresponding cardinality equality.

Main definitions

• TauCeti.ClassFieldTheory.GalRep n F: coefficient objects TopRep (ZMod n) G_F.
• TauCeti.ClassFieldTheory.muNRep n F: the roots of unity μₙ(Fˢ) as a coefficient object.
• TauCeti.ClassFieldTheory.kummerCoeffEquivMuNRep: the identification of its underlying module with TauCeti.KummerCoeff F n.
• TauCeti.ClassFieldTheory.muNRepH1Equiv: H¹(Gal(Fˢ/F), μₙ) ≃+ H¹(G_F, muNRep n F).
• TauCeti.ClassFieldTheory.muNRepH2Equiv: H²(Gal(Fˢ/F), μₙ) ≃+ H²(G_F, muNRep n F).
• TauCeti.ClassFieldTheory.kummerEquiv, TauCeti.ClassFieldTheory.kummerEquivOfCharZero: the Kummer isomorphism Fˣ ⧸ (Fˣ)ⁿ ≃+ H¹(G_F, muNRep n F), for n invertible in F and for n ≠ 0 in characteristic zero.
• TauCeti.ClassFieldTheory.kummerClass: the Kummer class of a unit in H¹(G_F, muNRep n F).
• TauCeti.ClassFieldTheory.muNRepEquivZMod: the chosen-root coordinate on μₙ.
• TauCeti.ClassFieldTheory.muNRepGenerator: the root with chosen coordinate 1.
• TauCeti.ClassFieldTheory.muNRepEquivTrivialFp: the identification of μₙ with trivial ℤ/n coefficients determined by a primitive nth root of unity in F.
• TauCeti.ClassFieldTheory.muNRepIsoTrivialFp: the same identification as an isomorphism of coefficient objects.
• TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp: its transport to Hᵈ in every degree d.
• TauCeti.ClassFieldTheory.kummerEquivTrivialFp: the Kummer isomorphism with trivial ℤ/n coefficients, given a primitive nth root of unity in F.

Main results

• TauCeti.ClassFieldTheory.kummerCoeffEquivMuNRep_smul: the dictionary is equivariant along the restriction isomorphism.
• TauCeti.ClassFieldTheory.continuous_kummerCoeffEquivMuNRep, TauCeti.ClassFieldTheory.continuous_kummerCoeffEquivMuNRep_symm: the dictionary and its inverse are continuous.
• TauCeti.ClassFieldTheory.isSmoothDiscrete_muNRep: muNRep n F is a smooth discrete coefficient object.
• TauCeti.ClassFieldTheory.muNRep_ρ_apply_eq_self: G_F acts trivially on muNRep n F when F contains a primitive nth root of unity.
• TauCeti.ClassFieldTheory.baer_muNRep: muNRep n F is an injective ZMod n-module when n is invertible in F.
• TauCeti.ClassFieldTheory.kummerClass_eq_muNRepH1Equiv_kummerCocycleClass: the Kummer class of a is the transported class of g ↦ g α / α, for any nth root α of a.
• TauCeti.ClassFieldTheory.kummerClass_eq_zero_iff: the Kummer class of a vanishes exactly when a is an nth power.
• TauCeti.ClassFieldTheory.kummerClass_surjective: every class of H¹(G_F, muNRep n F) is a Kummer class.

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 Kummer isomorphism.

The coefficient object μₙ

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.GalRep (n : ℕ) (F : Type u) [Field F] : Type (u + 1)

Coefficient objects for the absolute Galois group with ZMod n scalars: topological representations of G_F = Field.absoluteGaloisGroup F over ZMod n, on which Mathlib's continuousCohomology is defined.

Equations

• TauCeti.ClassFieldTheory.GalRep n F = TopRep (ZMod n) (Field.absoluteGaloisGroup F)

noncomputable def TauCeti.ClassFieldTheory.muNRep (n : ℕ) (F : Type u) [Field F] : GalRep n F

The nth roots of unity μₙ(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; kummerCoeffEquivMuNRep identifies the underlying module with TauCeti.KummerCoeff F n.

Equations

• TauCeti.ClassFieldTheory.muNRep n F = TopRep.res (↑(TauCeti.absoluteGaloisGroupRestrictEquiv F)) (TauCeti.ofDiscreteModule (ZMod n) (TauCeti.AbsoluteGaloisGroup F) (TauCeti.KummerCoeff F n))

instance TauCeti.ClassFieldTheory.instDiscreteTopologyVZModAbsoluteGaloisGroupMuNRep (n : ℕ) (F : Type u) [Field F] : DiscreteTopology ↑(muNRep n F)

μₙ carries the discrete topology.

noncomputable def TauCeti.ClassFieldTheory.kummerCoeffEquivMuNRep (n : ℕ) (F : Type u) [Field F] : KummerCoeff F n ≃+ ↑(muNRep n F)

The coefficient dictionary between the Kummer coefficient module TauCeti.KummerCoeff F n of Gal(Fˢ/F) and the underlying module of muNRep n F. It and its inverse are continuous (continuous_kummerCoeffEquivMuNRep, continuous_kummerCoeffEquivMuNRep_symm), and it is equivariant along the restriction isomorphism by kummerCoeffEquivMuNRep_smul.

Equations

• TauCeti.ClassFieldTheory.kummerCoeffEquivMuNRep n F = AddEquiv.refl (TauCeti.KummerCoeff F n)

theorem TauCeti.ClassFieldTheory.continuous_kummerCoeffEquivMuNRep (n : ℕ) (F : Type u) [Field F] : Continuous ⇑(kummerCoeffEquivMuNRep n F)

The coefficient dictionary is continuous, TauCeti.KummerCoeff F n being discrete.

theorem TauCeti.ClassFieldTheory.continuous_kummerCoeffEquivMuNRep_symm (n : ℕ) (F : Type u) [Field F] : Continuous ⇑(kummerCoeffEquivMuNRep n F).symm

The inverse of the coefficient dictionary is continuous, muNRep n F being discrete.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerCoeffEquivMuNRep_smul (n : ℕ) (F : Type u) [Field F] (g : Field.absoluteGaloisGroup F) (x : KummerCoeff F n) : (kummerCoeffEquivMuNRep n F) ((absoluteGaloisGroupRestrictEquiv F) g • x) = ((muNRep n F).ρ g) ((kummerCoeffEquivMuNRep n F) x)

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

theorem TauCeti.ClassFieldTheory.isSmoothDiscrete_muNRep (n : ℕ) (F : Type u) [Field F] : IsSmoothDiscrete (ZMod n) (muNRep n F)

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

instance TauCeti.ClassFieldTheory.instContinuousSMulAbsoluteGaloisGroupVZModMuNRep (n : ℕ) (F : Type u) [Field F] : ContinuousSMul (Field.absoluteGaloisGroup F) ↑(muNRep n F)

The action of G_F on μₙ is continuous, μₙ being smooth discrete.

theorem TauCeti.ClassFieldTheory.muNRep_ρ_apply_eq_self {n : ℕ} {F : Type u} [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (g : Field.absoluteGaloisGroup F) (x : ↑(muNRep n F)) : ((muNRep n F).ρ g) x = x

G_F acts trivially on μₙ when F contains a primitive nth root of unity, by TauCeti.smul_kummerCoeff_eq_self read through the coefficient dictionary.

theorem TauCeti.ClassFieldTheory.baer_muNRep {n : ℕ} {F : Type u} [Field F] (hn : IsUnit ↑n) : Module.Baer (ZMod n) ↑(muNRep n F)

μₙ is an injective ZMod n-module for n invertible in F, in the form of Baer's criterion: μₙ is then cyclic of order n (TauCeti.kummerCoeffAddEquivZMod), and ℤ/nℤ is self-injective (Module.Baer.zmod_self). Consequently Hom(-, μₙ) is exact on the modules killed by n (TauCeti.InternalHom.precomp_surjective_of_baer).

Transport of H¹

noncomputable def TauCeti.ClassFieldTheory.muNRepH1Equiv (n : ℕ) (F : Type u) [Field F] : ContCohomology.H1 (AbsoluteGaloisGroup F) (KummerCoeff F n) ≃+ ↑(continuousCohomology 1 (muNRep n F)).toModuleCat

H¹ of μₙ transported to the coefficient object muNRep n F: pullback along the restriction isomorphism G_F ≃ Gal(Fˢ/F) and the coefficient dictionary, followed by the comparison of explicit and canonical continuous cohomology, and by forgetting the ZMod n scalars, which continuous cohomology does not see.

Equations

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

theorem TauCeti.ClassFieldTheory.muNRepH1Equiv_apply (n : ℕ) (F : Type u) [Field F] (x : ContCohomology.H1 (AbsoluteGaloisGroup F) (KummerCoeff F n)) : (muNRepH1Equiv n F) x = (TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete (muNRep n F)) ((ContCohomology.explicitMap1 (AbsoluteGaloisGroup F) (KummerCoeff F n) (Field.absoluteGaloisGroup F) (↑(muNRep n F)) (↑(absoluteGaloisGroupRestrictEquiv F)) (kummerCoeffEquivMuNRep n F).toAddMonoidHom ⋯ ⋯) x)

muNRepH1Equiv is the pullback along the restriction isomorphism and the coefficient dictionary, followed by the degree-one comparison for the discrete object muNRep n F.

Transport of H²

noncomputable def TauCeti.ClassFieldTheory.muNRepH2Equiv (n : ℕ) (F : Type u) [Field F] : ContCohomology.H2 (AbsoluteGaloisGroup F) (KummerCoeff F n) ≃+ ↑(continuousCohomology 2 (muNRep n F)).toModuleCat

H² of μₙ transported to muNRep n F. This is pullback along absoluteGaloisGroupRestrictEquiv, the coefficient dictionary kummerCoeffEquivMuNRep, and the comparison between explicit and canonical continuous cohomology.

Equations

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

theorem TauCeti.ClassFieldTheory.muNRepH2Equiv_apply (n : ℕ) (F : Type u) [Field F] (x : ContCohomology.H2 (AbsoluteGaloisGroup F) (KummerCoeff F n)) : (muNRepH2Equiv n F) x = (TopRep.explicitH2AddEquivContinuousCohomologyOfDiscrete (muNRep n F)) ((ContCohomology.explicitMap2 (AbsoluteGaloisGroup F) (KummerCoeff F n) (Field.absoluteGaloisGroup F) (↑(muNRep n F)) (↑(absoluteGaloisGroupRestrictEquiv F)) (kummerCoeffEquivMuNRep n F).toAddMonoidHom ⋯ ⋯) x)

muNRepH2Equiv is the degree-two explicit transport followed by the comparison with Mathlib's canonical continuous cohomology.

The Kummer isomorphism on muNRep n F

noncomputable def TauCeti.ClassFieldTheory.kummerEquiv {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) : Additive (powerClassQuotient Fˣ n) ≃+ ↑(continuousCohomology 1 (muNRep n F)).toModuleCat

The Kummer isomorphism Fˣ ⧸ (Fˣ)ⁿ ≃+ H¹(G_F, μₙ) on the coefficient object muNRep n F, for n invertible in F: the Kummer isomorphism TauCeti.kummerIso followed by muNRepH1Equiv.

Equations

• TauCeti.ClassFieldTheory.kummerEquiv F hn = (MulEquiv.toAdditiveLeft (TauCeti.kummerIso F n hn)).trans (TauCeti.ClassFieldTheory.muNRepH1Equiv n F)

theorem TauCeti.ClassFieldTheory.kummerEquiv_apply {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) (x : Additive (powerClassQuotient Fˣ n)) : (kummerEquiv F hn) x = (muNRepH1Equiv n F) (Multiplicative.toAdd ((kummerIso F n hn) (Additive.toMul x)))

kummerEquiv is the Kummer isomorphism TauCeti.kummerIso transported by muNRepH1Equiv.

noncomputable def TauCeti.ClassFieldTheory.kummerClass {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) (a : Fˣ) : ↑(continuousCohomology 1 (muNRep n F)).toModuleCat

The Kummer class of a unit a of F in H¹(G_F, μₙ), on the coefficient object muNRep n F, for n invertible in F: the image of the power class of a under kummerEquiv.

Equations

• TauCeti.ClassFieldTheory.kummerClass F hn a = (TauCeti.ClassFieldTheory.kummerEquiv F hn) (Additive.ofMul ((TauCeti.powerClassHom Fˣ n) a))

@[simp]

theorem TauCeti.ClassFieldTheory.kummerEquiv_ofMul_mk {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) (a : Fˣ) : (kummerEquiv F hn) (Additive.ofMul ↑a) = kummerClass F hn a

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

theorem TauCeti.ClassFieldTheory.kummerClass_eq_muNRepH1Equiv_kummerMap {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) (a : Fˣ) : kummerClass F hn a = (muNRepH1Equiv n F) (Multiplicative.toAdd ((kummerMap F n hn) a))

The Kummer class is the transported Kummer map: it is TauCeti.kummerMap read through muNRepH1Equiv.

theorem TauCeti.ClassFieldTheory.kummerClass_eq_muNRepH1Equiv_kummerCocycleClass {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) {a : Fˣ} {α : (SeparableClosure F)ˣ} (hα : α ^ n = (Units.map ↑(algebraMap F (SeparableClosure F))) a) : kummerClass F hn a = (muNRepH1Equiv n F) (kummerCocycleClass hα)

The Kummer class of a is represented by g ↦ g α / α, transported to muNRep n F, for any nth root α of a in Fˢ.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerClass_one {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) : kummerClass F hn 1 = 0

The Kummer class of 1 is zero.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerClass_mul {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) (a b : Fˣ) : kummerClass F hn (a * b) = kummerClass F hn a + kummerClass F hn b

The Kummer class turns products into sums.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerClass_inv {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) (a : Fˣ) : kummerClass F hn a⁻¹ = -kummerClass F hn a

The Kummer class turns inverses into negatives.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerClass_div {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) (a b : Fˣ) : kummerClass F hn (a / b) = kummerClass F hn a - kummerClass F hn b

The Kummer class turns quotients into differences.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerClass_pow {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) (a : Fˣ) (k : ℕ) : kummerClass F hn (a ^ k) = k • kummerClass F hn a

The Kummer class turns powers into multiples.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerClass_zpow {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) (a : Fˣ) (k : ℤ) : kummerClass F hn (a ^ k) = k • kummerClass F hn a

The Kummer class turns integer powers into integer multiples.

theorem TauCeti.ClassFieldTheory.kummerClass_eq_zero_iff {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) {a : Fˣ} : kummerClass F hn a = 0 ↔ a ∈ powerSubgroup Fˣ n

The Kummer class of a vanishes exactly when a is an nth power in F.

theorem TauCeti.ClassFieldTheory.kummerClass_surjective {n : ℕ} (F : Type u) [Field F] (hn : IsUnit ↑n) : Function.Surjective (kummerClass F hn)

Every class of H¹(G_F, μₙ) is a Kummer class, n being invertible in F.

noncomputable def TauCeti.ClassFieldTheory.kummerEquivOfCharZero {n : ℕ} (F : Type u) [Field F] [CharZero F] (hn : n ≠ 0) : Additive (powerClassQuotient Fˣ n) ≃+ ↑(continuousCohomology 1 (muNRep n F)).toModuleCat

The Kummer isomorphism in characteristic zero, valid for every n ≠ 0. This covers every finite extension F of ℚ_p and every exponent, including those divisible by p, which are units of F but not of its valuation ring.

Equations

• TauCeti.ClassFieldTheory.kummerEquivOfCharZero F hn = TauCeti.ClassFieldTheory.kummerEquiv F ⋯

theorem TauCeti.ClassFieldTheory.kummerEquivOfCharZero_apply {n : ℕ} (F : Type u) [Field F] [CharZero F] (hn : n ≠ 0) (x : Additive (powerClassQuotient Fˣ n)) : (kummerEquivOfCharZero F hn) x = (kummerEquiv F ⋯) x

The characteristic-zero Kummer isomorphism is kummerEquiv at the unit (n : F).

@[simp]

theorem TauCeti.ClassFieldTheory.kummerEquivOfCharZero_ofMul_mk {n : ℕ} (F : Type u) [Field F] [CharZero F] (hn : n ≠ 0) (a : Fˣ) : (kummerEquivOfCharZero F hn) (Additive.ofMul ↑a) = kummerClass F ⋯ a

The characteristic-zero Kummer isomorphism sends the power class of a to the Kummer class of a.

Kummer theory with trivial coefficients

noncomputable def TauCeti.ClassFieldTheory.muNRepEquivTrivialFp (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) : ↑(muNRep n F) ≃+ ↑(trivialFp n (Field.absoluteGaloisGroup F))

The coefficient identification μₙ ≃ ℤ/n of a primitive root: a primitive nth root of unity ζ ∈ F identifies μₙ with the trivial coefficients ℤ/n, sending ζ ^ i to the class of i (coe_kummerCoeffEquivMuNRep_symm_muNRepEquivTrivialFp_symm_natCast). It is equivariant (muNRepEquivTrivialFp_smul) because G_F fixes ζ and hence acts trivially on μₙ.

Equations

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

theorem TauCeti.ClassFieldTheory.coe_kummerCoeffEquivMuNRep_symm_muNRepEquivTrivialFp_symm_natCast (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (i : ℕ) : ↑↑(Additive.toMul ((kummerCoeffEquivMuNRep n F).symm ((muNRepEquivTrivialFp n F hζ).symm ((trivialFpEquiv n (Field.absoluteGaloisGroup F)).symm ↑i)))) = (algebraMap F (SeparableClosure F)) ζ ^ i

The coefficient identification of a primitive root ζ sends ζ ^ i to the class of i: read back in μₙ(Fˢ), the class of i is the image of ζ ^ i.

noncomputable def TauCeti.ClassFieldTheory.muNRepEquivZMod {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) : ↑(muNRep n F) ≃+ ZMod n

The additive coordinate on μₙ selected by the primitive root ζ, sending ζ to 1.

Equations

• TauCeti.ClassFieldTheory.muNRepEquivZMod ζ hζ = (TauCeti.ClassFieldTheory.muNRepEquivTrivialFp n F hζ).trans (TauCeti.trivialFpEquiv n (Field.absoluteGaloisGroup F)).toAddEquiv

theorem TauCeti.ClassFieldTheory.muNRepEquivZMod_apply {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) (x : ↑(muNRep n F)) : (muNRepEquivZMod ζ hζ) x = (trivialFpEquiv n (Field.absoluteGaloisGroup F)) ((muNRepEquivTrivialFp n F hζ) x)

The chosen-root coordinate is the trivial-coefficient identification, read in ZMod n.

theorem TauCeti.ClassFieldTheory.muNRepEquivZMod_symm_apply {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) (c : ZMod n) : (muNRepEquivZMod ζ hζ).symm c = (muNRepEquivTrivialFp n F hζ).symm ((trivialFpEquiv n (Field.absoluteGaloisGroup F)).symm c)

The inverse chosen-root coordinate is the inverse trivial-coefficient identification.

noncomputable def TauCeti.ClassFieldTheory.muNRepGenerator {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) : ↑(muNRep n F)

The chosen primitive root, as the element of μₙ with coordinate 1.

Equations

• TauCeti.ClassFieldTheory.muNRepGenerator ζ hζ = (TauCeti.ClassFieldTheory.muNRepEquivZMod ζ hζ).symm 1

@[simp]

theorem TauCeti.ClassFieldTheory.muNRepEquivZMod_generator {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) : (muNRepEquivZMod ζ hζ) (muNRepGenerator ζ hζ) = 1

The chosen primitive root has coordinate 1.

theorem TauCeti.ClassFieldTheory.muNRepEquivTrivialFp_smul (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (g : Field.absoluteGaloisGroup F) (x : ↑(muNRep n F)) : (muNRepEquivTrivialFp n F hζ) (g • x) = g • (muNRepEquivTrivialFp n F hζ) x

The coefficient identification of a primitive root intertwines the action of G_F on μₙ with the trivial action on ℤ/n.

@[simp]

theorem TauCeti.ClassFieldTheory.muNRepEquivTrivialFp_ρ_apply (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (g : Field.absoluteGaloisGroup F) (x : ↑(muNRep n F)) : (muNRepEquivTrivialFp n F hζ) (((muNRep n F).ρ g) x) = (muNRepEquivTrivialFp n F hζ) x

The coefficient identification of a primitive root is invariant under the action of G_F on μₙ, which is trivial. This is the simp-normal form of muNRepEquivTrivialFp_smul.

noncomputable def TauCeti.ClassFieldTheory.muNRepIsoTrivialFp (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) : muNRep n F ≅ trivialFp n (Field.absoluteGaloisGroup F)

The coefficient isomorphism μₙ ≅ ℤ/n of a primitive root as coefficient objects: the identification muNRepEquivTrivialFp packaged as an isomorphism of topological representations, continuous because both sides are discrete and equivariant because G_F acts trivially on both (muNRep_ρ_apply_eq_self).

Equations

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

@[simp]

theorem TauCeti.ClassFieldTheory.muNRepIsoTrivialFp_hom_apply (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (x : ↑(muNRep n F)) : (CategoryTheory.ConcreteCategory.hom (muNRepIsoTrivialFp n F hζ).hom) x = (muNRepEquivTrivialFp n F hζ) x

The coefficient isomorphism of a primitive root acts on elements as the coefficient identification muNRepEquivTrivialFp.

@[simp]

theorem TauCeti.ClassFieldTheory.muNRepIsoTrivialFp_inv_apply (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (x : ↑(trivialFp n (Field.absoluteGaloisGroup F))) : (CategoryTheory.ConcreteCategory.hom (muNRepIsoTrivialFp n F hζ).inv) x = (muNRepEquivTrivialFp n F hζ).symm x

The inverse coefficient isomorphism of a primitive root acts on elements as the inverse of the coefficient identification muNRepEquivTrivialFp.

noncomputable def TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (d : ℕ) : ↑(continuousCohomology d (muNRep n F)).toModuleCat ≃ₗ[ZMod n] ↑(cohomFp n (Field.absoluteGaloisGroup F) d).toModuleCat

The coefficient transport from μₙ to trivial ℤ/n coefficients in every degree: the image of the coefficient isomorphism muNRepIsoTrivialFp of the chosen primitive root under H^d(G_F, -). The chosen root is identified with 1 : ZMod n.

Equations

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

theorem TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp_apply (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (d : ℕ) (x : ↑(continuousCohomology d (muNRep n F)).toModuleCat) : (muNRepCohomologyEquivTrivialFp n F hζ d) x = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (muNRepIsoTrivialFp n F hζ).hom d)) x

The coefficient transport is the coefficient map coeffMap of the coefficient isomorphism muNRepIsoTrivialFp.

theorem TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp_symm_apply (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (d : ℕ) (x : ↑(cohomFp n (Field.absoluteGaloisGroup F) d).toModuleCat) : (muNRepCohomologyEquivTrivialFp n F hζ d).symm x = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (muNRepIsoTrivialFp n F hζ).inv d)) x

The inverse coefficient transport is the coefficient map coeffMap of the inverse of the coefficient isomorphism muNRepIsoTrivialFp.

theorem TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp_one_apply (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (x : ↑(continuousCohomology 1 (muNRep n F)).toModuleCat) : (muNRepCohomologyEquivTrivialFp n F hζ 1) x = (trivialFp n (Field.absoluteGaloisGroup F)).explicitH1AddEquivContinuousCohomologyOfDiscrete ((ContCohomology.explicitMap1 (Field.absoluteGaloisGroup F) (↑(muNRep n F)) (Field.absoluteGaloisGroup F) (↑(trivialFp n (Field.absoluteGaloisGroup F))) (↑(ContinuousMulEquiv.refl (Field.absoluteGaloisGroup F))) (muNRepEquivTrivialFp n F hζ).toAddMonoidHom ⋯ ⋯) ((TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete (muNRep n F)).symm x))

In degree one, the coefficient transport is the pullback of explicit cocycles along the coefficient identification muNRepEquivTrivialFp of the chosen primitive root.

theorem TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp_two_apply (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (x : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat) : (muNRepCohomologyEquivTrivialFp n F hζ 2) x = (trivialFp n (Field.absoluteGaloisGroup F)).explicitH2AddEquivContinuousCohomologyOfDiscrete ((ContCohomology.explicitMap2 (Field.absoluteGaloisGroup F) (↑(muNRep n F)) (Field.absoluteGaloisGroup F) (↑(trivialFp n (Field.absoluteGaloisGroup F))) (↑(ContinuousMulEquiv.refl (Field.absoluteGaloisGroup F))) (muNRepEquivTrivialFp n F hζ).toAddMonoidHom ⋯ ⋯) ((TopRep.explicitH2AddEquivContinuousCohomologyOfDiscrete (muNRep n F)).symm x))

In degree two, the coefficient transport is the pullback of explicit cocycles along the coefficient identification muNRepEquivTrivialFp of the chosen primitive root.

noncomputable def TauCeti.ClassFieldTheory.kummerEquivTrivialFp (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) : Additive (powerClassQuotient Fˣ n) ≃+ ↑(cohomFp n (Field.absoluteGaloisGroup F) 1).toModuleCat

Given a primitive nth root of unity in F, the Kummer isomorphism identifies the nth-power classes with H¹(G_F, ℤ/n) for the trivial action. The coefficient identification sends the chosen root to 1 : ZMod n. No finiteness assumption is required.

Equations

• TauCeti.ClassFieldTheory.kummerEquivTrivialFp n F hζ = (TauCeti.ClassFieldTheory.kummerEquiv F ⋯).trans (TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp n F hζ 1).toAddEquiv

@[simp]

theorem TauCeti.ClassFieldTheory.kummerEquivTrivialFp_ofMul_mk (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (a : Fˣ) : (kummerEquivTrivialFp n F hζ) (Additive.ofMul ↑a) = (muNRepCohomologyEquivTrivialFp n F hζ 1) (kummerClass F ⋯ a)

The trivial-coefficient Kummer equivalence sends the power class of a to its μₙ Kummer class transported by the coefficient identification determined by the chosen root.

theorem TauCeti.ClassFieldTheory.natCard_cohomFp_one_absoluteGaloisGroup_of_isPrimitiveRoot (n : ℕ) (F : Type u) [Field F] [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) : Nat.card ↑(cohomFp n (Field.absoluteGaloisGroup F) 1).toModuleCat = Nat.card (powerClassQuotient Fˣ n)

If F contains a primitive nth root, the cardinality of H¹(G_F, ℤ/n) equals the number of nth-power classes. This equality of Nat.card also holds when both groups are infinite; it does not assert finiteness.