injective_iff_map_eq_one
theorem injective_iff_map_eq_one :
∀ {F : Type u_8} {G : Type u_9} {H : Type u_10} [inst : Group G] [inst_1 : MulOneClass H] [inst_2 : FunLike F G H]
[inst_3 : MonoidHomClass F G H] (f : F), Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 → a = 1
The theorem `injective_iff_map_eq_one` states that for any types `F`, `G`, `H` where `G` is a group, `H` is a MulOneClass (a class that supports multiplication and has a multiplicative identity), `F` is a function-like object from `G` to `H`, and `F` is a homomorphism from the group `G` to the monoid `H`, then a function `f` of type `F` is injective if and only if for all elements `a` in `G`, if `f(a)` equals to the multiplicative identity `1`, then `a` must also be the multiplicative identity `1`. In other words, a homomorphism from a group to a monoid is injective if and only if its kernel is the singleton set containing only the group's identity element.
More concisely: A homomorphism from a group to a monoid is injective if and only if its kernel consists only of the group's identity element.
|
injective_iff_map_eq_one'
theorem injective_iff_map_eq_one' :
∀ {F : Type u_8} {G : Type u_9} {H : Type u_10} [inst : Group G] [inst_1 : MulOneClass H] [inst_2 : FunLike F G H]
[inst_3 : MonoidHomClass F G H] (f : F), Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 ↔ a = 1
This theorem states that for any types `F`, `G`, and `H` where `G` is a group, `H` is a monoid, `F` has a function-like structure from `G` to `H`, and `F` forms a monoid homomorphism from `G` to `H`, a function `f` of type `F` is injective if and only if its kernel is trivial. Here, a trivial kernel means that for any element `a` of the group `G`, the result of applying the function `f` to `a` is the multiplicative identity element of `H` (denoted as `1`) if and only if `a` is the identity element of `G`. The injectivity of a function is defined as its ability to map distinct elements to distinct elements, that is, if `f a = f b` then `a = b`.
More concisely: A function `f` from a group `G` to a monoid `H`, which is a homomorphism and has a trivial kernel, is injective. (A trivial kernel means that `f(a) = 1_H` if and only if `a = 1_G` for all elements `a` in `G`, where `1_H` and `1_G` are the identity elements of `H` and `G` respectively.)
|
injective_iff_map_eq_zero'
theorem injective_iff_map_eq_zero' :
∀ {F : Type u_8} {G : Type u_9} {H : Type u_10} [inst : AddGroup G] [inst_1 : AddZeroClass H]
[inst_2 : FunLike F G H] [inst_3 : AddMonoidHomClass F G H] (f : F),
Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 ↔ a = 0
The theorem `injective_iff_map_eq_zero'` states that for all types `F`, `G`, and `H`, where `G` is an additive group, `H` is an additive monoid with a zero, `F` is a function from `G` to `H`, and `F` is an additive monoid homomorphism between `G` and `H`, a function `f` of type `F` is injective if and only if the result of applying `f` to any element `a` of `G` is zero if and only if `a` itself is zero. This theorem connects the concept of function injectivity with the triviality of the kernel in the context of homomorphisms from additive groups to additive monoids.
More concisely: A function from an additive group to an additive monoid with a zero is injective if and only if it maps the additive identity to the zero element of the codomain.
|
injective_iff_map_eq_zero
theorem injective_iff_map_eq_zero :
∀ {F : Type u_8} {G : Type u_9} {H : Type u_10} [inst : AddGroup G] [inst_1 : AddZeroClass H]
[inst_2 : FunLike F G H] [inst_3 : AddMonoidHomClass F G H] (f : F),
Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 → a = 0
The theorem `injective_iff_map_eq_zero` states that for any types `F`, `G`, and `H`, where `G` is an additive group, `H` is an additive monoid with zero, `F` is a function-like structure from `G` to `H`, and `F` is a homomorphism from the additive group `G` to the additive monoid `H`, a function `f` of type `F` is injective if and only if for all elements `a` of `G`, `f` maps `a` to zero if and only if `a` is zero. This theorem is relating the injectivity of a function to the triviality of its kernel. In other words, a homomorphism between these structures is injective if the only element it maps to zero is zero itself.
More concisely: A homomorphism from an additive group to an additive monoid with zero is injective if and only if it maps every element to zero if and only if that element is the additive identity.
|