Unit-valued Galois cohomology of isomorphic fields

A field isomorphism transports the discrete unit modules of the chosen separable closures, continuous two-cocycles, and their explicit second cohomology groups. The group map is contravariant, and the coefficient map is covariant. Their compatibility follows from the conjugation equation for the chosen absolute-Galois-group equivalence. The same compatible pair also identifies Mathlib's canonical continuousCohomology 2 groups, by TauCeti.ContCohomology.continuousCohomologyMap2Equiv, and the comparison with the explicit model carries one identification to the other (RingEquiv.explicitH2AddEquivContinuousCohomology_unitsH2Congr).

The compatible-pair construction is extracted from TauCeti.ClassFieldTheory.brCongr and specializes continuous cohomology's cocyclesMap2 and explicitMap2Equiv. Both field universes remain independent. The lift to separable closures is chosen: the inverse below is the inverse of this supplied identification, rather than a separately chosen lift of the inverse field isomorphism.

noncomputable def RingEquiv.unitsCoeffCongr {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) : TauCeti.UnitsCoeff K ≃+ TauCeti.UnitsCoeff L

The covariant identification of discrete unit coefficients induced by a field isomorphism, using the inverse of its chosen separable-closure identification.

@[simp]

theorem RingEquiv.unitsCoeffCongr_apply {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) (x : TauCeti.UnitsCoeff K) : ↑(Additive.toMul (e.unitsCoeffCongr x)) = e.separableClosureCongr.symm ↑(Additive.toMul x)

On underlying field elements, coefficient transport is the chosen separable-closure map.

@[simp]

theorem RingEquiv.unitsCoeffCongr_symm_apply {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) (x : TauCeti.UnitsCoeff L) : ↑(Additive.toMul (e.unitsCoeffCongr.symm x)) = e.separableClosureCongr ↑(Additive.toMul x)

The inverse coefficient transport is the chosen map from the target separable closure.

@[simp]

theorem RingEquiv.unitsCoeffCongr_smul {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) (g : TauCeti.AbsoluteGaloisGroup L) (x : TauCeti.UnitsCoeff K) : e.unitsCoeffCongr (e.absoluteGaloisGroupCongr g • x) = g • e.unitsCoeffCongr x

Coefficient transport intertwines the absolute Galois actions.

noncomputable def RingEquiv.unitsCocyclesCongr {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) : ↥(TauCeti.ContCohomology.Z2 (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K)) →+ ↥(TauCeti.ContCohomology.Z2 (TauCeti.AbsoluteGaloisGroup L) (TauCeti.UnitsCoeff L))

Transport of continuous unit-valued two-cocycles along a field isomorphism.

@[simp]

theorem RingEquiv.unitsCocyclesCongr_apply {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) (c : ↥(TauCeti.ContCohomology.Z2 (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K))) (g h : TauCeti.AbsoluteGaloisGroup L) : ↑(e.unitsCocyclesCongr c) (g, h) = e.unitsCoeffCongr (↑c (e.absoluteGaloisGroupCongr g, e.absoluteGaloisGroupCongr h))

The transported cocycle is evaluated at the transported automorphisms, then its value is transported between the separable closures.

noncomputable def RingEquiv.unitsH2Congr {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) : TauCeti.ContCohomology.H2 (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K) ≃+ TauCeti.ContCohomology.H2 (TauCeti.AbsoluteGaloisGroup L) (TauCeti.UnitsCoeff L)

A field isomorphism identifies the explicit second Galois cohomology groups with unit coefficients. This preserves the actual field, absolute Galois group and coefficient universes.

@[simp]

theorem RingEquiv.unitsH2Congr_mk {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) (c : ↥(TauCeti.ContCohomology.Z2 (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K))) : e.unitsH2Congr ↑c = ↑(e.unitsCocyclesCongr c)

On a cocycle class, field transport is given by the transported continuous cocycle.

@[simp]

theorem RingEquiv.unitsH2Congr_symm_unitsCocyclesCongr {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) (c : ↥(TauCeti.ContCohomology.Z2 (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K))) : e.unitsH2Congr.symm ↑(e.unitsCocyclesCongr c) = ↑c

Inverse transport recovers the class of a cocycle from its transported representative.

theorem RingEquiv.unitsH2Congr_symm_mk {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) (c : ↥(TauCeti.ContCohomology.Z2 (TauCeti.AbsoluteGaloisGroup L) (TauCeti.UnitsCoeff L))) : e.unitsH2Congr.symm ↑c = ↑((TauCeti.ContCohomology.cocyclesMap2 (TauCeti.AbsoluteGaloisGroup L) (TauCeti.UnitsCoeff L) (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K) (↑e.absoluteGaloisGroupCongr.symm) e.unitsCoeffCongr.symm.toAddMonoidHom ⋯ ⋯) c)

The inverse identification is induced by the inverse compatible group and coefficient maps of the chosen lift.

theorem RingEquiv.locallyCompactSpace_absoluteGaloisGroup {F : Type u_1} [Field F] : LocallyCompactSpace (TauCeti.AbsoluteGaloisGroup F)

The absolute Galois group is locally compact, being compact and Hausdorff. Instance search does not find this within its default budget, so it is assembled here from the Krull topology being Hausdorff, as in TauCeti.Algebra.CrossedProduct.Comparison.

noncomputable def RingEquiv.unitsContinuousH2Congr {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) : ↑(continuousCohomology 2 (TauCeti.ofDiscreteModule ℤ (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K))).toModuleCat ≃+ ↑(continuousCohomology 2 (TauCeti.ofDiscreteModule ℤ (TauCeti.AbsoluteGaloisGroup L) (TauCeti.UnitsCoeff L))).toModuleCat

A field isomorphism identifies Mathlib's canonical second continuous Galois cohomology groups with unit coefficients, along the same group and coefficient maps as RingEquiv.unitsH2Congr. The field universes remain independent.

theorem RingEquiv.unitsContinuousH2Congr_apply {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) (x : ↑(continuousCohomology 2 (TauCeti.ofDiscreteModule ℤ (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K))).toModuleCat) : e.unitsContinuousH2Congr x = (TauCeti.ContCohomology.continuousCohomologyMap2 (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K) (TauCeti.AbsoluteGaloisGroup L) (TauCeti.UnitsCoeff L) (↑e.absoluteGaloisGroupCongr) e.unitsCoeffCongr.toAddMonoidHom ⋯) x

Canonical field transport is the pullback along the transported automorphisms and the coefficient transport.

@[simp]

theorem RingEquiv.explicitH2AddEquivContinuousCohomology_unitsH2Congr {K : Type u} {L : Type v} [Field K] [Field L] (e : K ≃+* L) (x : TauCeti.ContCohomology.H2 (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K)) : e.unitsContinuousH2Congr ((TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K)) x) = (TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology (TauCeti.AbsoluteGaloisGroup L) (TauCeti.UnitsCoeff L)) (e.unitsH2Congr x)

The comparison of the explicit H² with Mathlib's continuous cohomology carries explicit field transport RingEquiv.unitsH2Congr to canonical field transport.