Theorems · Inductive type · group theory

IsLocalHom

{R : Type u_2} → {S : Type u_3} → {F : Type u_5} → [Monoid R] → [Monoid S] → [FunLike F R S] → F → Prop

A map f between monoids is local if any a in the domain is a unit whenever f a is a unit. See IsLocalRing.local_hom_TFAE for other equivalent definitions in the local ring case - from where this concept originates, but it is useful in other contexts, so we allow this generalisation in mathlib.

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

100 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 5 definitions · uses no axioms

Assumes

MonoidMonoidFunLike