Inflation of crossed-product cocycles

A TwoCocycle K L for a finite Galois subextension L of the separable closure of K inflates along restriction G_K → Gal(L/K) to a continuous cocycle of the absolute Galois group with values in Additive (Kˢ)ˣ. This file constructs its class in continuous H² and identifies it with the corresponding leg of the finite-quotient description of continuous cohomology.

The multiplicative-to-additive conversion is TwoCocycle.toCocycles₂. Continuity follows because restriction has finite discrete target. Inflation turns products of cocycles into sums of classes, cohomologous finite cocycles determine the same continuous class, and passing to a larger finite Galois subextension, along any compatible pair agreeing with the inclusions into Kˢ, does not change the class.

Conversely, strict finite-quotient descent of continuous 2-cocycles, followed by the infinite Galois correspondence, realizes every continuous cocycle as the inflation of a cocycle on a finite Galois subextension. Consequently every continuous cohomology class is the inflated class of a bundled GaloisCocycle.

The conventions follow Gille--Szamuely, Central Simple Algebras and Galois Cohomology, §4.4, and Serre, Local Fields, Chapter X.

noncomputable def TauCeti.TwoCocycle.inflate {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [Normal K ↥L] (c : TwoCocycle K ↥L) : TwoCocycle K (SeparableClosure K)

Inflation of a cocycle on Gal(L/K) to the absolute Galois group, along restriction and the inclusion L ⊆ Kˢ.

Equations

• TauCeti.TwoCocycle.inflate L c = TauCeti.TwoCocycle.comap (AlgEquiv.restrictNormalHom ↥L) L.val ⋯ c

@[simp]

theorem TauCeti.TwoCocycle.inflate_toFun {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [Normal K ↥L] (c : TwoCocycle K ↥L) (g h : AbsoluteGaloisGroup K) : (inflate L c).toFun g h = (Units.map ↑L.val.toRingHom) (c.toFun ((AlgEquiv.restrictNormalHom ↥L) g) ((AlgEquiv.restrictNormalHom ↥L) h))

Inflating a cocycle and evaluating it amounts to restricting both automorphisms and including its value in the separable closure.

theorem TauCeti.TwoCocycle.continuous_toCocycles₂_inflate {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) : Continuous ⇑(inflate L c).toCocycles₂

The cochain obtained by inflating from a finite normal subextension is continuous.

noncomputable def TauCeti.TwoCocycle.inflateZ2 {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) : ↥(ContCohomology.Z2 (AbsoluteGaloisGroup K) (UnitsCoeff K))

The inflated cocycle as an element of the explicit continuous cocycle group Z².

Equations

• TauCeti.TwoCocycle.inflateZ2 L c = ⟨⇑(TauCeti.TwoCocycle.inflate L c).toCocycles₂, ⋯⟩

@[simp]

theorem TauCeti.TwoCocycle.coe_inflateZ2 {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) : ↑(inflateZ2 L c) = ⇑(inflate L c).toCocycles₂

The cocycle underlying inflateZ2 is the additive cocycle of the inflated cocycle.

noncomputable def TauCeti.TwoCocycle.inflateClass {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) : ↑(continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K))).toModuleCat

The continuous cohomology class represented by the inflation of c.

Equations

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

theorem TauCeti.TwoCocycle.inflateClass_def {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) : inflateClass L c = (ContCohomology.explicitH2AddEquivContinuousCohomology (AbsoluteGaloisGroup K) (UnitsCoeff K)) ((ContCohomology.H2pi (AbsoluteGaloisGroup K) (UnitsCoeff K)) (inflateZ2 L c))

The representative of the continuous cohomology class inflateClass.

@[simp]

