## Stream: Is there code for X?

### Topic: Homomorphism estensionnality

#### Julien Marquet (Feb 11 2021 at 08:59):

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 (Feb 11 2021 at 09:02):

why not make the goal φ₁ = φ₂

#### Julien Marquet (Feb 11 2021 at 09:10):

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

#### Eric Wieser (Feb 11 2021 at 09:14):

The homomorphism arguments should be implicit too

#### Eric Wieser (Feb 11 2021 at 09:15):

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

#### Julien Marquet (Feb 11 2021 at 09:30):

I didn't notice the unprimed version, thanks !

#### Eric Wieser (Feb 11 2021 at 09:39):

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

Last updated: May 17 2021 at 15:13 UTC