class_group.lean

/-
Copyright (c) 2021 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Anne Baanen
-/

import group_theory.quotient_group
import ring_theory.dedekind_domain

/-!
# The ideal class group

This file defines the ideal class group `class_group f` of fractional ideals
with respect to the fraction map `f`.

## Main definitions
 - `to_principal_ideal` sends an invertible `x : f.codomain` to an invertible fractional ideal
 - `class_group` is the quotient of invertible fractional ideals modulo `to_principal_ideal.range`
 - `class_group.mk0` sends a nonzero integral ideal in a Dedekind domain to its class

## Main results
 - `class_group.mk0_eq_mk0_iff` shows the equivalence with the "classical" definition,
   where `I ~ J` iff `x I = y J` for `x y ≠ (0 : R)`
-/

open ring
open ring.fractional_ideal

section integral_domain

variables {R K L : Type*} [integral_domain R]
variables [field K] [field L] [decidable_eq L]
variables (f : fraction_map R K)
variables [algebra f.codomain L] [finite_dimensional f.codomain L]
variables [algebra R L] [is_scalar_tower R f.codomain L]

open ring.fractional_ideal units

section
/-- `to_principal_ideal x` sends `x ≠ 0 : K` to the fractional ideal generated by `x` -/
@[irreducible]
def to_principal_ideal : units f.codomain →* units (fractional_ideal f) :=
{ to_fun := λ x,
  ⟨ span_singleton x,
    span_singleton x⁻¹,
    by simp only [span_singleton_one, units.mul_inv', span_singleton_mul_span_singleton],
    by simp only [span_singleton_one, units.inv_mul', span_singleton_mul_span_singleton]⟩,
  map_mul' := λ x y, ext
    (by simp only [units.coe_mk, units.coe_mul, span_singleton_mul_span_singleton]),
  map_one' := ext (by simp only [span_singleton_one, units.coe_mk, units.coe_one]) }

local attribute [semireducible] to_principal_ideal

variables {f}

@[simp] lemma coe_to_principal_ideal (x : units f.codomain) :
  (to_principal_ideal f x : fractional_ideal f) = span_singleton x :=
rfl

@[simp] lemma to_principal_ideal_eq_iff {I : units (fractional_ideal f)} {x : units f.codomain} :
  to_principal_ideal f x = I ↔ span_singleton (x : f.codomain) = I :=
units.ext_iff

end

instance principal_ideals.normal : (to_principal_ideal f).range.normal :=
subgroup.normal_of_comm _

section
/-- The class group with respect to `f : fraction_map R K`
is the group of invertible fractional ideals modulo the principal ideals. -/
@[derive(comm_group)]
def class_group := quotient_group.quotient (to_principal_ideal f).range

instance : inhabited (class_group f) := ⟨1⟩

@[simp] lemma fractional_ideal.coe_to_fractional_ideal_top :
  ((⊤ : ideal R) : fractional_ideal f) = 1 :=
by { rw [← ideal.one_eq_top], refl }

@[simp] lemma units.mk0_one {M : Type*} [group_with_zero M] (h) :
  units.mk0 (1 : M) h = 1 :=
by { ext, refl }

@[simp] lemma units.mk0_map {M : Type*} [group_with_zero M] (x y : M) (hxy) :
  mk0 (x * y) hxy = mk0 x (mul_ne_zero_iff.mp hxy).1 * mk0 y (mul_ne_zero_iff.mp hxy).2 :=
by { ext, refl }

/-- The monoid of nonzero ideals. -/
def nonzero_ideal (R : Type*) [integral_domain R] : submonoid (ideal R) :=
{ carrier := {I | I ≠ ⊥},
  one_mem' := show (1 : ideal R) ≠ ⊥, by { rw ideal.one_eq_top, exact submodule.bot_ne_top.symm },
  mul_mem' := λ I J (hI : I ≠ ⊥) (hJ : J ≠ ⊥), show I * J ≠ ⊥,
    by { obtain ⟨x, x_mem, x_ne⟩ := I.ne_bot_iff.mp hI,
         obtain ⟨y, y_mem, y_ne⟩ := J.ne_bot_iff.mp hJ,
         exact (submodule.ne_bot_iff _).mpr
           ⟨x * y, ideal.mul_mem_mul x_mem y_mem, mul_ne_zero x_ne y_ne⟩ } }

/-- Send a nonzero ideal to the corresponding class in the class group. -/
noncomputable def class_group.mk0 [is_dedekind_domain R] :
  nonzero_ideal R →* class_group f :=
(quotient_group.mk' _).comp
  { to_fun := λ I, units.mk0 I
      ((fractional_ideal.coe_to_fractional_ideal_ne_zero (le_refl (non_zero_divisors R))).mpr I.2),
    map_one' := by simp,
    map_mul' := λ x y, by simp }

lemma quotient_group.mk'_eq_mk' {G : Type*} [group G] {N : subgroup G} [hN : N.normal] {x y : G} :
  quotient_group.mk' N x = quotient_group.mk' N y ↔ ∃ z ∈ N, x * z = y :=
(@quotient.eq _ (quotient_group.left_rel _) _ _).trans
  ⟨λ (h : x⁻¹ * y ∈ N), ⟨_, h, by rw [← mul_assoc, mul_right_inv, one_mul]⟩,
   λ ⟨z, z_mem, eq_y⟩,
     by { rw ← eq_y, show x⁻¹ * (x * z) ∈ N, rwa [← mul_assoc, mul_left_inv, one_mul] }⟩

lemma ideal.mem_mul_span_singleton {x y : R} {I : ideal R} :
  x ∈ I * ideal.span {y} ↔ ∃ z ∈ I, z * y = x :=
submodule.mem_smul_span_singleton

lemma ideal.mem_span_singleton_mul {x y : R} {I : ideal R} :
  x ∈ ideal.span {y} * I ↔ ∃ z ∈ I, y * z = x :=
by simp only [mul_comm, ideal.mem_mul_span_singleton]

lemma ideal.le_span_singleton_mul_iff {x : R} {I J : ideal R} :
  I ≤ ideal.span {x} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI :=
show (∀ {zI} (hzI : zI ∈ I), zI ∈ ideal.span {x} * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI,
by simp only [ideal.mem_span_singleton_mul]

lemma ideal.span_singleton_mul_le_iff {x : R} {I J : ideal R} :
  ideal.span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J :=
begin
  simp only [ideal.mul_le, ideal.mem_span_singleton_mul, ideal.mem_span_singleton],
  split,
  { intros h zI hzI,
    exact h x (dvd_refl x) zI hzI },
  { rintros h _ ⟨z, rfl⟩ zI hzI,
    rw [mul_comm x z, mul_assoc],
    exact J.mul_mem_left _ (h zI hzI) },
end

lemma ideal.span_singleton_mul_le_span_singleton_mul {x y : R} {I J : ideal R} :
  ideal.span {x} * I ≤ ideal.span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ :=
by simp only [ideal.span_singleton_mul_le_iff, ideal.mem_span_singleton_mul, eq_comm]

lemma ideal.eq_singleton_mul {x : R} (I J : ideal R) :
  I = ideal.span {x} * J ↔ ((∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ (∀ z ∈ J, x * z ∈ I)) :=
by simp only [le_antisymm_iff, ideal.le_span_singleton_mul_iff, ideal.span_singleton_mul_le_iff]

lemma ideal.singleton_mul_eq_singleton_mul {x y : R} (I J : ideal R) :
  ideal.span {x} * I = ideal.span {y} * J ↔
    ((∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧
     (∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ)) :=
by simp only [le_antisymm_iff, ideal.span_singleton_mul_le_span_singleton_mul, eq_comm]

lemma fractional_ideal.le_span_singleton_mul_iff {x : f.codomain} {I J : fractional_ideal f} :
  I ≤ span_singleton x * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI :=
show (∀ {zI} (hzI : zI ∈ I), zI ∈ span_singleton x * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI,
by { simp only [fractional_ideal.mem_singleton_mul, eq_comm], refl }

lemma fractional_ideal.span_singleton_mul_le_iff {x : f.codomain} {I J : fractional_ideal f} :
  span_singleton x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J :=
begin
  simp only [fractional_ideal.mul_le, fractional_ideal.mem_singleton_mul,
             fractional_ideal.mem_span_singleton],
  split,
  { intros h zI hzI,
    exact h x ⟨1, one_smul _ _⟩ zI hzI },
  { rintros h _ ⟨z, rfl⟩ zI hzI,
    rw [algebra.smul_mul_assoc],
    exact submodule.smul_mem J.1 _ (h zI hzI) },
end

lemma fractional_ideal.eq_span_singleton_mul {x : f.codomain} {I J : fractional_ideal f} :
  I = span_singleton x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I :=
by simp only [le_antisymm_iff, fractional_ideal.le_span_singleton_mul_iff,
              fractional_ideal.span_singleton_mul_le_iff]

lemma class_group.mk0_eq_mk0_iff [is_dedekind_domain R]
  (I J : nonzero_ideal R) :
  class_group.mk0 f I = class_group.mk0 f J ↔
    ∃ (x y : R) (hx : x ≠ 0) (hy : y ≠ 0), ideal.span {x} * (I : ideal R) = ideal.span {y} * J :=
begin
  simp only [class_group.mk0, monoid_hom.comp_apply, monoid_hom.coe_mk, quotient_group.mk'_eq_mk',
    exists_prop, monoid_hom.mem_range, ideal.singleton_mul_eq_singleton_mul],
  split,
  { rintros ⟨z, ⟨xy, hxy, rfl⟩, eq_J⟩,
    have : (J : fractional_ideal f) = (span_singleton xy * I),
    { simpa only [mul_comm, eq_comm, coe_mk0, monoid_hom.to_fun_eq_coe, coe_to_principal_ideal,
                  units.coe_mul]
        using congr_arg (coe : _ → fractional_ideal f) eq_J },
    obtain ⟨hJI, hIJ⟩ := (fractional_ideal.eq_span_singleton_mul _).mp this,
    have hx : (f.to_localization_map.sec (xy : f.codomain)).1 ≠ 0,
    { suffices : f.to_map (f.to_localization_map.sec (xy : f.codomain)).1 ≠ 0,
      { refine mt (λ h, _) this,
        rw [h, ring_hom.map_zero] },
      rw [ne.def, ← localization_map.sec_spec (xy : f.codomain), mul_eq_zero],
      push_neg,
      use xy.ne_zero,
      exact f.to_map_ne_zero_of_mem_non_zero_divisors _ },
    use [(f.to_localization_map.sec (xy : f.codomain)).1,
         (f.to_localization_map.sec (xy : f.codomain)).2,
         hx,
         non_zero_divisors.ne_zero_of_mem (f.to_localization_map.sec (xy : f.codomain)).2.2],
    have x_eq : (xy * f.to_map (f.to_localization_map.sec (xy : f.codomain)).2 : f.codomain) =
        f.to_map (f.to_localization_map.sec (xy : f.codomain)).1 :=
      localization_map.sec_spec (xy : f.codomain),
    split,
    { intros zI hzI,
      obtain ⟨zJ, hzJ, (zJ_eq : f.to_map zJ = _ * f.to_map _)⟩ := hIJ (f.to_map zI) _,
      { use [zJ, hzJ],
        apply f.injective,
        rw [f.to_map.map_mul, f.to_map.map_mul, zJ_eq, ← x_eq],
        ac_refl },
      { simpa only [exists_prop, mem_coe_ideal, exists_mem_to_map_eq, coe_coe] using hzI } },
    { intros zJ hzJ,
      obtain ⟨zI', hzI', eq_zJ⟩ := hJI (f.to_map zJ) _,
      obtain ⟨zI, hzI, rfl⟩ := fractional_ideal.mem_coe_ideal.mp hzI',
      { use [zI, hzI],
        apply f.injective,
        rw [f.to_map.map_mul, f.to_map.map_mul, ← eq_zJ, ← x_eq],
        ac_refl },
      { simpa only [exists_prop, mem_coe_ideal, exists_mem_to_map_eq, coe_coe] using hzJ } } },
  { rintros ⟨x, y, hx, hy, hIJ, hJI⟩,
    have hy' := mem_non_zero_divisors_iff_ne_zero.mpr hy,
    refine ⟨_, ⟨units.mk0 (f.mk' x ⟨y, hy'⟩) _, rfl⟩, _⟩,
    { rw [ne.def, f.mk'_eq_iff_eq_mul, zero_mul],
      exact mt (f.to_map.injective_iff.mp f.injective _) hx },
    suffices : (J : fractional_ideal f) = span_singleton (f.mk' x ⟨y, _⟩) * I,
    { apply units.ext,
      simpa only [mul_comm, eq_comm, coe_mk0, coe_to_principal_ideal, units.coe_mul] using this },
    refine (fractional_ideal.eq_span_singleton_mul _).mpr ⟨_, _⟩,
    { intros zJ' hzJ',
      obtain ⟨zJ, hzJ, rfl⟩ := mem_coe_ideal.mp hzJ',
      obtain ⟨zI, hzI, x_mul_eq_y_mul⟩ := hJI zJ hzJ,
      refine ⟨f.to_map zI, mem_coe_ideal.mpr ⟨zI, hzI, rfl⟩, _⟩,
      apply mul_left_cancel' (f.to_map_ne_zero_of_mem_non_zero_divisors ⟨y, hy'⟩),
      rw [← mul_assoc, localization_map.mk'_spec', ← ring_hom.map_mul, ← ring_hom.map_mul,
          x_mul_eq_y_mul, subtype.coe_mk] },
    { intros zI' hzI',
      obtain ⟨zI, hzI, rfl⟩ := mem_coe_ideal.mp hzI',
      obtain ⟨zJ, hzJ, x_mul_eq_y_mul⟩ := hIJ zI hzI,
      refine mem_coe_ideal.mpr ⟨zJ, hzJ, _⟩,
      apply mul_left_cancel' (f.to_map_ne_zero_of_mem_non_zero_divisors ⟨y, hy'⟩),
      rw [← mul_assoc, localization_map.mk'_spec', ← ring_hom.map_mul, ← ring_hom.map_mul,
          x_mul_eq_y_mul, subtype.coe_mk] } },
end

lemma class_group.mk0_surjective [is_dedekind_domain R] : function.surjective (class_group.mk0 f) :=
begin
  rintros ⟨I⟩,
  obtain ⟨a, a_ne_zero', ha⟩ := I.1.2,
  have a_ne_zero := non_zero_divisors.ne_zero_of_mem a_ne_zero',
  have fa_ne_zero : f.to_map a ≠ 0 := f.to_map_ne_zero_of_mem_non_zero_divisors ⟨a, a_ne_zero'⟩,
  refine ⟨⟨{ carrier := { x | (f.to_map a)⁻¹ * f.to_map x ∈ I.1 }, .. }, _⟩, _⟩,
  { simp only [ring_hom.map_zero, set.mem_set_of_eq, mul_zero, ring_hom.map_mul],
    exact submodule.zero_mem I },
  { simp only [ring_hom.map_add, set.mem_set_of_eq, mul_zero, ring_hom.map_mul, mul_add],
    exact λ _ _ ha hb, submodule.add_mem I ha hb },
  { simp only [smul_eq_mul, set.mem_set_of_eq, mul_zero, ring_hom.map_mul, mul_add,
               mul_left_comm (f.to_map a)⁻¹],
    exact λ c _ hb, submodule.smul_mem I c hb },
  { apply (submodule.ne_bot_iff _).mpr,
    obtain ⟨x, x_ne, x_mem⟩ := exists_ne_zero_mem_is_integer I.ne_zero,
    refine ⟨a * x, _, mul_ne_zero a_ne_zero x_ne⟩,
    change (f.to_map a)⁻¹ * f.to_map (a * x) ∈ I.1,
    rwa [ring_hom.map_mul, ← mul_assoc, inv_mul_cancel fa_ne_zero, one_mul] },
  { symmetry,
    apply quotient.sound,
    refine ⟨units.mk0 (f.to_map a) fa_ne_zero, _⟩,
    apply @mul_left_cancel _ _ I,
    rw [← mul_assoc, mul_right_inv, one_mul, eq_comm, mul_comm I],
    simp only [monoid_hom.coe_mk, subtype.coe_mk, ring_hom.map_mul, coe_coe],
    apply units.ext,
    simp only [units.coe_mul, coe_to_principal_ideal, coe_mk0,
               fractional_ideal.eq_span_singleton_mul],
    split,
    { intros zJ' hzJ',
      obtain ⟨zJ, hzJ : (f.to_map a)⁻¹ * f.to_map zJ ∈ (I : fractional_ideal f), rfl⟩ :=
        mem_coe_ideal.mp hzJ',
      refine ⟨_, hzJ, _⟩,
      rw [← mul_assoc, mul_inv_cancel fa_ne_zero, one_mul] },
    { intros zI' hzI',
      rw mem_coe_ideal,
      obtain ⟨y, hy⟩ := ha zI' hzI',
      refine ⟨y, _, hy⟩,
      show (f.to_map a)⁻¹ * f.to_map y ∈ (I : fractional_ideal f),
      rwa [hy, ← mul_assoc, inv_mul_cancel fa_ne_zero, one_mul] } }
end

end

instance submodule.is_principal_bot {R M : Type*} [ring R] [add_comm_group M] [module R M] :
  (⊥ : submodule R M).is_principal :=
⟨⟨0, submodule.span_zero_singleton.symm⟩⟩

lemma class_group.mk_eq_one_iff [is_dedekind_domain R]
  {I : units (fractional_ideal f)} :
  quotient_group.mk' (to_principal_ideal f).range I = 1 ↔
    (I : submodule R f.codomain).is_principal :=
begin
  rw [← (quotient_group.mk' _).map_one, eq_comm, quotient_group.mk'_eq_mk'],
  simp only [exists_prop, one_mul, exists_eq_right, to_principal_ideal_eq_iff,
             monoid_hom.mem_range, coe_coe],
  refine ⟨λ ⟨x, hx⟩, ⟨⟨x, by rw [← hx, coe_span_singleton]⟩⟩, _⟩,
  unfreezingI { intros hI },
  obtain ⟨x, hx⟩ := @submodule.is_principal.principal _ _ _ _ _ _ hI,
  have hx' : (I : fractional_ideal f) = span_singleton x,
  { apply subtype.coe_injective, rw [hx, coe_span_singleton] },
  refine ⟨units.mk0 x _, _⟩,
  { intro x_eq, apply units.ne_zero I, simp [hx', x_eq] },
  simp [hx']
end

@[simp] lemma localization_map.to_map_mem_coe_submodule {I : ideal R} {x : R} :
  f.to_map x ∈ f.coe_submodule I ↔ x ∈ I :=
(localization_map.mem_coe_submodule _).trans
  ⟨λ ⟨y, hy, y_eq⟩, by rwa ← f.injective y_eq,
   λ hx, ⟨x, hx, rfl⟩⟩

@[simp]
lemma localization_map.coe_submodule_injective : function.injective f.coe_submodule :=
λ I J h, submodule.ext (λ x, by simp only [← f.to_map_mem_coe_submodule, h])

@[simp]
lemma localization_map.coe_submodule_le {I : ideal R} {J : submodule R f.codomain} :
  f.coe_submodule I ≤ J ↔ submodule.map f.lin_coe I ≤ J :=
iff.rfl

@[simp]
lemma localization_map.coe_submodule_span_singleton (x : R) :
  f.coe_submodule (submodule.span R {x}) = submodule.span R {f.to_map x} :=
by rw [localization_map.coe_submodule, submodule.map_span, set.image_singleton,
       localization_map.lin_coe_apply]

@[simp]
lemma localization_map.coe_submodule_is_principal {I : ideal R} :
  (f.coe_submodule I).is_principal ↔ I.is_principal :=
begin
  split;
    unfreezingI { intros hI };
    obtain ⟨x, hx⟩ := @submodule.is_principal.principal _ _ _ _ _ _ hI,
  { have x_mem : x ∈ f.coe_submodule I := hx.symm ▸ submodule.mem_span_singleton_self x,
    obtain ⟨x, x_mem, rfl⟩ := (localization_map.mem_coe_submodule _).mp x_mem,
    refine ⟨⟨x, localization_map.coe_submodule_injective f _⟩⟩,
    rw [hx, localization_map.coe_submodule_span_singleton] },
  { refine ⟨⟨f.to_map x, _⟩⟩,
    rw [hx, f.coe_submodule_span_singleton] }
end

lemma class_group.mk0_eq_one_iff [is_dedekind_domain R]
  {I : ideal R} (hI : I ≠ 0) :
  class_group.mk0 f ⟨I, hI⟩ = 1 ↔ I.is_principal :=
(class_group.mk_eq_one_iff _).trans f.coe_submodule_is_principal

/-- The class number is `1` iff the ring of integers is a principal ideal domain. -/
lemma card_class_group_eq_one_iff [is_dedekind_domain R] [fintype (class_group f)] :
  fintype.card (class_group f) = 1 ↔ is_principal_ideal_ring R :=
begin
  rw fintype.card_eq_one_iff,
  split,
  { rintros ⟨I, hI⟩,
    have eq_one : ∀ J : class_group f, J = 1 := λ J, trans (hI J) (hI 1).symm,
    refine ⟨λ I, _⟩,
    by_cases hI : I = ⊥,
    { rw hI, exact submodule.is_principal_bot },
    exact (class_group.mk0_eq_one_iff f hI).mp (eq_one _) },
  { unfreezingI { intros hpid },
    use 1,
    rintros ⟨I⟩,
    exact (class_group.mk_eq_one_iff f).mpr (I : fractional_ideal f).is_principal }
end

end integral_domain