Documentation

GQ2.DeepDualityK

The K-level Tate pairing #

The first consumer of the base-generalized B6 (GQ2.tateDualityAt): the 𝔽₂-valued Tate pairing on M = HΒΉ(G_K, 𝔽₂) for K the splitting field (G_K = ker ρ), supplying the pairing hypotheses of the abstract hduality (GQ2.card_equivHoms_deep_eq_quot, GQ2/DeepDuality.lean Β§F):

Everything is ρ.ker-vocabulary (no IntermediateField enters); the isotropy (H3) discharge (cup_deepClasses lives over k.fixingSubgroup) is the f8 splice's k-plumbing.

Design details are recorded in docs/orchestration/p15f-handoff.md Β§8 and docs/orchestration/p15f7-axiom-proposal.md.

source
theorem GQ2.ker_isLocalDualizingGroup {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] :
IsLocalDualizingGroup (β†₯ρ.ker) 2

G_K = ker ρ is a local dualizing group: the subtype topological embedding into G_β„šβ‚‚ has finite index (the quotient injects into the finite C) and acts on ΞΌβ‚‚ by restriction (definitionally).

source
noncomputable def GQ2.tateDualityK {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] :
TateDualityG (β†₯ρ.ker) 2

The Tate-duality bundle at G_K β€” the first consumer of the base-generalized B6.

