## Stream: general

### Topic: injective hom iffs

#### Yakov Pechersky (Jan 05 2022 at 20:06):

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

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 (Jan 05 2022 at 20:39):

You should now use one_hom_class, monoid_with_zero_hom_class, ...

#### Yaël Dillies (Jan 05 2022 at 20:40):

Just one_hom_class actually :laughing:

#### Eric Rodriguez (Jan 05 2022 at 20:40):

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

#### Eric Rodriguez (Jan 05 2022 at 20:40):

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

#### Eric Rodriguez (Jan 05 2022 at 20:45):

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

#### Yakov Pechersky (Jan 05 2022 at 20:50):

OK, working on it

#### Yakov Pechersky (Jan 05 2022 at 20:54):

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

#### Yury G. Kudryashov (Jan 05 2022 at 23:48):

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

#### Yury G. Kudryashov (Jan 05 2022 at 23:49):

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

#### Yakov Pechersky (Jan 06 2022 at 01:07):

#11275

Last updated: Aug 03 2023 at 10:10 UTC