Independence of embeddings in first Galois cohomology

For a field extension L/K, compatible coefficient maps along embeddings Kˢ → Lˢ induce the same map on explicit H¹ if precomposing an embedding by an automorphism of Kˢ precomposes its coefficient map by the action of that automorphism. Two embeddings differ by such an automorphism, and conjugation of compatible pairs acts trivially on H¹.

This is the embedding-independence consequence of the conjugation formalism in Neukirch, Schmidt and Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §5.

theorem TauCeti.ContCohomology.explicitMap1_absoluteGaloisGroupMap_eq {K : Type uK} [Field K] {L : Type uL} [Field L] [Algebra K L] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction (AbsoluteGaloisGroup K) M] [ContinuousSMul (AbsoluteGaloisGroup K) M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction (AbsoluteGaloisGroup L) N] [ContinuousSMul (AbsoluteGaloisGroup L) N] (F : (SeparableClosure K →ₐ[K] SeparableClosure L) → M →+ N) (hF : ∀ (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (g : AbsoluteGaloisGroup L) (m : M), (F τ) ((absoluteGaloisGroupMap τ) g • m) = g • (F τ) m) (hFcomp : ∀ (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (h : AbsoluteGaloisGroup K) (m : M), (F (τ.comp ↑h)) m = (F τ) (h • m)) (τ τ' : SeparableClosure K →ₐ[K] SeparableClosure L) : explicitMap1 (AbsoluteGaloisGroup K) M (AbsoluteGaloisGroup L) N (absoluteGaloisGroupMap τ) (F τ) ⋯ ⋯ = explicitMap1 (AbsoluteGaloisGroup K) M (AbsoluteGaloisGroup L) N (absoluteGaloisGroupMap τ') (F τ') ⋯ ⋯

Pullbacks on explicit H¹ along embeddings of separable closures are independent of the embedding when the coefficient maps are equivariant and precomposition by an automorphism agrees with its action on coefficients. This follows from conjugation invariance in Neukirch, Schmidt and Wingberg, Cohomology of Number Fields, Chapter I, §5.