feat(ring_theory/dedekind_domain/selmer_group): add Selmer groups of …

…Dedekind domains (#15405)

src/ring_theory/dedekind_domain/selmer_group.lean

@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2022 David Kurniadi Angdinata. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Kurniadi Angdinata
+-/
+
+import data.zmod.quotient
+import ring_theory.dedekind_domain.adic_valuation
+
+/-!
+# Selmer groups of fraction fields of Dedekind domains
+
+Let $K$ be the field of fractions of a Dedekind domain $R$. For any set $S$ of prime ideals in the
+height one spectrum of $R$, and for any natural number $n$, the Selmer group $K(S, n)$ is defined to
+be the subgroup of the unit group $K^\times$ modulo $n$-th powers where each element has $v$-adic
+valuation divisible by $n$ for all prime ideals $v$ away from $S$. In other words, this is precisely
+$$ K(S, n) := \{x(K^\times)^n \in K^\times / (K^\times)^n \ \mid \
+                \forall v \notin S, \ \mathrm{ord}_v(x) \equiv 0 \pmod n\}. $$
+
+There is a fundamental short exact sequence
+$$ 1 \to R_S^\times / (R_S^\times)^n \to K(S, n) \to \mathrm{Cl}_S(R)[n] \to 0, $$
+where $R_S^\times$ is the $S$-unit group of $R$ and $\mathrm{Cl}_S(R)$ is the $S$-class group of
+$R$. If the flanking groups are both finite, then $K(S, n)$ is finite by the first isomorphism
+theorem. Such is the case when $R$ is the ring of integers of a number field $K$, $S$ is finite, and
+$n$ is positive, in which case $R_S^\times$ is finitely generated by Dirichlet's unit theorem and
+$\mathrm{Cl}_S(R)$ is finite by the class number theorem.
+
+This file defines the Selmer group $K(S, n)$ and some basic facts.
+
+## Main definitions
+
+ * `is_dedekind_domain.selmer_group`: the Selmer group.
+ * TODO: maps in the sequence.
+
+## Main statements
+
+ * TODO: proofs of exactness of the sequence.
+ * TODO: proofs of finiteness for global fields.
+
+## Notations
+
+ * `K⟮S, n⟯`: the Selmer group with parameters `K`, `S`, and `n`.
+
+## Implementation notes
+
+The Selmer group is typically defined as a subgroup of the Galois cohomology group $H^1(K, \mu_n)$
+with certain local conditions defined by $v$-adic valuations, where $\mu_n$ is the group of $n$-th
+roots of unity over a separable closure of $K$. Here $H^1(K, \mu_n)$ is identified with
+$K^\times / (K^\times)^n$ by the long exact sequence from Kummer theory and Hilbert's theorem 90,
+and the fundamental short exact sequence becomes an easy consequence of the snake lemma. This file
+will define all the maps explicitly for computational purposes, but isomorphisms to the Galois
+cohomological definition will be provided when possible.
+
+## References
+
+https://doc.sagemath.org/html/en/reference/number_fields/sage/rings/number_field/selmer_group.html
+
+## Tags
+
+class group, selmer group, unit group
+-/
+
+local notation (name := quot) K/n := Kˣ ⧸ (pow_monoid_hom n : Kˣ →* Kˣ).range
+
+namespace is_dedekind_domain
+
+noncomputable theory
+
+open_locale classical discrete_valuation non_zero_divisors
+
+universes u v
+
+variables {R : Type u} [comm_ring R] [is_domain R] [is_dedekind_domain R] {K : Type v} [field K]
+  [algebra R K] [is_fraction_ring R K] (v : height_one_spectrum R)
+
+/-! ### Valuations of non-zero elements -/
+
+namespace height_one_spectrum
+
+/-- The multiplicative `v`-adic valuation on `Kˣ`. -/
+def valuation_of_ne_zero_to_fun (x : Kˣ) : multiplicative ℤ :=
+let hx := is_localization.sec R⁰ (x : K) in multiplicative.of_add $
+  (-(associates.mk v.as_ideal).count (associates.mk $ ideal.span {hx.fst}).factors : ℤ)
+  - (-(associates.mk v.as_ideal).count (associates.mk $ ideal.span {(hx.snd : R)}).factors : ℤ)
+
+@[simp] lemma valuation_of_ne_zero_to_fun_eq (x : Kˣ) :
+  (v.valuation_of_ne_zero_to_fun x : ℤₘ₀) = v.valuation (x : K) :=
+begin
+  change _ = _ * _,
+  rw [units.coe_inv],
+  change _ = ite _ _ _ * (ite (coe _ = _) _ _)⁻¹,
+  rw [is_localization.to_localization_map_sec,
+      if_neg $ is_localization.sec_fst_ne_zero le_rfl x.ne_zero,
+      if_neg $ non_zero_divisors.coe_ne_zero _],
+  any_goals { exact is_domain.to_nontrivial R },
+  refl
+end
+
+/-- The multiplicative `v`-adic valuation on `Kˣ`. -/
+def valuation_of_ne_zero : Kˣ →* multiplicative ℤ :=
+{ to_fun   := v.valuation_of_ne_zero_to_fun,
+  map_one' := by { rw [← with_zero.coe_inj, valuation_of_ne_zero_to_fun_eq], exact map_one _ },
+  map_mul' := λ _ _, by { rw [← with_zero.coe_inj, with_zero.coe_mul],
+                          simp only [valuation_of_ne_zero_to_fun_eq], exact map_mul _ _ _ } }
+
+@[simp] lemma valuation_of_ne_zero_eq (x : Kˣ) :
+  (v.valuation_of_ne_zero x : ℤₘ₀) = v.valuation (x : K) :=
+valuation_of_ne_zero_to_fun_eq v x
+
+@[simp] lemma valuation_of_unit_eq (x : Rˣ) :
+  v.valuation_of_ne_zero (units.map (algebra_map R K : R →* K) x) = 1 :=
+begin
+  rw [← with_zero.coe_inj, valuation_of_ne_zero_eq, units.coe_map, eq_iff_le_not_lt],
+  split,
+  { exact v.valuation_le_one x },
+  { cases x with x _ hx _,
+    change ¬v.valuation (algebra_map R K x) < 1,
+    apply_fun v.int_valuation at hx,
+    rw [map_one, map_mul] at hx,
+    rw [not_lt, ← hx, ← mul_one $ v.valuation _, valuation_of_algebra_map,
+        mul_le_mul_left₀ $ left_ne_zero_of_mul_eq_one hx],
+    exact v.int_valuation_le_one _ }
+end
+
+local attribute [semireducible] mul_opposite
+
+/-- The multiplicative `v`-adic valuation on `Kˣ` modulo `n`-th powers. -/
+def valuation_of_ne_zero_mod (n : ℕ) : K/n →* multiplicative (zmod n) :=
+(int.quotient_zmultiples_nat_equiv_zmod n).to_multiplicative.to_monoid_hom.comp $
+  quotient_group.map (pow_monoid_hom n : Kˣ →* Kˣ).range
+  (add_subgroup.zmultiples (n : ℤ)).to_subgroup v.valuation_of_ne_zero
+begin
+  rintro _ ⟨x, rfl⟩,
+  exact ⟨v.valuation_of_ne_zero x, by simpa only [pow_monoid_hom_apply, map_pow, int.to_add_pow]⟩
+end
+
+@[simp] lemma valuation_of_unit_mod_eq (n : ℕ) (x : Rˣ) :
+  v.valuation_of_ne_zero_mod n (units.map (algebra_map R K : R →* K) x : K/n) = 1 :=
+by rw [valuation_of_ne_zero_mod, monoid_hom.comp_apply, ← quotient_group.coe_mk',
+       quotient_group.map_mk', valuation_of_unit_eq, quotient_group.coe_one, map_one]
+
+end height_one_spectrum
+
+/-! ### Selmer groups -/
+
+variables {S S' : set $ height_one_spectrum R} {n : ℕ}
+
+/-- The Selmer group `K⟮S, n⟯`. -/
+def selmer_group : subgroup $ K/n :=
+{ carrier  := {x : K/n | ∀ v ∉ S, (v : height_one_spectrum R).valuation_of_ne_zero_mod n x = 1},
+  one_mem' := λ _ _, by rw [map_one],
+  mul_mem' := λ _ _ hx hy v hv, by rw [map_mul, hx v hv, hy v hv, one_mul],
+  inv_mem' := λ _ hx v hv, by rw [map_inv, hx v hv, inv_one] }
+
+localized "notation K`⟮`S, n`⟯` := @selmer_group _ _ _ _ K _ _ _ S n" in selmer_group
+
+namespace selmer_group
+
+lemma monotone (hS : S ≤ S') : K⟮S, n⟯ ≤ (K⟮S', n⟯) := λ _ hx v, hx v ∘ mt (@hS v)
+
+/-- The multiplicative `v`-adic valuations on `K⟮S, n⟯` for all `v ∈ S`. -/
+def valuation : K⟮S, n⟯ →* S → multiplicative (zmod n) :=
+{ to_fun   := λ x v, (v : height_one_spectrum R).valuation_of_ne_zero_mod n (x : K/n),
+  map_one' := funext $ λ v, map_one _,
+  map_mul' := λ x y, funext $ λ v, map_mul _ x y }
+
+lemma valuation_ker_eq :
+  valuation.ker = (K⟮(∅ : set $ height_one_spectrum R), n⟯).subgroup_of (K⟮S, n⟯) :=
+begin
+  ext ⟨_, hx⟩,
+  split,
+  { intros hx' v _,
+    by_cases hv : v ∈ S,
+    { exact congr_fun hx' ⟨v, hv⟩ },
+    { exact hx v hv } },
+  { exact λ hx', funext $ λ v, hx' v $ set.not_mem_empty v }
+end
+
+/-- The natural homomorphism from `Rˣ` to `K⟮∅, n⟯`. -/
+def from_unit {n : ℕ} : Rˣ →* K⟮(∅ : set $ height_one_spectrum R), n⟯ :=
+{ to_fun   := λ x, ⟨quotient_group.mk $ units.map (algebra_map R K).to_monoid_hom x,
+                    λ v _, v.valuation_of_unit_mod_eq n x⟩,
+  map_one' := by simpa only [map_one],
+  map_mul' := λ _ _, by simpa only [map_mul] }
+
+lemma from_unit_ker [hn : fact $ 0 < n] :
+  (@from_unit R _ _ _ K _ _ _ n).ker = (pow_monoid_hom n : Rˣ →* Rˣ).range :=
+begin
+  ext ⟨_, _, _, _⟩,
+  split,
+  { intro hx,
+    rcases (quotient_group.eq_one_iff _).mp (subtype.mk.inj hx) with ⟨⟨v, i, vi, iv⟩, hx⟩,
+    have hv : ↑(_ ^ n : Kˣ) = algebra_map R K _ := congr_arg units.val hx,
+    have hi : ↑(_ ^ n : Kˣ)⁻¹ = algebra_map R K _ := congr_arg units.inv hx,
+    rw [units.coe_pow] at hv,
+    rw [← inv_pow, units.inv_mk, units.coe_pow] at hi,
+    rcases @is_integrally_closed.exists_algebra_map_eq_of_is_integral_pow R _ _ _ _ _ _ _ v _
+      hn.out (hv.symm ▸ is_integral_algebra_map) with ⟨v', rfl⟩,
+    rcases @is_integrally_closed.exists_algebra_map_eq_of_is_integral_pow R _ _ _ _ _ _ _ i _
+      hn.out (hi.symm ▸ is_integral_algebra_map) with ⟨i', rfl⟩,
+    rw [← map_mul, map_eq_one_iff _ $ no_zero_smul_divisors.algebra_map_injective R K] at vi,
+    rw [← map_mul, map_eq_one_iff _ $ no_zero_smul_divisors.algebra_map_injective R K] at iv,
+    rw [units.coe_mk, ← map_pow] at hv,
+    exact ⟨⟨v', i', vi, iv⟩, by simpa only [units.ext_iff, pow_monoid_hom_apply, units.coe_pow]
+                               using no_zero_smul_divisors.algebra_map_injective R K hv⟩ },
+  { rintro ⟨_, hx⟩,
+    rw [← hx],
+    exact subtype.mk_eq_mk.mpr
+      ((quotient_group.eq_one_iff _).mpr ⟨_, by simp only [pow_monoid_hom_apply, map_pow]⟩) }
+end
+
+/-- The injection induced by the natural homomorphism from `Rˣ` to `K⟮∅, n⟯`. -/
+def from_unit_lift [fact $ 0 < n] : R/n →* K⟮(∅ : set $ height_one_spectrum R), n⟯ :=
+(quotient_group.ker_lift _).comp
+  (quotient_group.quotient_mul_equiv_of_eq from_unit_ker).symm.to_monoid_hom
+
+lemma from_unit_lift_injective [fact $ 0 < n] :
+  function.injective $ @from_unit_lift R _ _ _ K _ _ _ n _ :=
+function.injective.comp (quotient_group.ker_lift_injective _) (mul_equiv.injective _)
+
+end selmer_group
+
+end is_dedekind_domain