theorem TauCeti.TwoCocycle.inflateZ2_mul {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (z w : TwoCocycle K ↥L) : inflateZ2 L (z * w) = inflateZ2 L z + inflateZ2 L w

Inflation turns the pointwise product of cocycles into the sum of continuous cocycles.

@[simp]

theorem TauCeti.TwoCocycle.inflateClass_mul {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (z w : TwoCocycle K ↥L) : inflateClass L (z * w) = inflateClass L z + inflateClass L w

Inflation is additive: the pointwise product of cocycles inflates to the sum of their continuous classes.

@[simp]

theorem TauCeti.TwoCocycle.inflateClass_one {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] : inflateClass L 1 = 0

The trivial cocycle inflates to the zero class.

@[simp]

theorem TauCeti.TwoCocycle.inflateClass_div {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (z w : TwoCocycle K ↥L) : inflateClass L (z / w) = inflateClass L z - inflateClass L w

Inflation turns the pointwise quotient of cocycles into the difference of their classes.

theorem TauCeti.TwoCocycle.inflateClass_eq_of_cohomologous {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] {z w : TwoCocycle K ↥L} (h : z.Cohomologous w) : inflateClass L z = inflateClass L w

Cohomologous crossed-product cocycles have the same class after inflation to continuous cohomology.

theorem TauCeti.TwoCocycle.inflate_comap {K : Type} [Field K] {L M : IntermediateField K (SeparableClosure K)} [Normal K ↥L] [Normal K ↥M] (π : Gal(↥M/K) →* Gal(↥L/K)) (ι : ↥L →ₐ[K] ↥M) (hπι : ∀ (g : Gal(↥M/K)) (x : ↥L), ι ((π g) x) = g (ι x)) (hι : ∀ (x : ↥L), M.val (ι x) = L.val x) (c : TwoCocycle K ↥L) : inflate M (comap π ι hπι c) = inflate L c

Refining a normal subextension along a compatible pair (π, ι), with ι compatible with the inclusions into Kˢ, before inflation does not change the cocycle on the absolute Galois group.

theorem TauCeti.TwoCocycle.inflateZ2_comap {K : Type} [Field K] {L M : IntermediateField K (SeparableClosure K)} [Normal K ↥L] [Normal K ↥M] (π : Gal(↥M/K) →* Gal(↥L/K)) (ι : ↥L →ₐ[K] ↥M) (hπι : ∀ (g : Gal(↥M/K)) (x : ↥L), ι ((π g) x) = g (ι x)) (hι : ∀ (x : ↥L), M.val (ι x) = L.val x) [FiniteDimensional K ↥L] [FiniteDimensional K ↥M] (c : TwoCocycle K ↥L) : inflateZ2 M (comap π ι hπι c) = inflateZ2 L c

Refining the finite normal subextension along a compatible pair does not change the inflated continuous cocycle.

theorem TauCeti.TwoCocycle.inflateClass_comap {K : Type} [Field K] {L M : IntermediateField K (SeparableClosure K)} [Normal K ↥L] [Normal K ↥M] (π : Gal(↥M/K) →* Gal(↥L/K)) (ι : ↥L →ₐ[K] ↥M) (hπι : ∀ (g : Gal(↥M/K)) (x : ↥L), ι ((π g) x) = g (ι x)) (hι : ∀ (x : ↥L), M.val (ι x) = L.val x) [FiniteDimensional K ↥L] [FiniteDimensional K ↥M] (c : TwoCocycle K ↥L) : inflateClass M (comap π ι hπι c) = inflateClass L c

Refining the finite normal subextension on which a cocycle is defined, along a compatible pair (π, ι) with ι compatible with the inclusions into Kˢ, does not change its inflated continuous cohomology class.

noncomputable def TauCeti.TwoCocycle.finiteLevelZ2 {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) : ↥(ContCohomology.Z2 (AbsoluteGaloisGroup K ⧸ ↑(galoisOpenNormalSubgroup K (↥L) L.val).toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑(galoisOpenNormalSubgroup K (↥L) L.val).toOpenSubgroup) (UnitsCoeff K)))

The cocycle at the finite quotient G_K/G_L, with values in the units fixed by G_L: the pullback, along the compatible pair given by the quotient identification G_K/G_L ≃ Gal(L/K) and the inclusion of Lˣ as the invariants, of c viewed as a cocycle of the discrete group Gal(L/K) with discrete coefficients.

Equations

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

@[simp]

theorem TauCeti.TwoCocycle.finiteLevelZ2_apply {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) (q r : AbsoluteGaloisGroup K ⧸ ↑(galoisOpenNormalSubgroup K (↥L) L.val).toOpenSubgroup) : ↑(↑(finiteLevelZ2 L c) (q, r)) = Additive.ofMul ((Units.map ↑L.val.toRingHom) (c.toFun ((quotientFixingSubgroupFieldRangeEquiv K (↥L) L.val) q) ((quotientFixingSubgroupFieldRangeEquiv K (↥L) L.val) r)))

The finite-level cocycle evaluates by restricting the two quotient classes and embedding the value of the original cocycle into the separable closure.

noncomputable def TauCeti.TwoCocycle.finiteLevelClass {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) : ContCohomology.H2 (AbsoluteGaloisGroup K ⧸ ↑(galoisOpenNormalSubgroup K (↥L) L.val).toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑(galoisOpenNormalSubgroup K (↥L) L.val).toOpenSubgroup) (UnitsCoeff K))

The class of a crossed-product cocycle at the finite quotient G_K/G_L.

Equations

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

theorem TauCeti.TwoCocycle.finiteLevelClass_def {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) : finiteLevelClass L c = (ContCohomology.H2pi (AbsoluteGaloisGroup K ⧸ ↑(galoisOpenNormalSubgroup K (↥L) L.val).toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑(galoisOpenNormalSubgroup K (↥L) L.val).toOpenSubgroup) (UnitsCoeff K))) (finiteLevelZ2 L c)

