OpenDivisorResidues.lean

def openKummerUnits (S : Set (Place K F)) (n : ℕ+) : Subgroup Fˣ where
  carrier := {u | ∀ v : Place K F, v ∉ S → (n : ℤ) ∣ v.ord (u : F)}
  one_mem' := by
    intro v _
    rw [Units.val_one, v.ord_one]
    exact dvd_zero _
  mul_mem' := by
    intro u w hu hw v hv
    rw [Units.val_mul, v.ord_mul (Units.ne_zero u) (Units.ne_zero w)]
    exact dvd_add (hu v hv) (hw v hv)
  inv_mem' := by
    intro u hu v hv
    rw [Units.val_inv_eq_inv_val, v.ord_inv]
    exact dvd_neg.mpr (hu v hv)

def openKummerPowers (S : Set (Place K F)) (n : ℕ+) :
    Subgroup (openKummerUnits K F S n)

def openKummerResidue (S : Set (Place K F)) (n : ℕ+) :
    openKummerUnits K F S n →* Multiplicative (S → ZMod (n : ℕ)) where
  toFun u := Multiplicative.ofAdd (fun v => (v.val.ord (u.val : F) : ZMod (n : ℕ)))
  map_one' := by
    apply Multiplicative.toAdd.injective
    funext v
    change (v.val.ord (1 : F) : ZMod (n : ℕ)) = 0
    rw [v.val.ord_one, Int.cast_zero]
  map_mul' u w := by
    apply Multiplicative.toAdd.injective
    funext v
    change (v.val.ord ((u.val : F) * (w.val : F)) : ZMod (n : ℕ)) =
      (v.val.ord (u.val : F) : ZMod (n : ℕ)) +
        (v.val.ord (w.val : F) : ZMod (n : ℕ))
    rw [v.val.ord_mul (Units.ne_zero u.val) (Units.ne_zero w.val), Int.cast_add]

theorem openKummerResidue_eq_one_iff
    (S : Set (Place K F)) (n : ℕ+) (u : openKummerUnits K F S n) :
    openKummerResidue S n u = 1 ↔ u.val ∈ kummerUnits K F n

theorem openKummerPowers_le_residue_ker
    (S : Set (Place K F)) (n : ℕ+) :
    openKummerPowers K F S n ≤ (openKummerResidue S n).ker

def openKummerResidueQuotient (S : Set (Place K F)) (n : ℕ+) :
    openKummerUnits K F S n ⧸ openKummerPowers K F S n →*
      Multiplicative (S → ZMod (n : ℕ))

theorem openKummerResidueQuotient_mk
    (S : Set (Place K F)) (n : ℕ+) (u : openKummerUnits K F S n) :
    openKummerResidueQuotient S n (QuotientGroup.mk u) =
      openKummerResidue S n u

def kummerUnitsToOpen (S : Set (Place K F)) (n : ℕ+) :
    kummerUnits K F n →* openKummerUnits K F S n where
  toFun u := ⟨u.val, fun v _ => u.property v⟩
  map_one' := rfl
  map_mul' _ _ := rfl

def kummerQuotientToOpen (S : Set (Place K F)) (n : ℕ+) :
    kummerUnits K F n ⧸ kummerPowers K F n →*
      openKummerUnits K F S n ⧸ openKummerPowers K F S n

theorem kummerQuotientToOpen_injective (S : Set (Place K F)) (n : ℕ+) :
    Function.Injective (kummerQuotientToOpen S n)

theorem kummerQuotientToOpen_range
    (S : Set (Place K F)) (n : ℕ+) :
    (kummerQuotientToOpen S n).range =
      (openKummerResidueQuotient S n).ker