Zulip Chat Archive

Stream: Is there code for X?

Topic: Homomorphism estensionnality


view this post on Zulip 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.)

view this post on Zulip Kenny Lau (Feb 11 2021 at 09:02):

why not make the goal φ₁ = φ₂

view this post on Zulip 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...

view this post on Zulip Eric Wieser (Feb 11 2021 at 09:14):

The homomorphism arguments should be implicit too

view this post on Zulip 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

view this post on Zulip Julien Marquet (Feb 11 2021 at 09:30):

I didn't notice the unprimed version, thanks !

view this post on Zulip 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