Mathlib.Algebra.Group.Units.Hom

Units.map definition

(f : M →* N) : Mˣ →* Nˣ

Full source

/-- The group homomorphism on units induced by a `MonoidHom`. -/
@[to_additive "The additive homomorphism on `AddUnit`s induced by an `AddMonoidHom`."]
def map (f : M →* N) : MˣMˣ →* Nˣ :=
  MonoidHom.mk'
    (fun u => ⟨f u.val, f u.inv,
      by rw [← f.map_mul, u.val_inv, f.map_one],
      by rw [← f.map_mul, u.inv_val, f.map_one]⟩)
    fun x y => ext (f.map_mul x y)

Induced homomorphism on units of monoids

Informal description

Given a monoid homomorphism $ f \colon M \to N $, the function `Units.map f` is the induced group homomorphism from the group of units $ M^\times $ of $ M $ to the group of units $ N^\times $ of $ N $. For any unit $ u \in M^\times $, the image under `Units.map f` is the unit $ (f(u), f(u^{-1})) $ in $ N^\times $, where $ u^{-1} $ is the inverse of $ u $ in $ M^\times $.

Units.coe_map theorem

(f : M →* N) (x : Mˣ) : ↑(map f x) = f x

Full source

@[to_additive (attr := simp)]
theorem coe_map (f : M →* N) (x : Mˣ) : ↑(map f x) = f x := rfl

Image of Unit under Induced Homomorphism Equals Direct Image

Informal description

For any monoid homomorphism $f \colon M \to N$ and any unit $x \in M^\times$, the underlying element of the image of $x$ under the induced homomorphism $\mathrm{map}\,f$ equals the image of $x$ under $f$, i.e., $\mathrm{map}\,f(x) = f(x)$.

Units.coe_map_inv theorem

(f : M →* N) (u : Mˣ) : ↑(map f u)⁻¹ = f ↑u⁻¹

Full source

@[to_additive (attr := simp)]
theorem coe_map_inv (f : M →* N) (u : Mˣ) : ↑(map f u)⁻¹ = f ↑u⁻¹ := rfl

Inverse Preservation under Induced Homomorphism on Units

Informal description

For any monoid homomorphism $f \colon M \to N$ and any unit $u \in M^\times$, the inverse of the image of $u$ under the induced homomorphism on units equals the image under $f$ of the inverse of $u$, i.e., $(f(u))^{-1} = f(u^{-1})$.

Units.map_mk theorem

 (f : M →* N) (val inv : M) (val_inv inv_val) :
  map f (mk val inv val_inv inv_val) =
    mk (f val) (f inv) (by rw [← f.map_mul, val_inv, f.map_one]) (by rw [← f.map_mul, inv_val, f.map_one])

Full source

@[to_additive (attr := simp)]
lemma map_mk (f : M →* N) (val inv : M) (val_inv inv_val) :
    map f (mk val inv val_inv inv_val) = mk (f val) (f inv)
      (by rw [← f.map_mul, val_inv, f.map_one]) (by rw [← f.map_mul, inv_val, f.map_one]) := rfl

Induced Unit Homomorphism Preserves Unit Construction

Informal description

Let $M$ and $N$ be monoids and let $f \colon M \to N$ be a monoid homomorphism. For any elements $val, inv \in M$ satisfying the unit conditions $val \cdot inv = 1$ and $inv \cdot val = 1$, the induced homomorphism on units satisfies: \[ \text{map } f (\text{mk } val\ inv\ val\_inv\ inv\_val) = \text{mk } (f\ val)\ (f\ inv)\ (f\ val \cdot f\ inv = 1)\ (f\ inv \cdot f\ val = 1) \] where the right-hand side uses the fact that $f$ preserves multiplication and identity.

Units.map_comp theorem

(f : M →* N) (g : N →* P) : map (g.comp f) = (map g).comp (map f)

Full source

@[to_additive (attr := simp)]
theorem map_comp (f : M →* N) (g : N →* P) : map (g.comp f) = (map g).comp (map f) := rfl

Composition Property of Induced Homomorphisms on Units

Informal description

Given monoids $ M $, $ N $, and $ P $, and monoid homomorphisms $ f \colon M \to N $ and $ g \colon N \to P $, the induced homomorphism on units satisfies the composition property: \[ \text{map}(g \circ f) = \text{map}(g) \circ \text{map}(f) \] Here, $\text{map}(f) \colon M^\times \to N^\times$ denotes the induced group homomorphism on the units of $M$ and $N$ respectively, and $\circ$ denotes function composition.

