The μ₂ coefficients as trivial F₂ coefficients #
Let K be a field with [Invertible (2 : K)] and G_K = AbsoluteGaloisGroup K. This file
identifies the Kummer coefficient module μ₂ = μ₂(Kˢ) of TauCeti.Kummer with the trivial 𝔽₂
coefficient object TauCeti.trivialF2 G_K of the profinite-cohomology layer.
The identification is elementary: an element of μ₂ is a root of unity ζ of a separable closure
with ζ ^ 2 = 1, so ζ is ±1, and ±1 ∈ K, so the Galois action on μ₂ is trivial
(TauCeti.mu2_smul_eq_self). The value dictionary TauCeti.mu2EquivZMod2 is the specialization of
the general roots-of-unity dictionary IsPrimitiveRoot.zmodEquivRootsOfUnity of
TauCeti.RingTheory.RootsOfUnity.ZMod at the primitive root -1, which is primitive at every
characteristic other than 2 (IsPrimitiveRoot.neg_one); it sends 0 to 0 and -1 to 1,
and its type pins it, because ZMod 2 has no additive self-equivalence other than the identity,
so sending 0 to 0 already determines it.
Crossed with the universe lift of TauCeti.trivialF2Equiv, the value dictionary is an
isomorphism of coefficient objects TauCeti.kummerCoeffIsoTrivialF2 from the KummerCoeff K 2
object of TopRep ℤ G_K to the trivial 𝔽₂ object, which is the coefficient object that
degree-one continuous cohomology is written against here. Nothing here is specific to local
fields: the action on μ₂ is trivial over every field, and the hypothesis
[Invertible (2 : K)] is what makes 1 and -1 distinct, so that μ₂ has two elements and the
dictionary with ZMod 2 exists at all. Over a field of characteristic 2 the second roots of
unity are the single element 1 = -1, which ZMod 2 is not.
The Kummer class (a) ∈ H¹(G_K, 𝔽₂) of a unit a is read in that trivial carrier, and
TauCeti.kummerSquareClassEquiv identifies the square-class group Kˣ ⧸ (Kˣ)² with it by sending
the class of a to (a).
Main definitions #
TauCeti.mu2NegOne: the element ofμ₂represented by-1, that is-1read as a2nd root of unity; it is the nontrivial element ofμ₂when[Invertible (2 : K)]holds.TauCeti.mu2EquivZMod2: the value dictionaryμ₂ ≃+ ZMod 2.TauCeti.kummerCoeffEquiv: the same dictionary, crossed with the universe lift, as an additive equivalence of the coefficient carriersKummerCoeff K 2 ≃+ (trivialF2 G_K).V.TauCeti.kummerCoeffIsoTrivialF2: the isomorphism of coefficient objectsofDiscreteModule ℤ G_K (KummerCoeff K 2) ≅ trivialF2 G_K, whose application rulesTauCeti.kummerCoeffIsoTrivialF2_hom_applyandTauCeti.kummerCoeffIsoTrivialF2_inv_applyare the value dictionary and its inverse.TauCeti.kummerClass: the Kummer class(a) ∈ H¹(G_K, 𝔽₂)of a unit, read in thetrivialF2 G_Kcarrier.TauCeti.kummerCocycleModTwoandTauCeti.kummerCocycleModTwoClass: the explicit𝔽₂-valued Kummer cocycle of a chosen square root and its cohomology class.TauCeti.kummerSquareClassEquiv: the Kummer isomorphism on the square-class groupKˣ ⧸ (Kˣ)², an additive equivalence withH¹(G_K, 𝔽₂).
Main results #
TauCeti.toMul_eq_one_or_neg_oneandTauCeti.eq_zero_or_eq_mu2NegOne: the2nd roots of unity of a separable closure are1and-1, so an element ofμ₂is0ormu2NegOne.TauCeti.mu2NegOne_ne_zero: the two elements ofμ₂are distinct, because2is invertible inK.TauCeti.mu2EquivZMod2_apply_mu2NegOne,TauCeti.mu2EquivZMod2_eq_one_iff: the value dictionary on the nontrivial element ofμ₂.TauCeti.mu2_smul_eq_self: the Galois action onμ₂is trivial.TauCeti.kummerClass_oneandTauCeti.kummerClass_mul: the Kummer class of a unit is a homomorphism fromKˣintoH¹(G_K, 𝔽₂)written additively.TauCeti.mu2EquivZMod2_kummerCocycleandTauCeti.kummerCocycleModTwo_apply: the Kummer cocycle, read inZMod 2, is0when a Galois element fixes the chosen square root and1otherwise.TauCeti.kummerCocycleModTwoClass_eq_explicitCoeff1Equiv: the explicit mod-two cocycle class is the generic Kummer cocycle class read through the coefficient dictionaryμ₂ ≃ 𝔽₂.TauCeti.kummerClass_eq_kummerCocycleModTwoClass_of_sq_eq: that explicit class is the canonical Kummer class, under the degree-one comparison with continuous cohomology.TauCeti.kummerClass_eq_zero_iff_square: the Kummer class of a unit ofKˣvanishes exactly at the squares inKˣ.TauCeti.kummerSquareClassEquiv_squareClass: a square class is sent to the Kummer class of any of its representatives.
The elements of μ₂ #
The element of μ₂ represented by -1, that is -1 read as a 2nd root of unity in a
separable closure of the base field. It is the nontrivial element of μ₂ when 2 is invertible in
K (TauCeti.mu2NegOne_ne_zero); in characteristic two -1 = 1, and then it is the element 0
of μ₂.
Equations
Instances For
The underlying unit of TauCeti.mu2NegOne is -1, so mu2NegOne is exactly -1 read
as a 2nd root of unity in a separable closure of the base field.
The 2nd roots of unity of a separable closure are 1 and -1: ζ ^ 2 = 1 in a field
forces ζ = 1 or ζ = -1. No hypothesis on the characteristic is needed here: in characteristic
two the two values coincide (-1 = 1), which is why the two roots are shown to be distinct only
under [Invertible (2 : K)] (TauCeti.mu2NegOne_ne_zero).
An element of μ₂ is 0 or -1.
The two elements of μ₂ are distinct, because 2 is invertible in the base field.
The trivial Galois action #
The Galois action on μ₂ is trivial. Every 2nd root of unity in a separable closure is
±1 (TauCeti.toMul_eq_one_or_neg_one), hence lies in the base field and is fixed by G_K. This
is what makes the Kummer coefficients at n = 2 isomorphic to the trivial F₂ coefficient
object, whereas the action on μₙ for n > 2 is not trivial in general. It is a statement about
a field in any characteristic: the hypothesis [Invertible (2 : K)] is what tells the two roots
apart, not what triviality of the action needs.
The value dictionary #
The μ₂ coefficient module is ZMod 2, as an additive group: it is the specialization of
IsPrimitiveRoot.zmodEquivRootsOfUnity at the primitive root -1 (IsPrimitiveRoot.neg_one,
since the characteristic of Kˢ is not 2 when 2 is invertible in K), read backwards. The
generator is canonical: it is the nontrivial element -1 of μ₂, so the dictionary sends 0 to
0 and -1 to 1, and there is only one additive equivalence ZMod 2 ≃+ ZMod 2.
Equations
Instances For
The value dictionary sends the nontrivial element of μ₂ to 1, read at the exponent
1 from the inverse rule IsPrimitiveRoot.zmodEquivRootsOfUnity_symm_apply_pow.
The value dictionary sends an element of μ₂ to 1 exactly when it is the nontrivial
element: the dictionary is an equivalence, and it sends mu2NegOne to 1.
The coefficient object #
The coefficient carriers of μ₂ and of the trivial 𝔽₂ object are the same additive
group. This is TauCeti.mu2EquivZMod2 crossed with the universe lift of
TauCeti.trivialF2Equiv; it is the dictionary read on carriers, and
TauCeti.kummerCoeffIsoTrivialF2 is the same dictionary read in the category TopRep ℤ G_K.
Equations
Instances For
The dictionary is the value dictionary crossed with the universe lift.
The inverse dictionary reads a value through the universe lift.
The dictionary is G_K-equivariant, the two sides being the trivial action.
The Kummer coefficients at n = 2 and the trivial 𝔽₂ coefficient object are the same
coefficient object. The isomorphism is the value dictionary of TauCeti.mu2EquivZMod2, crossed
with the universe lift of TauCeti.trivialF2Equiv, and it is a morphism of coefficient objects
because the Galois action on μ₂ is trivial (TauCeti.mu2_smul_eq_self). The target is the
trivial 𝔽₂ object itself, TauCeti.kummerClass is that isomorphism read on degree-one continuous
cohomology, and its two application rules below are the value dictionary and its inverse.
Equations
Instances For
The isomorphism reads on carriers as the value dictionary.
The inverse isomorphism reads on carriers as the inverse value dictionary.
The Kummer class of a unit #
The degree-one map on continuous cohomology induced by the coefficient isomorphism
TauCeti.kummerCoeffIsoTrivialF2, read off the image isomorphism the continuous-cohomology functor
TauCeti.ContinuousCohomology.continuousCohomologyFunctor assigns to it.
Equations
Instances For
The Kummer class (a) ∈ H¹(G_K, 𝔽₂) of a unit a: the canonical Kummer map
TauCeti.kummerMapCanonical at n = 2, read through the coefficient-object isomorphism
TauCeti.kummerCoeffIsoTrivialF2.
Equations
- TauCeti.kummerClass a = (TopModuleCat.Hom.hom (TauCeti.kummerCohomMap K)) (Multiplicative.toAdd ((TauCeti.kummerMapCanonical K 2 ⋯) a))
Instances For
The Kummer class is the canonical Kummer map followed by the degree-one coefficient
map from roots of unity to trivial 𝔽₂ coefficients.
The Kummer class of 1 is the neutral element: TauCeti.kummerClass is a homomorphism
from Kˣ into H¹(G_K, 𝔽₂) written additively, paired with the multiplication law
TauCeti.kummerClass_mul.
The Kummer class of a product is the sum of the two Kummer classes: the
multiplicative-to-additive law of the Kummer class, its identity law being
TauCeti.kummerClass_one.
Equality of units of a separable closure is decidable, classically. This is what lets the
value formula TauCeti.kummerCocycleModTwo_apply be stated with an if; it carries no
mathematical content and is local to this file.
Instances For
The 𝔽₂-valued Kummer cocycle of a chosen square root. If α² = a, this is
the ratio cocycle g ↦ g • α / α, transported from μ₂ to the trivial 𝔽₂ coefficient
module. Its decoded values are computed by TauCeti.kummerCocycleModTwo_apply.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value of the Kummer cocycle in ZMod 2. The Kummer ratio g • α / α of a chosen
square root α is 0 when g fixes α and 1 when it exchanges the two square roots.
The square-root formula for the mod-two Kummer cocycle. Its value at g is 0 when
g fixes the chosen square root and 1 when it exchanges the two square roots.
The explicit cohomology class of the mod-two Kummer cocycle attached to a chosen square
root. It is independent of that choice because it is the coefficient transport of
TauCeti.kummerCocycleClass.
Equations
- TauCeti.kummerCocycleModTwoClass K hα = ↑(TauCeti.kummerCocycleModTwo K hα)
Instances For
The explicit mod-two Kummer class is the class of the explicit mod-two Kummer cocycle.
The explicit mod-two cocycle class is the generic Kummer cocycle class transported along
the coefficient equivalence μ₂ ≃ 𝔽₂.
The explicit mod-two Kummer cocycle class does not depend on the chosen square root.
The Kummer class of a unit vanishes exactly at the squares in Kˣ.
The degree-one comparison carries the coefficient dictionary to TauCeti.kummerCohomMap.
Reading the explicit coefficient equivalence μ₂ ≃ 𝔽₂ on explicit H¹ and then comparing with
canonical continuous cohomology is the same as comparing first and then applying the map that
TauCeti.kummerCoeffIsoTrivialF2 induces; the trailing transport is the one of
TauCeti.ofDiscreteModule_trivialF2, which kummerCoeffIsoTrivialF2 absorbs into its target.
The mod-two Kummer class is the explicit mod-two cocycle class of any square root.
If α² = a, the class TauCeti.kummerCocycleModTwoClass of the 𝔽₂-valued cocycle
g ↦ g • α / α becomes the Kummer class (a) under the degree-one comparison with canonical
continuous cohomology, followed by the transport of TauCeti.ofDiscreteModule_trivialF2 that
identifies the coefficient object of the comparison with TauCeti.trivialF2 itself.
The Kummer isomorphism on square classes #
The Kummer isomorphism on the square classes Kˣ ⧸ (Kˣ)² ≃+ H¹(G_K, 𝔽₂): the square class
of a unit a is sent to the Kummer class (a). The square-class side is the square-class group
Kˣ ⧸ (Kˣ)², that is TauCeti.SquareClassGroup K, in which the class of a is
TauCeti.squareClass a.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Kummer isomorphism on square classes sends the square class of a to the Kummer class
(a), which is the statement that identifies its two sides.