Inflation of compatible cocycles and field-extension restriction

Let L/K be a field extension, and identify its separable closure with that of K using an embedding σ : L → Kˢ. Suppose that finite normal subextensions E ⊆ Kˢ and F ⊆ Lˢ are related by a ring embedding compatible with that identification, and that their automorphisms intertwine through a homomorphism π : Aut_L(F) → Aut_K(E). If two finite cocycles agree under this compatible pair, inflation of the cocycle over F is restriction of the inflated class over E.

The comparison uses the existing TwoCocycle.inflateClass and galoisResUnits, including the coefficient identification between the units of the two separable closures. It applies to the restricted cocycle of an intermediate field, without requiring that intermediate field to be normal over K.

References

• J.-P. Serre, Local Fields, GTM 67 (1979), Chapter X, §5.
• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, §4.4.

theorem TauCeti.TwoCocycle.inflateZ2_restriction_apply {K L : Type u} [Field K] [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [Normal K ↥E] (F : IntermediateField L (SeparableClosure L)) [FiniteDimensional L ↥F] [Normal L ↥F] (ι : ↥E →+* ↥F) (π : Gal(↥F/L) →* Gal(↥E/K)) (hι : ∀ (x : ↥E), (separableClosureRingEquiv K L σ).symm (E.val x) = F.val (ι x)) (hπ : ∀ (g : Gal(↥F/L)) (x : ↥E), ι ((π g) x) = g (ι x)) (c : TwoCocycle K ↥E) (d : TwoCocycle L ↥F) (hd : ∀ (g h : Gal(↥F/L)), d.toFun g h = (Units.map ↑ι) (c.toFun (π g) (π h))) (g h : AbsoluteGaloisGroup L) : (unitsCoeffMap K L σ) (↑(inflateZ2 E c) (↑((absoluteGaloisGroupEquivFixingSubgroup K L σ) g), ↑((absoluteGaloisGroupEquivFixingSubgroup K L σ) h))) = ↑(inflateZ2 F d) (g, h)

The inflated cocycles agree pointwise after restricting the group and identifying the coefficient modules of the two separable closures.

theorem TauCeti.TwoCocycle.inflateClass_galoisResUnits {K L : Type u} [Field K] [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [Normal K ↥E] (F : IntermediateField L (SeparableClosure L)) [FiniteDimensional L ↥F] [Normal L ↥F] (ι : ↥E →+* ↥F) (π : Gal(↥F/L) →* Gal(↥E/K)) (hι : ∀ (x : ↥E), (separableClosureRingEquiv K L σ).symm (E.val x) = F.val (ι x)) (hπ : ∀ (g : Gal(↥F/L)) (x : ↥E), ι ((π g) x) = g (ι x)) (c : TwoCocycle K ↥E) (d : TwoCocycle L ↥F) (hd : ∀ (g h : Gal(↥F/L)), d.toFun g h = (Units.map ↑ι) (c.toFun (π g) (π h))) : (CategoryTheory.ConcreteCategory.hom (galoisResUnits K L σ 2)) (inflateClass E c) = inflateClass F d

Inflation of a finite cocycle compatible with a field extension is the restriction of the original inflated cohomology class, with the canonical units-coefficient transport.