The representative of the finite-level cohomology class finiteLevelClass.

theorem TauCeti.TwoCocycle.inflateClass_eq_finiteQuotientComparison {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [Normal K ↥L] (c : TwoCocycle K ↥L) : inflateClass L c = (ContCohomology.explicitH2AddEquivContinuousCohomology (AbsoluteGaloisGroup K) (UnitsCoeff K)) ((CategoryTheory.ConcreteCategory.hom ((ContCohomology.explicitFiniteQuotientComparison2 (AbsoluteGaloisGroup K) (UnitsCoeff K)).app (Opposite.op (galoisOpenNormalSubgroup K (↥L) L.val)))) (finiteLevelClass L c))

The inflated crossed-product class is the finite-quotient comparison class. More precisely, its explicit H² representative is the image of the class at the quotient G_K/G_L under the L-leg of explicitFiniteQuotientComparison2.

noncomputable def TauCeti.GaloisCocycle.inflateClass {K : Type} [Field K] (c : GaloisCocycle K) : ↑(continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K))).toModuleCat

The continuous cohomology class obtained by inflating a bundled finite Galois cocycle.

Equations

• c.inflateClass = TauCeti.TwoCocycle.inflateClass c.extension c.cocycle

@[simp]

theorem TauCeti.GaloisCocycle.inflateClass_def {K : Type} [Field K] (c : GaloisCocycle K) : c.inflateClass = TwoCocycle.inflateClass c.extension c.cocycle

The class of a bundled finite Galois cocycle is the inflated class of its cocycle.

Exhaustion by finite Galois cocycles

theorem TauCeti.exists_galoisCocycle_inflateZ2 {K : Type} [Field K] (z : ↥(ContCohomology.Z2 (AbsoluteGaloisGroup K) (UnitsCoeff K))) : ∃ (c : GaloisCocycle K), TwoCocycle.inflateZ2 c.extension c.cocycle = z

Every continuous 2-cocycle of the absolute Galois group is inflated from a finite Galois subextension. The equality is on cocycle representatives: no coboundary is subtracted.

The finite subextension is the fixed field of the open normal subgroup supplied by strict finite-quotient descent.

theorem TauCeti.exists_galoisCocycle_inflateClass {K : Type} [Field K] (x : ↑(continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K))).toModuleCat) : ∃ (c : GaloisCocycle K), c.inflateClass = x

Every continuous degree-two class of the absolute Galois group is inflated from a finite Galois cocycle.