Units.map_injective theorem

{f : M →* N} (hf : Function.Injective f) : Function.Injective (map f)

Full source

@[to_additive]
lemma map_injective {f : M →* N} (hf : Function.Injective f) :
    Function.Injective (map f) := fun _ _ e => ext (hf (congr_arg val e))

Injectivity of Induced Homomorphism on Units

Informal description

Let $f \colon M \to N$ be an injective monoid homomorphism. Then the induced homomorphism on units $\text{map}\, f \colon M^\times \to N^\times$ is also injective.

Units.map_id theorem

: map (MonoidHom.id M) = MonoidHom.id Mˣ

Full source

@[to_additive (attr := simp)]
theorem map_id : map (MonoidHom.id M) = MonoidHom.id Mˣ := by ext; rfl

Identity Homomorphism Induces Identity on Units

Informal description

The induced homomorphism on units of a monoid $M$ by the identity monoid homomorphism $\text{id}_M \colon M \to M$ is equal to the identity homomorphism on the group of units $M^\times$, i.e., $\text{map}(\text{id}_M) = \text{id}_{M^\times}$.

Units.coeHom definition

: Mˣ →* M

Full source

/-- Coercion `Mˣ → M` as a monoid homomorphism. -/
@[to_additive "Coercion `AddUnits M → M` as an AddMonoid homomorphism."]
def coeHom : MˣMˣ →* M where
  toFun := Units.val; map_one' := val_one; map_mul' := val_mul

Canonical inclusion of units into the monoid

Informal description

The monoid homomorphism that sends a unit $ u $ of a monoid $ M $ to its underlying element in $ M $. This map preserves the multiplicative identity and multiplication, i.e., it satisfies $ \text{coeHom}(1) = 1 $ and $ \text{coeHom}(u \cdot v) = \text{coeHom}(u) \cdot \text{coeHom}(v) $ for any units $ u, v \in M^\times $.

Units.coeHom_apply theorem

(x : Mˣ) : coeHom M x = ↑x

Full source

@[to_additive (attr := simp)]
theorem coeHom_apply (x : Mˣ) : coeHom M x = ↑x := rfl

Canonical Inclusion of Units Evaluates to Underlying Element

Informal description

For any unit $x$ in the group of units $M^\times$ of a monoid $M$, the evaluation of the canonical inclusion homomorphism $\text{coeHom}$ at $x$ equals the underlying element of $x$ in $M$, i.e., $\text{coeHom}(x) = x$.

Units.val_zpow_eq_zpow_val theorem

: ∀ (u : αˣ) (n : ℤ), ((u ^ n : αˣ) : α) = (u : α) ^ n

Full source

@[to_additive (attr := simp, norm_cast)]
theorem val_zpow_eq_zpow_val : ∀ (u : αˣ) (n : ℤ), ((u ^ n : αˣ) : α) = (u : α) ^ n :=
  (Units.coeHom α).map_zpow

Power of Unit's Underlying Element Equals Underlying Element of Power

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$ and any integer $n$, the underlying element of the $n$-th power of $u$ in $\alpha^\times$ equals the $n$-th power of the underlying element of $u$ in $\alpha$, i.e., $(u^n : \alpha) = (u : \alpha)^n$.

map_units_inv theorem

{F : Type*} [FunLike F M α] [MonoidHomClass F M α] (f : F) (u : Units M) : f ↑u⁻¹ = (f u)⁻¹

Full source

@[to_additive (attr := simp)]
theorem _root_.map_units_inv {F : Type*} [FunLike F M α] [MonoidHomClass F M α]
    (f : F) (u : Units M) :
    f ↑u⁻¹ = (f u)⁻¹ := ((f : M →* α).comp (Units.coeHom M)).map_inv u

Monoid homomorphisms preserve inverses of units: $f(u^{-1}) = (f(u))^{-1}$

Informal description

Let $M$ and $\alpha$ be monoids, and let $F$ be a type of functions from $M$ to $\alpha$ that is both function-like and a monoid homomorphism class. For any monoid homomorphism $f \colon M \to \alpha$ in $F$ and any unit $u \in M^\times$, the image of the inverse unit $f(u^{-1})$ is equal to the inverse of the image $(f(u))^{-1}$ in $\alpha$.

Units.liftRight definition

(f : M →* N) (g : M → Nˣ) (h : ∀ x, ↑(g x) = f x) : M →* Nˣ

Full source

/-- If a map `g : M → Nˣ` agrees with a homomorphism `f : M →* N`, then
this map is a monoid homomorphism too. -/
@[to_additive
  "If a map `g : M → AddUnits N` agrees with a homomorphism `f : M →+ N`, then this map
  is an AddMonoid homomorphism too."]
def liftRight (f : M →* N) (g : M → Nˣ) (h : ∀ x, ↑(g x) = f x) : M →* Nˣ where
  toFun := g
  map_one' := by ext; rw [h 1]; exact f.map_one
  map_mul' x y := Units.ext <| by simp only [h, val_mul, f.map_mul]

Lifting a monoid homomorphism to units

Informal description

Given a monoid homomorphism $ f \colon M \to N $ and a function $ g \colon M \to N^\times $ (where $ N^\times $ denotes the group of units of $ N $) such that for every $ x \in M $, the underlying element of $ g(x) $ equals $ f(x) $, then $ g $ is also a monoid homomorphism from $ M $ to $ N^\times $.

Units.coe_liftRight theorem

{f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) : (liftRight f g h x : N) = f x

Full source

@[to_additive (attr := simp)]
theorem coe_liftRight {f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) :
    (liftRight f g h x : N) = f x := h x

Underlying Element of Lifted Homomorphism Equals Original Homomorphism

Informal description

Given a monoid homomorphism $f \colon M \to N$ and a function $g \colon M \to N^\times$ (where $N^\times$ denotes the group of units of $N$) such that for every $x \in M$, the underlying element of $g(x)$ equals $f(x)$, then the underlying element of the lifted homomorphism $\text{liftRight}(f, g, h)(x)$ equals $f(x)$ for all $x \in M$.

Units.mul_liftRight_inv theorem

{f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) : f x * ↑(liftRight f g h x)⁻¹ = 1

Full source

@[to_additive (attr := simp)]
theorem mul_liftRight_inv {f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) :
    f x * ↑(liftRight f g h x)⁻¹ = 1 := by
  rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]

Right inverse property of lifted homomorphism: $f(x) \cdot g(x)^{-1} = 1$

Informal description

Let $f \colon M \to N$ be a monoid homomorphism and $g \colon M \to N^\times$ a function such that for all $x \in M$, the underlying element of $g(x)$ equals $f(x)$. Then for any $x \in M$, we have $f(x) \cdot (\text{liftRight}(f, g, h)(x))^{-1} = 1$, where $\text{liftRight}(f, g, h) \colon M \to N^\times$ is the lifted homomorphism.

Units.liftRight_inv_mul theorem

{f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) : ↑(liftRight f g h x)⁻¹ * f x = 1

Full source

@[to_additive (attr := simp)]
theorem liftRight_inv_mul {f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) :
    ↑(liftRight f g h x)⁻¹ * f x = 1 := by
  rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]

Left inverse property of lifted homomorphism: $g(x)^{-1} \cdot f(x) = 1$

Informal description

Let $f \colon M \to N$ be a monoid homomorphism and $g \colon M \to N^\times$ a function such that for all $x \in M$, the underlying element of $g(x)$ equals $f(x)$. Then for any $x \in M$, we have $(\text{liftRight}(f, g, h)(x))^{-1} \cdot f(x) = 1$, where $\text{liftRight}(f, g, h) \colon M \to N^\times$ is the lifted homomorphism.

MonoidHom.toHomUnits definition

{G M : Type*} [Group G] [Monoid M] (f : G →* M) : G →* Mˣ

Full source

/-- If `f` is a homomorphism from a group `G` to a monoid `M`,
then its image lies in the units of `M`,
and `f.toHomUnits` is the corresponding monoid homomorphism from `G` to `Mˣ`. -/
@[to_additive
  "If `f` is a homomorphism from an additive group `G` to an additive monoid `M`,
  then its image lies in the `AddUnits` of `M`,
  and `f.toHomUnits` is the corresponding homomorphism from `G` to `AddUnits M`."]
def toHomUnits {G M : Type*} [Group G] [Monoid M] (f : G →* M) : G →* Mˣ :=
  Units.liftRight f (fun g => ⟨f g, f g⁻¹, map_mul_eq_one f (mul_inv_cancel _),
    map_mul_eq_one f (inv_mul_cancel _)⟩)
    fun _ => rfl

Lifting a monoid homomorphism to the group of units

Informal description

Given a group $G$ and a monoid $M$, any monoid homomorphism $f \colon G \to M$ has its image contained in the group of units $M^\times$ of $M$. The function `toHomUnits` constructs the corresponding monoid homomorphism from $G$ to $M^\times$.

MonoidHom.coe_toHomUnits theorem

{G M : Type*} [Group G] [Monoid M] (f : G →* M) (g : G) : (f.toHomUnits g : M) = f g

Full source

@[to_additive (attr := simp)]
theorem coe_toHomUnits {G M : Type*} [Group G] [Monoid M] (f : G →* M) (g : G) :
    (f.toHomUnits g : M) = f g := rfl

Underlying Element of Lifted Homomorphism to Units

Informal description

Let $G$ be a group and $M$ a monoid. For any monoid homomorphism $f \colon G \to M$ and any element $g \in G$, the underlying element of the unit $f.\text{toHomUnits}(g) \in M^\times$ is equal to $f(g)$. In other words, the composition of $f.\text{toHomUnits}$ with the canonical inclusion $M^\times \hookrightarrow M$ recovers $f$.

IsUnit.map theorem

[MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) : IsUnit (f x)

Full source

@[to_additive]
theorem map [MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) : IsUnit (f x) := by
  rcases h with ⟨y, rfl⟩; exact (Units.map (f : M →* N) y).isUnit

Preservation of Units under Monoid Homomorphisms

Informal description

Let $M$ and $N$ be monoids, and let $F$ be a type of homomorphisms from $M$ to $N$ that preserve the monoid structure. For any homomorphism $f \in F$ and any element $x \in M$ that is a unit (i.e., has a multiplicative inverse), the image $f(x)$ is also a unit in $N$.

IsUnit.of_leftInverse theorem

[MonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) (h : IsUnit (f x)) : IsUnit x

Full source

@[to_additive]
theorem of_leftInverse [MonoidHomClass G N M] {f : F} {x : M} (g : G)
    (hfg : Function.LeftInverse g f) (h : IsUnit (f x)) : IsUnit x := by
  simpa only [hfg x] using h.map g

Left Inverse Homomorphism Preserves Unit Property

Informal description

Let $M$ and $N$ be monoids, and let $F$ and $G$ be types of homomorphisms from $M$ to $N$ and from $N$ to $M$, respectively, that preserve the monoid structure. Given a homomorphism $f \in F$, an element $x \in M$, and a homomorphism $g \in G$ such that $g$ is a left inverse of $f$ (i.e., $g(f(y)) = y$ for all $y \in M$), if $f(x)$ is a unit in $N$, then $x$ is a unit in $M$.

isUnit_map_of_leftInverse theorem

 [MonoidHomClass F M N] [MonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) :
  IsUnit (f x) ↔ IsUnit x

Full source

/-- Prefer `IsLocalHom.of_leftInverse`, but we can't get rid of this because of `ToAdditive`. -/
@[to_additive]
theorem _root_.isUnit_map_of_leftInverse [MonoidHomClass F M N] [MonoidHomClass G N M]
    {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) :
    IsUnitIsUnit (f x) ↔ IsUnit x := ⟨of_leftInverse g hfg, map _⟩

Unit Preservation under Left-Invertible Monoid Homomorphisms

Informal description

Let $M$ and $N$ be monoids, and let $F$ and $G$ be types of homomorphisms from $M$ to $N$ and from $N$ to $M$, respectively, that preserve the monoid structure. Given a homomorphism $f \in F$, an element $x \in M$, and a homomorphism $g \in G$ such that $g$ is a left inverse of $f$ (i.e., $g(f(y)) = y$ for all $y \in M$), then $f(x)$ is a unit in $N$ if and only if $x$ is a unit in $M$.

IsUnit.liftRight definition

(f : M →* N) (hf : ∀ x, IsUnit (f x)) : M →* Nˣ

Full source

/-- If a homomorphism `f : M →* N` sends each element to an `IsUnit`, then it can be lifted
to `f : M →* Nˣ`. See also `Units.liftRight` for a computable version. -/
@[to_additive
  "If a homomorphism `f : M →+ N` sends each element to an `IsAddUnit`, then it can be
  lifted to `f : M →+ AddUnits N`. See also `AddUnits.liftRight` for a computable version."]
noncomputable def liftRight (f : M →* N) (hf : ∀ x, IsUnit (f x)) : M →* Nˣ :=
  (Units.liftRight f fun x => (hf x).unit) fun _ => rfl

Lifting a monoid homomorphism to units

Informal description

Given a monoid homomorphism $ f \colon M \to N $ such that $ f(x) $ is a unit in $ N $ for every $ x \in M $, this defines a monoid homomorphism from $ M $ to the group of units $ N^\times $.

IsUnit.coe_liftRight theorem

(f : M →* N) (hf : ∀ x, IsUnit (f x)) (x) : (IsUnit.liftRight f hf x : N) = f x

Full source

@[to_additive]
theorem coe_liftRight (f : M →* N) (hf : ∀ x, IsUnit (f x)) (x) :
    (IsUnit.liftRight f hf x : N) = f x := rfl

Coercion of Lifted Homomorphism Recovers Original Map

Informal description

For any monoid homomorphism $f \colon M \to N$ such that $f(x)$ is a unit in $N$ for every $x \in M$, and for any $x \in M$, the underlying element of the unit $\text{IsUnit.liftRight}\,f\,hf\,x$ in $N$ equals $f(x)$. In other words, the composition of the lift with the coercion to $N$ recovers the original homomorphism.

IsUnit.mul_liftRight_inv theorem

(f : M →* N) (h : ∀ x, IsUnit (f x)) (x) : f x * ↑(IsUnit.liftRight f h x)⁻¹ = 1

Full source

@[to_additive (attr := simp)]
theorem mul_liftRight_inv (f : M →* N) (h : ∀ x, IsUnit (f x)) (x) :
    f x * ↑(IsUnit.liftRight f h x)⁻¹ = 1 := Units.mul_liftRight_inv (by intro; rfl) x

Right inverse property of lifted homomorphism: $f(x) \cdot g(x)^{-1} = 1$

Informal description

Let $f \colon M \to N$ be a monoid homomorphism such that $f(x)$ is a unit in $N$ for every $x \in M$. Then for any $x \in M$, we have $f(x) \cdot (\text{liftRight}(f, h)(x))^{-1} = 1$, where $\text{liftRight}(f, h) \colon M \to N^\times$ is the lifted homomorphism to the group of units.

IsUnit.liftRight_inv_mul theorem

(f : M →* N) (h : ∀ x, IsUnit (f x)) (x) : ↑(IsUnit.liftRight f h x)⁻¹ * f x = 1

Full source

@[to_additive (attr := simp)]
theorem liftRight_inv_mul (f : M →* N) (h : ∀ x, IsUnit (f x)) (x) :
    ↑(IsUnit.liftRight f h x)⁻¹ * f x = 1 := Units.liftRight_inv_mul (by intro; rfl) x

Left inverse property of lifted homomorphism: $g(x)^{-1} \cdot f(x) = 1$

Informal description

Let $f \colon M \to N$ be a monoid homomorphism such that $f(x)$ is a unit in $N$ for every $x \in M$. Then for any $x \in M$, the inverse of the lifted homomorphism $\text{IsUnit.liftRight}\,f\,h\,x$ in $N^\times$ multiplied by $f(x)$ equals the identity element $1$ in $N$, i.e., \[ (\text{IsUnit.liftRight}\,f\,h\,x)^{-1} \cdot f(x) = 1. \]

IsLocalHom structure

(f : F)

Full source

/-- A local ring homomorphism is a map `f` between monoids such that `a` in the domain
  is a unit if `f a` is a unit for any `a`. 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. -/
class IsLocalHom (f : F) : Prop where
  /-- A local homomorphism `f : R ⟶ S` will send nonunits of `R` to nonunits of `S`. -/
  map_nonunit : ∀ a, IsUnit (f a) → IsUnit a

Local Monoid Homomorphism

Informal description

A monoid homomorphism $ f $ between monoids is called *local* if for any element $ a $ in the domain, $ a $ is a unit whenever $ f(a) $ is a unit. This concept generalizes the notion of local ring homomorphisms to arbitrary monoids.

IsUnit.of_map theorem

(f : F) [IsLocalHom f] (a : R) (h : IsUnit (f a)) : IsUnit a

Full source

@[simp]
theorem IsUnit.of_map (f : F) [IsLocalHom f] (a : R) (h : IsUnit (f a)) : IsUnit a :=
  IsLocalHom.map_nonunit a h

Local Homomorphisms Preserve Units

Informal description

Let $f \colon R \to S$ be a local monoid homomorphism between monoids $R$ and $S$. For any element $a \in R$, if $f(a)$ is a unit in $S$, then $a$ is a unit in $R$.

isUnit_map_iff theorem

(f : F) [IsLocalHom f] (a : R) : IsUnit (f a) ↔ IsUnit a

Full source

@[simp]
theorem isUnit_map_iff (f : F) [IsLocalHom f] (a : R) : IsUnitIsUnit (f a) ↔ IsUnit a :=
  ⟨IsLocalHom.map_nonunit a, IsUnit.map f⟩

Characterization of Units under Local Monoid Homomorphisms

Informal description

Let $R$ and $S$ be monoids, and let $f \colon R \to S$ be a local monoid homomorphism. For any element $a \in R$, the image $f(a)$ is a unit in $S$ if and only if $a$ is a unit in $R$.

isLocalHom_of_leftInverse theorem

[FunLike G S R] [MonoidHomClass G S R] {f : F} (g : G) (hfg : Function.LeftInverse g f) : IsLocalHom f

Full source

theorem isLocalHom_of_leftInverse [FunLike G S R] [MonoidHomClass G S R]
    {f : F} (g : G) (hfg : Function.LeftInverse g f) : IsLocalHom f where
  map_nonunit a ha := by rwa [isUnit_map_of_leftInverse g hfg] at ha

Left-invertible homomorphisms are local

Informal description

Let $R$ and $S$ be monoids, and let $F$ and $G$ be types of homomorphisms from $R$ to $S$ and from $S$ to $R$, respectively, that preserve the monoid structure. Given a homomorphism $f \in F$ and a homomorphism $g \in G$ such that $g$ is a left inverse of $f$ (i.e., $g(f(x)) = x$ for all $x \in R$), then $f$ is a local homomorphism (i.e., $f$ maps nonunits to nonunits).

MonoidHom.isLocalHom_comp theorem

(g : S →* T) (f : R →* S) [IsLocalHom g] [IsLocalHom f] : IsLocalHom (g.comp f)

Full source

@[instance]
theorem MonoidHom.isLocalHom_comp (g : S →* T) (f : R →* S) [IsLocalHom g]
    [IsLocalHom f] : IsLocalHom (g.comp f) where
  map_nonunit a := IsLocalHom.map_nonunitIsLocalHom.map_nonunit a ∘ IsLocalHom.map_nonunit (f := g) (f a)

Composition of Local Monoid Homomorphisms is Local

Informal description

Let $R$, $S$, and $T$ be monoids, and let $f \colon R \to^* S$ and $g \colon S \to^* T$ be monoid homomorphisms. If both $f$ and $g$ are local homomorphisms (i.e., they map nonunits to nonunits), then their composition $g \circ f \colon R \to^* T$ is also a local homomorphism.

isLocalHom_toMonoidHom theorem

(f : F) [IsLocalHom f] : IsLocalHom (f : R →* S)

Full source

@[instance 100]
theorem isLocalHom_toMonoidHom (f : F) [IsLocalHom f] :
    IsLocalHom (f : R →* S) :=
  ⟨IsLocalHom.map_nonunit (f := f)⟩

Local Homomorphism Property Preserved Under Monoid Homomorphism Conversion

Informal description

Let $R$ and $S$ be monoids, and let $f \colon R \to S$ be a monoid homomorphism. If $f$ is a local homomorphism (i.e., it maps nonunits to nonunits), then the induced monoid homomorphism $f \colon R \to^* S$ is also local.

MonoidHom.isLocalHom_of_comp theorem

(f : R →* S) (g : S →* T) [IsLocalHom (g.comp f)] : IsLocalHom f

Full source

theorem MonoidHom.isLocalHom_of_comp (f : R →* S) (g : S →* T) [IsLocalHom (g.comp f)] :
    IsLocalHom f :=
  ⟨fun _ ha => (isUnit_map_iff (g.comp f) _).mp (ha.map g)⟩

Local Homomorphism Property Inherited from Composition

Informal description

Let $R$, $S$, and $T$ be monoids, and let $f \colon R \to^* S$ and $g \colon S \to^* T$ be monoid homomorphisms. If the composition $g \circ f \colon R \to^* T$ is a local homomorphism, then $f$ is also a local homomorphism.

Mathlib.Algebra.Group.Units.Hom

Main declarations

TODO