(ZMod m) ⧸ span {(n : ZMod m)} ≃+* (ZMod (m.gcd n))

Stream: Is there code for X?

[张守信(Shouxin Zhang)]

Is there a similar conclusion to this very elegant conclusion in the library? Or, can it be proved in less than 5 lines?

open Function Ideal in
noncomputable def ZModEquiv (m n : ℕ) : (ZMod m) ⧸ span {(n : ZMod m)} ≃+* (ZMod (m.gcd n)) := by
  by_cases hm : m = 0
  . rw [show m.gcd n = n by simp [hm]]
    show ZMod m ⧸ span {(n : ZMod m)} ≃+* ZMod n
    let e : ZMod 0 ≃+* ℤ := by rfl
    have h_map : Ideal.map e (span {(n : ZMod 0)}) = Ideal.span {(n : ℤ)} := by
      erw [@map_span, Set.image_singleton, map_natCast]
    apply RingEquiv.trans ?_ (h_map ▸ Int.quotientSpanEquivZMod n)
    exact Ideal.quotientEquiv _ _ (by rw [hm]; exact e) (by simp [map_span])
  letI : NeZero m := by exact { out := hm }
  let g := m.gcd n
  have h_dvd : g ∣ m := Nat.gcd_dvd_left m n
  let φ : ZMod m →+* ZMod g := ZMod.castHom h_dvd _
  have hφ_surj : Surjective φ := by
    unfold φ
    exact ZMod.ringHom_surjective (ZMod.castHom h_dvd (ZMod g))
  have h_ker_g : RingHom.ker φ = Ideal.span {↑g} := by
    unfold φ
    ext x
    rw [@RingHom.mem_ker, ZMod.castHom_apply, @mem_span_singleton]
    rw [ZMod.cast_eq_val, ZMod.natCast_zmod_eq_zero_iff_dvd]
    constructor
    . intro hx
      rw [← ZMod.natCast_zmod_val x]
      exact Nat.cast_dvd_cast hx
    . intro hx
      obtain ⟨k, rfl⟩ := hx
      rw [← ZMod.natCast_zmod_val k, ZMod.val_mul]
      simp [Nat.dvd_mod_iff h_dvd]
  have h_span_eq : Ideal.span {(m.gcd n : ZMod m)} = Ideal.span {(n : ZMod m)} := by
    ext x; simp [@mem_span_singleton, g]
    refine ⟨fun hx => ?_, fun hx => ?_⟩
    . obtain ⟨k, rfl⟩ := hx
      refine Dvd.dvd.mul_right ?_ k; clear k
      rw [← Int.cast_natCast (m.gcd n), Nat.gcd_eq_gcd_ab]
      simp
    . exact (Nat.cast_dvd_cast (Nat.gcd_dvd_right m n)).trans hx
  let iso1 := RingHom.quotientKerEquivOfSurjective hφ_surj
  let iso2 := quotEquivOfEq h_span_eq
  unfold g at *
  exact RingEquiv.trans iso2.symm (RingEquiv.trans (quotEquivOfEq h_ker_g.symm) iso1)

[Aaron Liu]

import Mathlib

open Ideal

def ZModEquiv (m n : ℕ) : (ZMod m) ⧸ span {(n : ZMod m)} ≃+* (ZMod (m.gcd n)) :=
  haveI : CharP (ZMod m ⧸ span {(n : ZMod m)}) (m.gcd n) := sorry
  RingEquiv.ofRingHom
    (Ideal.Quotient.lift (span {(n : ZMod m)})
      (ZMod.castHom (Nat.gcd_dvd_left m n) (ZMod (m.gcd n))) <| by
        intro a ha
        obtain ⟨a, rfl⟩ := ZMod.intCast_surjective a
        rw [mem_span_singleton] at ha
        apply (ZMod.castHom (Nat.gcd_dvd_left m n) (ZMod (m.gcd n))).map_dvd at ha
        simpa [(ZMod.natCast_zmod_eq_zero_iff_dvd ..).mpr (Nat.gcd_dvd_right m n)] using ha)
    ((ZMod.castHom dvd_rfl (ZMod m ⧸ span {(n : ZMod m)})))
    (by
      ext x
      obtain ⟨x, rfl⟩ := ZMod.intCast_surjective x
      simp)
    (by
      ext x
      obtain ⟨x, rfl⟩ := ZMod.intCast_surjective x
      simp)

[Aaron Liu]

Not 5 lines, but this doesn't have by_cases, so I think it's more "canonical".

[张守信(Shouxin Zhang)]

I think maybe we should also have a Zulip stream/topic specifically for asking if theorems one intends to prove are already duplicated in the library (API check). Subsequently, this would facilitate submitting useful supplementary theorems to mathlib4. It might reduce distraction/noise in threads that are really focused on proof golfing, so people who need that kind of help can get more attention. And increase the number of useful PRs.

[Ruben Van de Velde]

That's this stream

[张守信(Shouxin Zhang)]

Aaron Liu said:

Not 5 lines, but this doesn't have by_cases, so I think it's more "canonical".

The instance prove seems not trivial.

[Aaron Liu]

Oh, I forgot that one part

[Aaron Liu]

Hold on, let me fix it

[张守信(Shouxin Zhang)]

Ruben Van de Velde said:

That's this stream

I disagree with this, because needing a proof and asking if the API has a simple implementation of a library theorem are actually very different. :penguin:

[Kevin Buzzard]

It's what this stream is used for in practice

[Johan Commelin]

... and in theory

as far as I know