doc-next-gen

Mathlib.Algebra.GroupWithZero.Units.Lemmas

Module docstring

{"# Further lemmas about units in a MonoidWithZero or a GroupWithZero.

"}

isLocalHom_of_exists_map_ne_one theorem
[FunLike F G₀ M] [MonoidHomClass F G₀ M] {f : F} (hf : ∃ x : G₀, f x ≠ 1) : IsLocalHom f
Full source 
lemma isLocalHom_of_exists_map_ne_one [FunLike F G₀ M] [MonoidHomClass F G₀ M] {f : F}
    (hf : ∃ x : G₀, f x ≠ 1) : IsLocalHom f where
  map_nonunit a h := by
    rcases eq_or_ne a 0 with (rfl | h)
    · obtain ⟨t, ht⟩ := hf
      refine (ht ?_).elim
      have := map_mul f t 0
      rw [← one_mul (f (t * 0)), mul_zero] at this
      exact (h.mul_right_cancel this).symm
    · exact ⟨⟨a, a⁻¹, mul_inv_cancel₀ h, inv_mul_cancel₀ h⟩, rfl⟩
Existence of Non-Identity Image Implies Local Homomorphism Property for Group-with-Zero to Monoid Maps
Informal description
Let $G₀$ be a group with zero and $M$ be a monoid. Given a monoid homomorphism $f \colon G₀ \to M$ (i.e., a function preserving multiplication and identity) such that there exists some $x \in G₀$ with $f(x) \neq 1$, then $f$ is a local homomorphism. This means that for any $a \in G₀$, if $f(a)$ is a unit in $M$, then $a$ is a unit in $G₀$.
instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial instance
[GroupWithZero G₀] [FunLike F G₀ M₀] [MonoidWithZeroHomClass F G₀ M₀] [Nontrivial M₀] (f : F) : IsLocalHom f
Full source 
instance [GroupWithZero G₀] [FunLike F G₀ M₀] [MonoidWithZeroHomClass F G₀ M₀] [Nontrivial M₀]
    (f : F) : IsLocalHom f :=
  isLocalHom_of_exists_map_ne_one ⟨0, by simp⟩
Monoid with Zero Homomorphisms from Groups with Zero are Local Homomorphisms
Informal description
Let $G₀$ be a group with zero and $M₀$ be a nontrivial monoid with zero. Every monoid with zero homomorphism $f \colon G₀ \to M₀$ is a local homomorphism, meaning that for any $a \in G₀$, if $f(a)$ is a unit in $M₀$, then $a$ is a unit in $G₀$.
Commute.div_eq_div_iff theorem
(hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = c * b
Full source 
/-- The `MonoidWithZero` version of `div_eq_div_iff_mul_eq_mul`. -/
protected lemma div_eq_div_iff (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :
    a / b = c / d ↔ a * d = c * b := hbd.div_eq_div_iff_of_isUnit hb.isUnit hd.isUnit
Equality of Fractions with Commuting Nonzero Elements: $\frac{a}{b} = \frac{c}{d} \leftrightarrow a \cdot d = c \cdot b$
Informal description
Let $a, b, c, d$ be elements in a group with zero such that $b$ and $d$ commute (i.e., $b \cdot d = d \cdot b$), and suppose $b \neq 0$ and $d \neq 0$. Then the equality of fractions $\frac{a}{b} = \frac{c}{d}$ holds if and only if $a \cdot d = c \cdot b$.
map_eq_zero theorem
: f a = 0 ↔ a = 0
Full source 
@[simp]
theorem map_eq_zero : f a = 0 ↔ a = 0 :=
  not_iff_not.1 (map_ne_zero f)
Zero Preservation under Monoid with Zero Homomorphisms: $f(a) = 0 \leftrightarrow a = 0$
Informal description
For a monoid with zero homomorphism $f \colon M_0 \to N_0$ and an element $a \in M_0$, the image $f(a)$ is zero if and only if $a$ is zero.
map_inv₀ theorem
: f a⁻¹ = (f a)⁻¹
Full source 
/-- A monoid homomorphism between groups with zeros sending `0` to `0` sends `a⁻¹` to `(f a)⁻¹`. -/
@[simp]
theorem map_inv₀ : f a⁻¹ = (f a)⁻¹ := by
  by_cases h : a = 0
  · simp [h, map_zero f]
  · apply eq_inv_of_mul_eq_one_left
    rw [← map_mul, inv_mul_cancel₀ h, map_one]
Inverse Preservation under Monoid Homomorphisms in Groups with Zero
Informal description
Let $G₀$ and $H₀$ be groups with zero, and let $f \colon G₀ \to H₀$ be a monoid homomorphism that maps $0$ to $0$. Then for any element $a \in G₀$, the image of the inverse $a^{-1}$ under $f$ is equal to the inverse of the image of $a$, i.e., $f(a^{-1}) = (f(a))^{-1}$.
map_div₀ theorem
: f (a / b) = f a / f b
Full source 
@[simp]
theorem map_div₀ : f (a / b) = f a / f b :=
  map_div' f (map_inv₀ f) a b
Division Preservation under Monoid Homomorphisms in Groups with Zero
Informal description
Let $G₀$ and $H₀$ be groups with zero, and let $f \colon G₀ \to H₀$ be a monoid homomorphism that maps $0$ to $0$. Then for any elements $a, b \in G₀$, the image of the quotient $a / b$ under $f$ is equal to the quotient of the images, i.e., $f(a / b) = f(a) / f(b)$.
MonoidWithZero.inverse definition
{M : Type*} [CommMonoidWithZero M] : M →*₀ M
Full source 
/-- We define the inverse as a `MonoidWithZeroHom` by extending the inverse map by zero
on non-units. -/
noncomputable def MonoidWithZero.inverse {M : Type*} [CommMonoidWithZero M] :
    M →*₀ M where
  toFun := Ring.inverse
  map_zero' := Ring.inverse_zero _
  map_one' := Ring.inverse_one _
  map_mul' x y := (Ring.mul_inverse_rev x y).trans (mul_comm _ _)
Inverse as a monoid with zero homomorphism
Informal description
The function `MonoidWithZero.inverse` is defined as a monoid with zero homomorphism from a commutative monoid with zero `M` to itself. It extends the inverse map by sending non-units to zero, i.e., for any `x ∈ M`, \[ \text{MonoidWithZero.inverse}(x) = \begin{cases} x^{-1} & \text{if } x \text{ is a unit}, \\ 0 & \text{otherwise}. \end{cases} \] This function preserves the multiplicative identity (sending 1 to 1), the zero element (sending 0 to 0), and satisfies the property that the inverse of a product is the product of the inverses in reverse order (i.e., `(xy)⁻¹ = y⁻¹x⁻¹`).
MonoidWithZero.coe_inverse theorem
{M : Type*} [CommMonoidWithZero M] : (MonoidWithZero.inverse : M → M) = Ring.inverse
Full source 
@[simp]
theorem MonoidWithZero.coe_inverse {M : Type*} [CommMonoidWithZero M] :
    (MonoidWithZero.inverse : M → M) = Ring.inverse :=
  rfl
Equality of MonoidWithZero.inverse and Ring.inverse Functions
Informal description
For any commutative monoid with zero $M$, the function `MonoidWithZero.inverse` (viewed as a function from $M$ to $M$) is equal to the function `Ring.inverse`.
MonoidWithZero.inverse_apply theorem
{M : Type*} [CommMonoidWithZero M] (a : M) : MonoidWithZero.inverse a = Ring.inverse a
Full source 
@[simp]
theorem MonoidWithZero.inverse_apply {M : Type*} [CommMonoidWithZero M] (a : M) :
    MonoidWithZero.inverse a = Ring.inverse a :=
  rfl
Equality of MonoidWithZero.inverse and Ring.inverse
Informal description
For any element $a$ in a commutative monoid with zero $M$, the value of the monoid-with-zero homomorphism `MonoidWithZero.inverse` at $a$ is equal to the value of the ring inverse function `Ring.inverse` at $a$.
invMonoidWithZeroHom definition
{G₀ : Type*} [CommGroupWithZero G₀] : G₀ →*₀ G₀
Full source 
/-- Inversion on a commutative group with zero, considered as a monoid with zero homomorphism. -/
def invMonoidWithZeroHom {G₀ : Type*} [CommGroupWithZero G₀] : G₀ →*₀ G₀ :=
  { invMonoidHom with map_zero' := inv_zero }
Inversion as a monoid with zero homomorphism
Informal description
The inversion operation on a commutative group with zero, considered as a monoid with zero homomorphism from the group to itself. It maps each element $a$ to its inverse $a^{-1}$, preserves the identity element ($1^{-1} = 1$), satisfies the homomorphism property $(ab)^{-1} = a^{-1}b^{-1}$ for all $a, b$ in the group, and maps zero to zero ($0^{-1} = 0$).
map_zpow₀ theorem
{F G₀ G₀' : Type*} [GroupWithZero G₀] [GroupWithZero G₀'] [FunLike F G₀ G₀'] [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (x : G₀) (n : ℤ) : f (x ^ n) = f x ^ n
Full source 
/-- If a monoid homomorphism `f` between two `GroupWithZero`s maps `0` to `0`, then it maps `x^n`,
`n : ℤ`, to `(f x)^n`. -/
@[simp]
theorem map_zpow₀ {F G₀ G₀' : Type*} [GroupWithZero G₀] [GroupWithZero G₀'] [FunLike F G₀ G₀']
    [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (x : G₀) (n : ℤ) : f (x ^ n) = f x ^ n :=
  map_zpow' f (map_inv₀ f) x n
Integer Power Preservation under Monoid-with-Zero Homomorphisms
Informal description
Let $G₀$ and $G₀'$ be groups with zero, and let $F$ be a type of homomorphisms from $G₀$ to $G₀'$ that preserve the monoid-with-zero structure. For any homomorphism $f \colon G₀ \to G₀'$ in $F$ and any element $x \in G₀$, the image of $x^n$ under $f$ equals the $n$-th power of $f(x)$ for all integers $n$, i.e., $f(x^n) = (f(x))^n$.