Homomorphism estensionnality

Stream: Is there code for X?

[Julien Marquet]

I proved this :

import data.real.cau_seq
import ring_theory.unique_factorization_domain

open is_absolute_value
open_locale classical

theorem ext_hom_primes {α} [comm_monoid_with_zero α] [wf_dvd_monoid α]
  {β} [monoid_with_zero β]
  (φ₁ φ₂: monoid_with_zero_hom α β)
  (h_units: ∀ u: units α, φ₁ u = φ₂ u)
  (h_irreducibles: ∀ a: α, irreducible a → φ₁ a = φ₂ a):
    (φ₁: α → β) = φ₂ :=
begin
  rw ← monoid_with_zero_hom.to_fun_eq_coe,
  rw ← monoid_with_zero_hom.to_fun_eq_coe,
  ext x,
  exact wf_dvd_monoid.induction_on_irreducible x
    (by rw [φ₁.map_zero', φ₂.map_zero'])
    (by {
      rintros _ ⟨ u, rfl ⟩,
      exact h_units u,
    })
    (by {
      intros a i ha hi hφa,
      simp only [monoid_with_zero_hom.map_mul, monoid_with_zero_hom.to_fun_eq_coe],
      rw h_irreducibles i hi,
      rw ← monoid_with_zero_hom.to_fun_eq_coe φ₁,
      rw hφa,
      refl,
    }),
end

I wanted to PR this to mathlib, but I don't really know where to put it.
(Also I'm not entierely sure if this is the right way to formulate it.)

[Kenny Lau]

why not make the goal φ₁ = φ₂

[Julien Marquet]

It actually seemed more natural in the context where I used it but now you say it...

[Eric Wieser]

The homomorphism arguments should be implicit too

[Eric Wieser]

And you shouldn't need to rewrite them into to_fun, use the unprimed map_zero instead of the primed one

[Julien Marquet]

I didn't notice the unprimed version, thanks !

[Eric Wieser]

The primed ones only exist because the has_coe_to_fun instance can't be set up early enough to avoid them