Equations
Instances For
    source
    theorem GQ2.smul_muN_two_trivial_ker {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (g : β†₯ρ.ker) (x : MuN 2) :
    g β€’ x = x

    The kernel acts trivially on ΞΌβ‚‚ (restriction of the trivial G_β„šβ‚‚-action).

    source
    noncomputable def GQ2.zmodMuDualEquiv :
    ZMod 2 ≃+ MuDual 2 (ZMod 2)

    The coefficient bridge 𝔽₂ ≃+ Hom(𝔽₂, ΞΌβ‚‚): a ↦ (m ↦ ΞΌβ‚‚-lift of aΒ·m). Feeds H1congr to move HΒΉ(G_K, 𝔽₂)-classes into the duality bundle's MuDual-slot.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem GQ2.zmodMuDualEquiv_equivariant {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (g : β†₯ρ.ker) (a : ZMod 2) :
      zmodMuDualEquiv (g β€’ a) = g β€’ zmodMuDualEquiv a

      Equivariance of the coefficient bridge (both sides carry trivial β†₯(ker ρ)-actions: 𝔽₂ definitionally, the ΞΌβ‚‚-dual by smul_muN_two_trivial_ker).

      source
      noncomputable def GQ2.pairingK {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] :
      ContCoh.H1 (β†₯ρ.ker) (ZMod 2) β†’+ ContCoh.H1 (β†₯ρ.ker) (ZMod 2) β†’+ ZMod 2

      The K-level Tate pairing on M = HΒΉ(G_K, 𝔽₂): transport the left argument through the coefficient bridge, cup with the evaluation pairing, and read off through the invariant map of tateDualityK β€” B(x, y) := inv_K (xβ€² βˆͺ y).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem GQ2.pairingK_nondeg {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] (x : ContCoh.H1 (β†₯ρ.ker) (ZMod 2)) (hx : βˆ€ (y : ContCoh.H1 (β†₯ρ.ker) (ZMod 2)), ((pairingK ρ) x) y = 0) :
        x = 0

        (H2) Nondegeneracy of the K-level pairing β€” the (1,1)-perfectness clause of the base-generalized B6 at G_K: a class pairing trivially with everything is zero.

        source
        theorem GQ2.conjMap_mul_apply {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (g : AbsGalQ2) (n m : β†₯ρ.ker) :
        LocalKummer.conjMap ρ g (n * m) = LocalKummer.conjMap ρ g n * LocalKummer.conjMap ρ g m

        conjMap is multiplicative in the kernel argument.

        source
        theorem GQ2.conjMap_conjMap_inv {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (g : AbsGalQ2) (n : β†₯ρ.ker) :
        LocalKummer.conjMap ρ g (LocalKummer.conjMap ρ g⁻¹ n) = n

        conjMap ρ g inverts conjMap ρ g⁻¹.

        source
        theorem GQ2.comp_conjMap_mem_B2 {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (g : AbsGalQ2) {f : β†₯ρ.ker Γ— β†₯ρ.ker β†’ MuN 2} (hf : f ∈ ContCoh.B2 (β†₯ρ.ker) (MuN 2)) :
        (fun (p : β†₯ρ.ker Γ— β†₯ρ.ker) => f (LocalKummer.conjMap ρ g p.1, LocalKummer.conjMap ρ g p.2)) ∈ ContCoh.B2 (β†₯ρ.ker) (MuN 2)

        Coboundary transport along conjugation: precomposition with conjMap Γ— conjMap carries BΒ²(ker ρ, ΞΌβ‚‚) into itself (δ¹ψ ↦ δ¹(ψ ∘ conjMap); the coefficient action is trivial).

        source
        theorem GQ2.comp_conjMap_mem_B2_iff {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (g : AbsGalQ2) {f : β†₯ρ.ker Γ— β†₯ρ.ker β†’ MuN 2} :
        (fun (p : β†₯ρ.ker Γ— β†₯ρ.ker) => f (LocalKummer.conjMap ρ g p.1, LocalKummer.conjMap ρ g p.2)) ∈ ContCoh.B2 (β†₯ρ.ker) (MuN 2) ↔ f ∈ ContCoh.B2 (β†₯ρ.ker) (MuN 2)

        The two-sided form: precomposition with conjMap Γ— conjMap preserves BΒ² in both directions.

        source
        theorem GQ2.conjAct_H1mk {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (g : AbsGalQ2) (a : β†₯(ContCoh.Z1 (β†₯ρ.ker) (ZMod 2))) :
        LocalKummer.conjAct ρ g ((ContCoh.H1mk (β†₯ρ.ker) (ZMod 2)) a) = (ContCoh.H1mk (β†₯ρ.ker) (ZMod 2)) ⟨fun (n : β†₯ρ.ker) => ↑a (LocalKummer.conjMap ρ g n), β‹―βŸ©

        conjAct on an H1mk-class: the mk-level form of conjAct_h1ofFun.

        source
        theorem GQ2.inv_H2mk_eq_of_comp_conjMap {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] (g : AbsGalQ2) (Fc F : β†₯(ContCoh.Z2 (β†₯ρ.ker) (MuN 2))) (hco : ↑Fc = fun (p : β†₯ρ.ker Γ— β†₯ρ.ker) => ↑F (LocalKummer.conjMap ρ g p.1, LocalKummer.conjMap ρ g p.2)) :
        (tateDualityK ρ).inv ((ContCoh.H2mk (β†₯ρ.ker) (MuN 2)) Fc) = (tateDualityK ρ).inv ((ContCoh.H2mk (β†₯ρ.ker) (MuN 2)) F)

        The invariant map kills conjugation: if the cocycle Fc is (pointwise) F precomposed with conjMap Γ— conjMap, the two inv-values agree. ZMod 2-valued, so it suffices that the two classes vanish together β€” and vanishing is BΒ²-membership, transported by comp_conjMap_mem_B2_iff. (Stated with the composition as an equation hypothesis so the call site avoids higher-order unification.)

        source
        theorem GQ2.pairingK_conjAct {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] (g : AbsGalQ2) (x y : ContCoh.H1 (β†₯ρ.ker) (ZMod 2)) :
        ((pairingK ρ) (LocalKummer.conjAct ρ g x)) (LocalKummer.conjAct ρ g y) = ((pairingK ρ) x) y

        (H1) Conjugation invariance of the K-level pairing: B(gΒ·x, gΒ·y) = B(x, y) for the conjAct-action of any g : G_β„šβ‚‚. The transported cup cocycle is on the nose the original precomposed with conjMap Γ— conjMap (the coefficient actions are trivial), and the invariant map kills that precomposition (inv_H2mk_comp_conjMap).

        source
        theorem GQ2.pairingK_conjModule {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] (hρsurj : Function.Surjective ⇑ρ) (c : C) (x y : ContCoh.H1 (β†₯ρ.ker) (ZMod 2)) :
        ((pairingK ρ) (c β€’ x)) (c β€’ y) = ((pairingK ρ) x) y

        (H1) in conjModule form β€” the literal hBinv hypothesis of the abstract hduality (card_equivHoms_deep_eq_quot with instA := conjModule ρ hρsurj).

        The (H3) isotropy splice: pairingK vanishes on deep Γ— deep #

        Eq. (94)'s (U_{e+1}, U_{e+1}) = 1 in class vocabulary. The Tier-5 fact (LocalKummer.cup_deepClasses, over the finite base k with the 𝔽₂-valued trivialCupPairing) splices to pairingK on HΒΉ(ker ρ, 𝔽₂) across two boundaries:

        Since inv_K is injective, vanishing of the HΒ²(ΞΌβ‚‚)-class (= BΒ²-membership of the explicit cup cocycle) forces pairingK = 0. No new leaf: the axioms are tateDualityAt (B6β€²) plus cup_deepClasses's Tier-5 chain.

        source
        def GQ2.kerToFixing {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) (hker : βˆ€ (x : Kummer.GaloisGroup β„š_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (n : β†₯ρ.ker) :
        β†₯k.fixingSubgroup

        The identity inclusion β†₯(ker ρ) β†’ β†₯(k.fixingSubgroup) under a pointwise identification of the kernel with the fixing subgroup (G_K = ker ρ).

        Equations
        Instances For
          source
          theorem GQ2.kerToFixing_mul {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) (hker : βˆ€ (x : Kummer.GaloisGroup β„š_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (n m : β†₯ρ.ker) :
          kerToFixing ρ k hker (n * m) = kerToFixing ρ k hker n * kerToFixing ρ k hker m

          kerToFixing is multiplicative (both sides are the ambient product).

          source
          theorem GQ2.continuous_kerToFixing {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) (hker : βˆ€ (x : Kummer.GaloisGroup β„š_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) :
          Continuous (kerToFixing ρ k hker)

          kerToFixing is continuous (it is the identity on underlying elements).

          source
          theorem GQ2.norm_sub_one_le_of_isMidUnit {N : Subgroup (Kummer.GaloisGroup β„š_[2])} {A : AlgebraicClosure β„š_[2]} (h : IsMidUnit N A) :
          β€–A - 1β€– ≀ β€–2β€–

          Norm bridge for MID units, the ≀-mirror of LocalKummer.norm_sub_one_lt_of_isDeepUnit: A = 1 + 2b with β€–bβ€– ≀ 1 gives β€–A βˆ’ 1β€– ≀ β€–2β€–.

          source
          theorem GQ2.midClass_eq_kummerClassK (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] {ΞΎ : ContCoh.H1 (β†₯k.fixingSubgroup) (ZMod 2)} (hΞΎ : ΞΎ ∈ midClassesSubgroup k.fixingSubgroup) :
          βˆƒ (a : (β†₯k)Λ£), ‖↑↑a - 1β€– ≀ β€–2β€– ∧ kummerClassK k a = ΞΎ

          Bridge midClasses β†’ kummerClassK β€” the ≀-mirror of LocalKummer.deepClass_eq_kummerClassK: over a finite base k, a mid Kummer class in HΒΉ(G_k, 𝔽₂) is the Kummer class of a genuine U_e-unit a ∈ kΛ£ (β€–a βˆ’ 1β€– ≀ β€–2β€–).

          source
          theorem GQ2.cup_midClasses_deepClasses (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] (htriv : βˆ€ (g : β†₯k.fixingSubgroup) (m : ZMod 2), g β€’ m = m) {ΞΎ Ξ· : ContCoh.H1 (β†₯k.fixingSubgroup) (ZMod 2)} (hΞΎ : ΞΎ ∈ midClassesSubgroup k.fixingSubgroup) (hΞ· : Ξ· ∈ LocalKummer.deepClasses k.fixingSubgroup) :
          ((trivialCupPairing 2 (β†₯k.fixingSubgroup) htriv) ΞΎ) Ξ· = 0

          Eq. (94), mid βŸ‚ deep in class vocabulary over the finite base k ((U_e, U_{e+1}) = 1) β€” combines the two kummerClassK bridges with the Tier-5 cup_mid_deep.

          source
          theorem GQ2.pairingK_deep_deep {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] (htriv : βˆ€ (g : β†₯k.fixingSubgroup) (m : ZMod 2), g β€’ m = m) (hker : βˆ€ (x : Kummer.GaloisGroup β„š_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) {ΞΎ Ξ· : ContCoh.H1 (β†₯ρ.ker) (ZMod 2)} (hΞΎ : ΞΎ ∈ deepClassesSubgroup ρ.ker) (hΞ· : Ξ· ∈ deepClassesSubgroup ρ.ker) :
          ((pairingK ρ) ξ) η = 0

          (H3) Isotropy of the deep classes under the K-level pairing: two deep Kummer classes pair to zero. Spliced from the Tier-5 cup_deepClasses as described in the section header.

          source
          theorem GQ2.pairingK_mid_deep {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] (htriv : βˆ€ (g : β†₯k.fixingSubgroup) (m : ZMod 2), g β€’ m = m) (hker : βˆ€ (x : Kummer.GaloisGroup β„š_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) {ΞΎ Ξ· : ContCoh.H1 (β†₯ρ.ker) (ZMod 2)} (hΞΎ : ΞΎ ∈ midClassesSubgroup ρ.ker) (hΞ· : Ξ· ∈ deepClassesSubgroup ρ.ker) :
          ((pairingK ρ) ξ) η = 0

          Mid βŸ‚ deep under the K-level pairing β€” (U_e, U_{e+1}) = 1 spliced to ker ρ (same witness-transport as pairingK_deep_deep, with the Tier-5 input cup_midClasses_deepClasses). The "easy half" of (H4)'s sharpness Deep^βŠ₯ = E.

          source
          theorem GQ2.midClassesSubgroup_le_pairPerp_pairingK {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] (htriv : βˆ€ (g : β†₯k.fixingSubgroup) (m : ZMod 2), g β€’ m = m) (hker : βˆ€ (x : Kummer.GaloisGroup β„š_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) :
          midClassesSubgroup ρ.ker ≀ pairPerp (pairingK ρ) (deepClassesSubgroup ρ.ker)

          The "easy half" of (H4) in pairPerp form: E = midClasses ≀ Deep^βŠ₯ under pairingK. Sharpness (Deep^βŠ₯ ≀ E) follows from this + the cardinality balance #Deep^βŠ₯ = #(M β§Έ Deep) = #E (the counting brick).

          source
          theorem GQ2.deepClassesSubgroup_le_pairPerp_pairingK {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 β†’β‚œ* C) [DiscreteTopology C] [Finite C] (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] (htriv : βˆ€ (g : β†₯k.fixingSubgroup) (m : ZMod 2), g β€’ m = m) (hker : βˆ€ (x : Kummer.GaloisGroup β„š_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) :
          deepClassesSubgroup ρ.ker ≀ pairPerp (pairingK ρ) (deepClassesSubgroup ρ.ker)

          The hiso input of the abstract hduality in pairPerp form: Deep ≀ Deep^βŠ₯ under pairingK.