Unitality of a multiplicative map

A multiplicative map need not preserve 1, and the zero map shows it need not. Where multiplication in the codomain is left-cancellative away from zero there is nothing in between: such a map is identically zero or unital, the zero map being the only non-unital one. A unital one is promoted to a bundled unital map by AlgHom.ofLinearMap or RingHom.mk'.

This is the dichotomy that lets a type of multiplicative maps carry a zero without adjoining one.

Main results

• MulHomClass.forall_apply_eq_zero_or_map_one: such a map vanishes identically or sends 1 to 1.

Implementation notes

The statement is class-general, over MulHomClass, so it holds of every bundled multiplicative map type — MonoidHom, RingHom, NonUnitalAlgHom — without a specialisation for each. Its vanishing alternative is pointwise, ∀ x, p x = 0, rather than p = 0, because the class carries no Zero on the map type.

theorem MulHomClass.forall_apply_eq_zero_or_map_one {A : Type u_1} {B : Type u_2} {G : Type u_3} [MulOneClass A] [MulZeroOneClass B] [IsLeftCancelMulZero B] [FunLike G A B] [MulHomClass G A B] (p : G) : (∀ (x : A), p x = 0) ∨ p 1 = 1

A multiplicative map vanishes identically or is unital.

theorem MulHomClass.map_one_of_exists_apply_ne_zero {A : Type u_1} {B : Type u_2} {G : Type u_3} [MulOneClass A] [MulZeroOneClass B] [IsLeftCancelMulZero B] [FunLike G A B] [MulHomClass G A B] {p : G} (hp : ∃ (x : A), p x ≠ 0) : p 1 = 1

A multiplicative map that is somewhere nonzero is unital.