Transport of first cohomology to the kernel field

The comparison between cohomology on ker ρ and the corresponding local Galois group.

See GQ2.DeepCount for the paper-facing overview, source citations, and deviations.

The ker ρ ↔ G_k transport of H¹

hker is a POINTWISE identification, so the types H1 ↥(ker ρ) and H1 k.fixingSubgroup differ as terms and an Eq-rewrite dies on dependent motives. Instead: with trivial coefficients the transport is plain COCYCLE PRECOMPOSITION along the identity inclusions kerToFixing/fixingToKer (the conjAct-machinery pattern: Quotient.out-based maps with H1ofFun-computation rules — the B¹ = 0 argument makes the representative exact).

def GQ2.fixingToKer {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (n : ↥k.fixingSubgroup) : ↥ρ.ker

The identity inclusion ↥k.fixingSubgroup → ↥(ker ρ) (inverse of kerToFixing).

Equations

• GQ2.fixingToKer ρ k hker n = ⟨↑n, ⋯⟩

theorem GQ2.comp_fixingToKer_mem_Z1 {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) {f : ↥ρ.ker → ZMod 2} (hf : f ∈ ContCoh.Z1 (↥ρ.ker) (ZMod 2)) : (fun (n : ↥k.fixingSubgroup) => f (fixingToKer ρ k hker n)) ∈ ContCoh.Z1 (↥k.fixingSubgroup) (ZMod 2)

Precomposition with fixingToKer carries Z¹(ker ρ) to Z¹(G_k).

theorem GQ2.comp_kerToFixing_mem_Z1 {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) {f : ↥k.fixingSubgroup → ZMod 2} (hf : f ∈ ContCoh.Z1 (↥k.fixingSubgroup) (ZMod 2)) : (fun (n : ↥ρ.ker) => f (kerToFixing ρ k hker n)) ∈ ContCoh.Z1 (↥ρ.ker) (ZMod 2)

Precomposition with kerToFixing carries Z¹(G_k) to Z¹(ker ρ).

noncomputable def GQ2.h1KerToFix {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (ξ : ContCoh.H1 (↥ρ.ker) (ZMod 2)) : ContCoh.H1 (↥k.fixingSubgroup) (ZMod 2)

Transport H¹(ker ρ) → H¹(G_k) (cocycle precomposition with fixingToKer).

Equations

• GQ2.h1KerToFix ρ k hker ξ = GQ2.H1ofFun ↥k.fixingSubgroup fun (n : ↥k.fixingSubgroup) => ↑(Quotient.out ξ) (GQ2.fixingToKer ρ k hker n)

noncomputable def GQ2.h1FixToKer {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (η : ContCoh.H1 (↥k.fixingSubgroup) (ZMod 2)) : ContCoh.H1 (↥ρ.ker) (ZMod 2)

Transport H¹(G_k) → H¹(ker ρ) (cocycle precomposition with kerToFixing).

Equations

• GQ2.h1FixToKer ρ k hker η = GQ2.H1ofFun ↥ρ.ker fun (n : ↥ρ.ker) => ↑(Quotient.out η) (GQ2.kerToFixing ρ k hker n)

theorem GQ2.h1KerToFix_h1ofFun {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) {f : ↥ρ.ker → ZMod 2} (hf : f ∈ ContCoh.Z1 (↥ρ.ker) (ZMod 2)) : h1KerToFix ρ k hker (H1ofFun (↥ρ.ker) f) = H1ofFun ↥k.fixingSubgroup fun (n : ↥k.fixingSubgroup) => f (fixingToKer ρ k hker n)

Computation rule for h1KerToFix (the B¹ = 0 argument: the canonical representative of an H1ofFun-class is the function itself).

theorem GQ2.h1FixToKer_h1ofFun {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) {f : ↥k.fixingSubgroup → ZMod 2} (hf : f ∈ ContCoh.Z1 (↥k.fixingSubgroup) (ZMod 2)) : h1FixToKer ρ k hker (H1ofFun (↥k.fixingSubgroup) f) = H1ofFun ↥ρ.ker fun (n : ↥ρ.ker) => f (kerToFixing ρ k hker n)

Computation rule for h1FixToKer.

theorem GQ2.h1FixToKer_h1KerToFix {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (ξ : ContCoh.H1 (↥ρ.ker) (ZMod 2)) : h1FixToKer ρ k hker (h1KerToFix ρ k hker ξ) = ξ

The round trip ker → fix → ker is the identity.

theorem GQ2.h1KerToFix_h1FixToKer {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (η : ContCoh.H1 (↥k.fixingSubgroup) (ZMod 2)) : h1KerToFix ρ k hker (h1FixToKer ρ k hker η) = η

The round trip fix → ker → fix is the identity.

theorem GQ2.h1KerToFix_add {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (ξ η : ContCoh.H1 (↥ρ.ker) (ZMod 2)) : h1KerToFix ρ k hker (ξ + η) = h1KerToFix ρ k hker ξ + h1KerToFix ρ k hker η

h1KerToFix is additive.

noncomputable def GQ2.h1KerFixEquiv {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) : ContCoh.H1 (↥ρ.ker) (ZMod 2) ≃+ ContCoh.H1 (↥k.fixingSubgroup) (ZMod 2)

The transport equivalence H¹(ker ρ) ≃+ H¹(G_k).

Equations

• GQ2.h1KerFixEquiv ρ k hker = { toFun := GQ2.h1KerToFix ρ k hker, invFun := GQ2.h1FixToKer ρ k hker, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

theorem GQ2.h1KerToFix_mem_deep_iff {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (ξ : ContCoh.H1 (↥ρ.ker) (ZMod 2)) : h1KerToFix ρ k hker ξ ∈ LocalKummer.deepClasses k.fixingSubgroup ↔ ξ ∈ deepClassesSubgroup ρ.ker

h1KerToFix carries deep classes to deep classes, and conversely (the (A, β)-data transports verbatim; memberships move along hker).

theorem GQ2.h1KerToFix_mem_mid_iff {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (ξ : ContCoh.H1 (↥ρ.ker) (ZMod 2)) : h1KerToFix ρ k hker ξ ∈ midClassesSubgroup k.fixingSubgroup ↔ ξ ∈ midClassesSubgroup ρ.ker

The mid-classes version of the transport.

theorem GQ2.card_quot_deep_le_card_mid_ker {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥k] [Finite (ContCoh.H1 (↥ρ.ker) (ZMod 2))] (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (π : AlgebraicClosure ℚ_[2]) (hπk : π ∈ k) (hπ0 : π ≠ 0) (hπ1 : ‖π‖ < 1) (hπmax : ∀ x ∈ k, ‖x‖ < 1 → ‖x‖ ≤ ‖π‖) {e : ℕ} (he : ‖2‖ = ‖π‖ ^ e) (he_pos : 1 ≤ e) {f : ℕ} (hf_pos : 1 ≤ f) (hcard_zero : Nat.card (↥(normUnits k) ⧸ (depthUnits k π 1).subgroupOf (normUnits k)) = 2 ^ f - 1) (hcard_gr : ∀ (i : ℕ), 1 ≤ i → Nat.card (↥(depthUnits k π i) ⧸ (depthUnits k π (i + 1)).subgroupOf (depthUnits k π i)) = 2 ^ f) : Nat.card (ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ deepClassesSubgroup ρ.ker) ≤ Nat.card ↥(midClassesSubgroup ρ.ker)

The transported structural count, in ker ρ-vocabulary: #(H¹(ker ρ) ⧸ Deep) ≤ #E.