The Krull bridge: open index-2 subgroup ⇒ quadratic subextension

As part of the proof of kummerClassK_surjective, this file shows that an open subgroup of index 2 H ≤ G_k := ↥(k.fixingSubgroup) determines a quadratic subextension k ≤ L whose fixing group cuts out exactly H, with [L : k] = 2 (exists_quadratic_of_open_index_two).

Route (all joints pinned in B12-0.3): H' := H.map k.fixingSubgroup.subtype is open in the ambient Gal(ℚ̄₂/ℚ₂) (k finite ⇒ k.fixingSubgroup open; push the image forward by IsOpen.isOpenMap_subtype_val), hence closed; L := fixedField H' (staying in the ambient group — never transporting to Gal(ℚ̄₂/↥k)); Krull's InfiniteGalois.fixingSubgroup_fixedField gives L.fixingSubgroup = H', through which H'-openness feeds InfiniteGalois.isOpen_iff_finite to yield FiniteDimensional ℚ_[2] L; the subgroupOf-form descends by comap_map_eq_self_of_injective; and the degree is the ported finrank_extendScalars_eq_two.

Placement. It imports only GQ2.EvensKahn (+ Mathlib), so it stays strictly upstream of Foundations/Axioms.lean. The three extendScalars degree lemmas it needs (finiteDimensional_extendScalars, index_extendScalars_fixingSubgroup, finrank_extendScalars_eq_two) live downstream in GQ2.ShapiroDeepness (InvolutionVanish.lean), so they are re-proved here as private copies, verbatim-modulo-namespace (pure Mathlib field theory; the private marker guarantees no clash with any parallel port).

The public theorem lives in namespace GQ2.KummerSurjectivity so the final surjectivity assembly can import this field-theoretic layer without introducing a cycle.

Ported extendScalars degree lemmas

Private, verbatim-modulo-namespace copies of GQ2.ShapiroDeepness.{finiteDimensional_extendScalars, index_extendScalars_fixingSubgroup, finrank_extendScalars_eq_two} (InvolutionVanish.lean), which sit downstream of Foundations/Axioms.lean. Their proofs are pure Mathlib field theory.

The Krull bridge

theorem GQ2.KummerSurjectivity.exists_quadratic_of_open_index_two (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥k] (H : Subgroup ↥k.fixingSubgroup) (hHopen : IsOpen ↑H) (hHindex : H.index = 2) : ∃ (L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hkL : k ≤ L), FiniteDimensional ℚ_[2] ↥L ∧ L.fixingSubgroup.subgroupOf k.fixingSubgroup = H ∧ Module.finrank ↥k ↥(IntermediateField.extendScalars hkL) = 2

B12-2 (§4-I2): an open subgroup of index 2 in G_k cuts out a quadratic subextension.

Given k finite over ℚ₂ and an open subgroup H ≤ G_k = ↥(k.fixingSubgroup) of index 2, there is an intermediate field k ≤ L, finite over ℚ₂, with L.fixingSubgroup.subgroupOf k.fixingSubgroup = H and [L : k] = 2. This is the Krull–Galois half of the kummerClassK_surjective discharge: it turns the kernel of a nonzero H¹(G_k, 𝔽₂)-cocycle into the quadratic extension whose Kummer class realises that cocycle.