Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC