injective hom iffs

Stream: general

[Yakov Pechersky]

Do we have the following? What should they be with our new class structure? Are ring_homs outside the class structure?

import algebra.ring.basic

@[to_additive]
lemma one_hom.map_eq_one_iff {R S : Type*} [has_one R] [has_one S] (f : one_hom R S)
  (hf : function.injective f) {x : R} :
  f x = 1 ↔ x = 1 :=
⟨λ h, hf $ by simp [h], λ h, by simpa using congr_arg f h⟩

lemma monoid_with_zero_hom.map_eq_one_iff {R S : Type*} [monoid_with_zero R] [monoid_with_zero S]
  (f : monoid_with_zero_hom R S) (hf : function.injective f) {x : R} :
  f x = 1 ↔ x = 1 :=
f.to_monoid_hom.to_one_hom.map_eq_one_iff hf

lemma monoid_with_zero_hom.map_eq_zero_iff {R S : Type*} [monoid_with_zero R] [monoid_with_zero S]
  (f : monoid_with_zero_hom R S) (hf : function.injective f) {x : R} :
  f x = 0 ↔ x = 0 :=
f.to_zero_hom.map_eq_zero_iff hf

lemma ring_hom.map_eq_one_iff {R S : Type*} [non_assoc_semiring R] [non_assoc_semiring S]
  (f : R →+* S) (hf : function.injective f) {x : R} :
  f x = 1 ↔ x = 1 :=
f.to_monoid_hom.to_one_hom.map_eq_one_iff hf

lemma ring_hom.map_eq_zero_iff {R S : Type*} [non_assoc_semiring R] [non_assoc_semiring S]
  (f : R →+* S) (hf : function.injective f) {x : R} :
  f x = 0 ↔ x = 0 :=
f.to_monoid_with_zero_hom.to_zero_hom.map_eq_zero_iff hf

[Yaël Dillies]

You should now use one_hom_class, monoid_with_zero_hom_class, ...

[Yaël Dillies]

Just one_hom_class actually :laughing:

[Eric Rodriguez]

for ring_homs, we have docs#ring_hom.injective_iff. not sure about other versions

[Eric Rodriguez]

but yes, I agree this should be fun-liked, especially now that we nearly got the fixes in!

[Eric Rodriguez]

oh, there's also both monoid-hom versions, ofc (dah): docs#add_monoid_hom.injective_iff

[Yakov Pechersky]

OK, working on it

[Yakov Pechersky]

Those existing ones are a bit weak, because the iff.mpr to produce an injective f requires inverses on the domain

[Yury G. Kudryashov]

We have docs#function.injective.eq_iff'

[Yury G. Kudryashov]

Your lemma is just hf.eq_iff' (map_one f)

[Yury G. Kudryashov]

Feel free to add to algebra/group/hom for a map_one_class

[Yakov Pechersky]

#11275