Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.SelmerStructure

Selmer structures and their Selmer groups #

Let M be a G-module. A Selmer structure on M, relative to a family (H i, N i) of "local" groups and modules, consists of a localisation map H¹(G, M) → H¹(H i, N i) for each index i, given as the pullback along a compatible pair (H i → G, M → N i), together with a local condition: a subgroup of each H¹(H i, N i). Its Selmer group is the subgroup of H¹(G, M) of classes whose every localisation satisfies the local condition,

Sel_𝓕(M) = {c ∈ H¹(G, M) | ∀ i, loc_i c ∈ 𝓕_i}.

In the arithmetic application G is the absolute Galois group of a global field K, M is a discrete G_K-module, the index runs over the places v of K, H v = G_{K_v} maps to G_K through a choice of embedding of separable closures, and N v is the corresponding module over K_v. The m-Selmer group and the Shafarevich–Tate group of an elliptic curve (TauCeti/AlgebraicGeometry/EllipticCurve/GaloisCohomology/Selmer/Basic.lean) are the Selmer groups of two Selmer structures of this kind. Allowing a coefficient map M → N i, rather than restricting the action on M itself, is what lets the local module be formed over a separable closure of the local field. Rubin also requires the local conditions at almost all places to be the unramified classes; that is a property of a Selmer structure over a global field, not part of the data here, and none of the statements below use it.

Main definitions #

Main results #

References #

source
structure TauCeti.ContCohomology.SelmerStructure (G : Type u_1) [Monoid G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [DistribMulAction G M] {ι : Type u_3} (H : ι → Type u_4) [(i : ι) → Monoid (H i)] [(i : ι) → TopologicalSpace (H i)] (N : ι → Type u_5) [(i : ι) → AddCommGroup (N i)] [(i : ι) → TopologicalSpace (N i)] [∀ (i : ι), IsTopologicalAddGroup (N i)] [(i : ι) → DistribMulAction (H i) (N i)] [∀ (i : ι), ContinuousSMul (H i) (N i)] :
Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

A Selmer structure on the G-module M, relative to the local groups H i and local modules N i: for each index i, a compatible pair (groupHom i, coeffHom i) along which H¹(G, M) is localised to H¹(H i, N i), and a local condition subgroup of H¹(H i, N i).

  • groupHom (i : ι) : H i →ₜ* G

    The map from the ith local group to G, such as the inclusion of a decomposition group.

  • coeffHom (i : ι) : M →+ N i

    The map from M to the ith local module.

  • continuous_coeffHom (i : ι) : Continuous ⇑(self.coeffHom i)
  • coeffHom_smul (i : ι) (h : H i) (x : M) : (self.coeffHom i) ((self.groupHom i) h • x) = h • (self.coeffHom i) x
  • localCondition (i : ι) : AddSubgroup (H1 (H i) (N i))

    The local condition at i, a subgroup of H¹(H i, N i).

Instances For
    source
    def TauCeti.ContCohomology.SelmerStructure.localization {G : Type u_1} [Monoid G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {ι : Type u_3} {H : ι → Type u_4} [(i : ι) → Monoid (H i)] [(i : ι) → TopologicalSpace (H i)] {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → TopologicalSpace (N i)] [∀ (i : ι), IsTopologicalAddGroup (N i)] [(i : ι) → DistribMulAction (H i) (N i)] [∀ (i : ι), ContinuousSMul (H i) (N i)] (𝓕 : SelmerStructure G M H N) (i : ι) :
    H1 G M →+ H1 (H i) (N i)

    The localisation map H¹(G, M) → H¹(H i, N i) of a Selmer structure: pullback along the compatible pair (groupHom i, coeffHom i).

    Instances For
      source
      theorem TauCeti.ContCohomology.SelmerStructure.localization_eq_explicitMap1 {G : Type u_1} [Monoid G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {ι : Type u_3} {H : ι → Type u_4} [(i : ι) → Monoid (H i)] [(i : ι) → TopologicalSpace (H i)] {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → TopologicalSpace (N i)] [∀ (i : ι), IsTopologicalAddGroup (N i)] [(i : ι) → DistribMulAction (H i) (N i)] [∀ (i : ι), ContinuousSMul (H i) (N i)] (𝓕 : SelmerStructure G M H N) (i : ι) :
      𝓕.localization i = explicitMap1 G M (H i) (N i) (𝓕.groupHom i) (𝓕.coeffHom i) ⋯ ⋯

      𝓕.localization i is the pullback along (𝓕.groupHom i, 𝓕.coeffHom i).

      source
      def TauCeti.ContCohomology.SelmerStructure.selmerGroup {G : Type u_1} [Monoid G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {ι : Type u_3} {H : ι → Type u_4} [(i : ι) → Monoid (H i)] [(i : ι) → TopologicalSpace (H i)] {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → TopologicalSpace (N i)] [∀ (i : ι), IsTopologicalAddGroup (N i)] [(i : ι) → DistribMulAction (H i) (N i)] [∀ (i : ι), ContinuousSMul (H i) (N i)] (𝓕 : SelmerStructure G M H N) :
      AddSubgroup (H1 G M)

      The Selmer group of a Selmer structure: the classes in H¹(G, M) whose localisation at every index lies in the local condition.

      Instances For
        source
        @[simp]
        theorem TauCeti.ContCohomology.SelmerStructure.mem_selmerGroup_iff {G : Type u_1} [Monoid G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {ι : Type u_3} {H : ι → Type u_4} [(i : ι) → Monoid (H i)] [(i : ι) → TopologicalSpace (H i)] {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → TopologicalSpace (N i)] [∀ (i : ι), IsTopologicalAddGroup (N i)] [(i : ι) → DistribMulAction (H i) (N i)] [∀ (i : ι), ContinuousSMul (H i) (N i)] (𝓕 : SelmerStructure G M H N) {c : H1 G M} :
        c ∈ 𝓕.selmerGroup ↔ ∀ (i : ι), (𝓕.localization i) c ∈ 𝓕.localCondition i

        A class is Selmer exactly when its localisation at every index satisfies the local condition.