Mathlib.Algebra.GroupWithZero.WithZero

WithZero.one instance

: One (WithZero α)

Full source

instance one : One (WithZero α) where
  __ := ‹One α›

The One Element in a Group with Adjoined Zero

Informal description

The type `WithZero α` obtained by adjoining a zero element to a group `α` has a canonical one element, where the one element is the image of the one element of `α` under the inclusion map.

WithZero.coe_one theorem

: ((1 : α) : WithZero α) = 1

Full source

@[simp, norm_cast] lemma coe_one : ((1 : α) : WithZero α) = 1 := rfl

Inclusion Preserves Identity in Group with Adjoined Zero

Informal description

The canonical inclusion map from a group $\alpha$ to $\text{WithZero}(\alpha)$ preserves the multiplicative identity, i.e., the image of $1 \in \alpha$ under the inclusion is equal to $1 \in \text{WithZero}(\alpha)$.

WithZero.instMulZeroClass instance

: MulZeroClass (WithZero α)

Full source

instance instMulZeroClass : MulZeroClass (WithZero α) where
  mul := Option.map₂ (· * ·)
  zero_mul := Option.map₂_none_left (· * ·)
  mul_zero := Option.map₂_none_right (· * ·)

Multiplication with Zero Structure on Adjoined Zero Group

Informal description

The type `WithZero α` obtained by adjoining a zero element to a group `α` forms a `MulZeroClass`, where multiplication is defined by extending the group multiplication with the rule that any product involving zero is zero.

WithZero.coe_mul theorem

(a b : α) : (↑(a * b) : WithZero α) = a * b

Full source

@[simp, norm_cast] lemma coe_mul (a b : α) : (↑(a * b) : WithZero α) = a * b := rfl

Inclusion Preserves Multiplication in Group with Adjoined Zero

Informal description

For any two elements $a, b$ in a group $\alpha$, the canonical inclusion map from $\alpha$ to $\text{WithZero}(\alpha)$ preserves multiplication, i.e., the image of $a * b$ under the inclusion is equal to the product of the images of $a$ and $b$ in $\text{WithZero}(\alpha)$.

WithZero.unzero_mul theorem

 {x y : WithZero α} (hxy : x * y ≠ 0) :
  unzero hxy = unzero (left_ne_zero_of_mul hxy) * unzero (right_ne_zero_of_mul hxy)

Full source

lemma unzero_mul {x y : WithZero α} (hxy : x * y ≠ 0) :
    unzero hxy = unzero (left_ne_zero_of_mul hxy) * unzero (right_ne_zero_of_mul hxy) := by
  simp only [← coe_inj, coe_mul, coe_unzero]

Preservation of Nonzero Product under `unzero` in Group with Adjoined Zero

Informal description

For any two elements $x, y$ in the group with adjoined zero $\text{WithZero}(\alpha)$ such that their product $x \cdot y$ is nonzero, the element obtained by removing the zero case (via `unzero`) from $x \cdot y$ equals the product of the elements obtained by removing the zero case from $x$ and $y$ respectively. In other words, if $x \cdot y \neq 0$, then $\text{unzero}(x \cdot y) = \text{unzero}(x) \cdot \text{unzero}(y)$.

WithZero.instNoZeroDivisors instance

: NoZeroDivisors (WithZero α)

Full source

instance instNoZeroDivisors : NoZeroDivisors (WithZero α) := ⟨Option.map₂_eq_none_iff.1⟩

No Zero Divisors in Adjoined Zero Group

Informal description

The type `WithZero α` obtained by adjoining a zero element to a group `α` has no zero divisors. That is, for any two elements $x, y \in \text{WithZero }\alpha$, if $x \cdot y = 0$, then either $x = 0$ or $y = 0$.

WithZero.instSemigroupWithZero instance

[Semigroup α] : SemigroupWithZero (WithZero α)

Full source

instance instSemigroupWithZero [Semigroup α] : SemigroupWithZero (WithZero α) where
  mul_assoc _ _ _ := Option.map₂_assoc mul_assoc

Semigroup with Zero Structure on Adjoined Zero Semigroup

Informal description

For any semigroup $\alpha$, the type $\text{WithZero }\alpha$ obtained by adjoining a zero element to $\alpha$ forms a semigroup with zero. The multiplication operation extends the semigroup multiplication with the rule that any product involving zero is zero, and remains associative.

WithZero.instCommSemigroup instance

[CommSemigroup α] : CommSemigroup (WithZero α)

Full source

instance instCommSemigroup [CommSemigroup α] : CommSemigroup (WithZero α) where
  mul_comm _ _ := Option.map₂_comm mul_comm

Commutative Semigroup Structure on Adjoined Zero Commutative Semigroup

Informal description

For any commutative semigroup $\alpha$, the type $\text{WithZero }\alpha$ obtained by adjoining a zero element to $\alpha$ forms a commutative semigroup. The multiplication operation extends the semigroup multiplication with the rule that any product involving zero is zero, and remains associative and commutative.

WithZero.instMulZeroOneClass instance

[MulOneClass α] : MulZeroOneClass (WithZero α)

Full source

instance instMulZeroOneClass [MulOneClass α] : MulZeroOneClass (WithZero α) where
  one_mul := Option.map₂_left_identity one_mul
  mul_one := Option.map₂_right_identity mul_one

Multiplicative Structure with Zero and One on Adjoined Zero Group

Informal description

For any type $\alpha$ with a multiplicative identity and multiplication operation (i.e., a `MulOneClass`), the type `WithZero α` obtained by adjoining a zero element to $\alpha$ forms a `MulZeroOneClass`. This structure extends the multiplication operation with the rule that any product involving zero is zero, while preserving the multiplicative identity from $\alpha$.

WithZero.coeMonoidHom definition

: α →* WithZero α

Full source

/-- Coercion as a monoid hom. -/
@[simps apply]
def coeMonoidHom : α →* WithZero α where
  toFun        := (↑)
  map_one'     := rfl
  map_mul' _ _ := rfl

Canonical monoid homomorphism to $\text{WithZero}\ \alpha$

Informal description

The canonical monoid homomorphism from a type $\alpha$ to the type $\text{WithZero}\ \alpha$, which adjoins a zero element to $\alpha$. This homomorphism maps each element $a \in \alpha$ to itself in $\text{WithZero}\ \alpha$ and preserves the multiplicative identity and multiplication operation.

WithZero.monoidWithZeroHom_ext theorem

⦃f g : WithZero α →*₀ β⦄ (h : f.toMonoidHom.comp coeMonoidHom = g.toMonoidHom.comp coeMonoidHom) : f = g

Full source

@[ext high]
theorem monoidWithZeroHom_ext ⦃f g : WithZeroWithZero α →*₀ β⦄
    (h : f.toMonoidHom.comp coeMonoidHom = g.toMonoidHom.comp coeMonoidHom) :
    f = g :=
  DFunLike.ext _ _ fun
    | 0 => (map_zero f).trans (map_zero g).symm
    | (g : α) => DFunLike.congr_fun h g

Extensionality of Monoid-with-Zero Homomorphisms on Adjoined Zero Groups

Informal description

Let $\alpha$ and $\beta$ be types with multiplicative structures (MulOneClass), and let $f, g \colon \text{WithZero}\ \alpha \to^*_0 \beta$ be monoid-with-zero homomorphisms. If the compositions $f \circ \iota$ and $g \circ \iota$ are equal, where $\iota \colon \alpha \to^* \text{WithZero}\ \alpha$ is the canonical inclusion homomorphism, then $f = g$.

WithZero.lift' definition

: (α →* β) ≃ (WithZero α →*₀ β)

Full source

/-- The (multiplicative) universal property of `WithZero`. -/
@[simps! symm_apply_apply]
noncomputable nonrec def lift' : (α →* β) ≃ (WithZero α →*₀ β) where
  toFun f :=
    { toFun := fun
        | 0 => 0
        | (a : α) => f a
      map_zero' := rfl
      map_one' := map_one f
      map_mul' := fun
        | 0, _ => (zero_mul _).symm
        | (_ : α), 0 => (mul_zero _).symm
        | (_ : α), (_ : α) => map_mul f _ _ }
  invFun F := F.toMonoidHom.comp coeMonoidHom
  left_inv _ := rfl
  right_inv _ := monoidWithZeroHom_ext rfl

Universal property of adjoining a zero to a monoid

Informal description

The equivalence between monoid homomorphisms $ \alpha \to^* \beta $ and monoid-with-zero homomorphisms $ \text{WithZero}\ \alpha \to^*_0 \beta $. Given a monoid homomorphism $ f \colon \alpha \to^* \beta $, the corresponding monoid-with-zero homomorphism $ \text{WithZero}\ \alpha \to^*_0 \beta $ is defined by: - Mapping $ 0 $ to $ 0 $, - Mapping $ (a : \alpha) $ to $ f(a) $. Conversely, any monoid-with-zero homomorphism $ F \colon \text{WithZero}\ \alpha \to^*_0 \beta $ restricts to a monoid homomorphism $ \alpha \to^* \beta $ by precomposing with the canonical inclusion $ \alpha \to \text{WithZero}\ \alpha $. This equivalence is bijective, meaning the two constructions are mutual inverses.

WithZero.lift'_zero theorem

(f : α →* β) : lift' f (0 : WithZero α) = 0

Full source

lemma lift'_zero (f : α →* β) : lift' f (0 : WithZero α) = 0 := rfl

Zero Preservation in Induced Monoid-with-Zero Homomorphism

Informal description

For any monoid homomorphism $f \colon \alpha \to^* \beta$, the induced monoid-with-zero homomorphism $\text{lift'}\ f \colon \text{WithZero}\ \alpha \to^*_0 \beta$ maps the zero element $0 \in \text{WithZero}\ \alpha$ to the zero element $0 \in \beta$.

WithZero.lift'_coe theorem

(f : α →* β) (x : α) : lift' f (x : WithZero α) = f x

Full source

@[simp] lemma lift'_coe (f : α →* β) (x : α) : lift' f (x : WithZero α) = f x := rfl

Lift of Monoid Homomorphism Preserves Nonzero Elements

Informal description

For any monoid homomorphism $f \colon \alpha \to \beta$ and any element $x \in \alpha$, the lift of $f$ to $\text{WithZero}\ \alpha$ evaluated at the inclusion of $x$ equals $f(x)$, i.e., $\text{lift}'\, f\, (x : \text{WithZero}\ \alpha) = f(x)$.

WithZero.lift'_unique theorem

(f : WithZero α →*₀ β) : f = lift' (f.toMonoidHom.comp coeMonoidHom)

Full source

lemma lift'_unique (f : WithZeroWithZero α →*₀ β) : f = lift' (f.toMonoidHom.comp coeMonoidHom) :=
  (lift'.apply_symm_apply f).symm

Uniqueness of Monoid-with-Zero Homomorphism via Lifting

Informal description

For any monoid-with-zero homomorphism $f \colon \text{WithZero}\ \alpha \to^*_0 \beta$, $f$ is equal to the homomorphism obtained by lifting the composition of $f$ with the canonical inclusion $\alpha \to \text{WithZero}\ \alpha$. That is, $f = \text{lift}'(f \circ \iota)$, where $\iota \colon \alpha \to \text{WithZero}\ \alpha$ is the canonical monoid homomorphism.

WithZero.map' definition

(f : α →* β) : WithZero α →*₀ WithZero β

Full source

/-- The `MonoidWithZero` homomorphism `WithZero α →* WithZero β` induced by a monoid homomorphism
  `f : α →* β`. -/
noncomputable def map' (f : α →* β) : WithZeroWithZero α →*₀ WithZero β := lift' (coeMonoidHom.comp f)

Induced monoid-with-zero homomorphism from adjoining a zero

Informal description

Given a monoid homomorphism $ f \colon \alpha \to^* \beta $, the function `WithZero.map' f` is the induced monoid-with-zero homomorphism from `WithZero α` to `WithZero β`, defined by: - Mapping $ 0 $ to $ 0 $, - Mapping $ (a : \alpha) $ to $ f(a) $.

WithZero.map'_zero theorem

(f : α →* β) : map' f 0 = 0

Full source

lemma map'_zero (f : α →* β) : map' f 0 = 0 := rfl

Preservation of Zero by Induced Monoid-with-Zero Homomorphism

Informal description

For any monoid homomorphism $f \colon \alpha \to^* \beta$, the induced monoid-with-zero homomorphism $\text{WithZero.map'}\ f$ maps the zero element $0$ in $\text{WithZero}\ \alpha$ to the zero element $0$ in $\text{WithZero}\ \beta$.

WithZero.map'_coe theorem

(f : α →* β) (x : α) : map' f (x : WithZero α) = f x

Full source

@[simp] lemma map'_coe (f : α →* β) (x : α) : map' f (x : WithZero α) = f x := rfl

Image of Nonzero Element under Induced Monoid-with-Zero Homomorphism

Informal description

Given a monoid homomorphism $f \colon \alpha \to \beta$ and an element $x \in \alpha$, the induced monoid-with-zero homomorphism $\text{map}'\, f$ maps the element $x$ in $\text{WithZero}\, \alpha$ to $f(x)$ in $\text{WithZero}\, \beta$. That is, $\text{map}'\, f\, x = f(x)$.

WithZero.map'_id theorem

: map' (MonoidHom.id β) = MonoidHom.id (WithZero β)

Full source

@[simp]
lemma map'_id : map' (MonoidHom.id β) = MonoidHom.id (WithZero β) := by
  ext x; induction x <;> rfl

Identity Preservation in `WithZero.map'`

Informal description

The induced monoid-with-zero homomorphism `WithZero.map'` applied to the identity monoid homomorphism on $\beta$ is equal to the identity monoid homomorphism on `WithZero β`.

WithZero.map'_map' theorem

(f : α →* β) (g : β →* γ) (x) : map' g (map' f x) = map' (g.comp f) x

Full source

lemma map'_map'  (f : α →* β) (g : β →* γ) (x) : map' g (map' f x) = map' (g.comp f) x := by
  induction x <;> rfl

Composition Property of Induced Monoid-with-Zero Homomorphisms

Informal description

Given monoid homomorphisms $f \colon \alpha \to^* \beta$ and $g \colon \beta \to^* \gamma$, and an element $x$ in $\text{WithZero}\,\alpha$, the following equality holds: $$ \text{map'}\,g\,(\text{map'}\,f\,x) = \text{map'}\,(g \circ f)\,x $$ where $\text{map'}$ is the induced monoid-with-zero homomorphism obtained by adjoining a zero element, and $\circ$ denotes the composition of monoid homomorphisms.

WithZero.map'_comp theorem

(f : α →* β) (g : β →* γ) : map' (g.comp f) = (map' g).comp (map' f)

Full source

@[simp]
lemma map'_comp (f : α →* β) (g : β →* γ) : map' (g.comp f) = (map' g).comp (map' f) :=
  MonoidWithZeroHom.ext fun x => (map'_map' f g x).symm

Composition of Induced Monoid-with-Zero Homomorphisms

Informal description

Given monoid homomorphisms $f \colon \alpha \to^* \beta$ and $g \colon \beta \to^* \gamma$, the induced monoid-with-zero homomorphism of the composition $g \circ f$ is equal to the composition of the induced homomorphisms, i.e., $$ \text{map'}\,(g \circ f) = \text{map'}\,g \circ \text{map'}\,f. $$

WithZero.pow instance

: Pow (WithZero α) ℕ

Full source

instance pow : Pow (WithZero α) ℕ where
  pow
    | none, 0 => 1
    | none, _ + 1 => 0
    | some x, n => ↑(x ^ n)

Power Operation on a Group with Adjoined Zero

Informal description

For any group $\alpha$, the type $\text{WithZero}\,\alpha$ obtained by adjoining a zero element to $\alpha$ has a natural power operation $\text{WithZero}\,\alpha \to \mathbb{N} \to \text{WithZero}\,\alpha$ defined by extending the power operation on $\alpha$ with $0^n = 0$ for all $n \in \mathbb{N}$.

WithZero.coe_pow theorem

(a : α) (n : ℕ) : (↑(a ^ n) : WithZero α) = a ^ n

Full source

@[simp, norm_cast] lemma coe_pow (a : α) (n : ℕ) : (↑(a ^ n) : WithZero α) = a ^ n := rfl

Compatibility of Power Operation with Zero Adjoined: $\uparrow(a^n) = a^n$

Informal description

For any element $a$ in a group $\alpha$ and any natural number $n$, the canonical inclusion of $a^n$ into $\text{WithZero}\,\alpha$ equals the $n$-th power of $a$ in $\text{WithZero}\,\alpha$, i.e., $\uparrow(a^n) = a^n$.

WithZero.instMonoidWithZero instance

[Monoid α] : MonoidWithZero (WithZero α)

Full source

instance instMonoidWithZero [Monoid α] : MonoidWithZero (WithZero α) where
  npow n a := a ^ n
  npow_zero
    | 0 => rfl
    | some _ => congr_arg some (pow_zero _)
  npow_succ
    | n, 0 => by simp only [mul_zero]; rfl
    | n, some _ => congr_arg some <| pow_succ _ _

Monoid with Zero Structure on Adjoined Zero Group

Informal description

For any monoid $\alpha$, the type $\text{WithZero}\,\alpha$ obtained by adjoining a zero element to $\alpha$ forms a monoid with zero. This structure extends the multiplication operation from $\alpha$ with the rule that any product involving zero is zero, while preserving the multiplicative identity from $\alpha$.

WithZero.instCommMonoidWithZero instance

[CommMonoid α] : CommMonoidWithZero (WithZero α)

Full source

instance instCommMonoidWithZero [CommMonoid α] : CommMonoidWithZero (WithZero α) :=
  { WithZero.instMonoidWithZero, WithZero.instCommSemigroup with }

Commutative Monoid with Zero Structure on Adjoined Zero Commutative Monoid

Informal description

For any commutative monoid $\alpha$, the type $\text{WithZero}\,\alpha$ obtained by adjoining a zero element to $\alpha$ forms a commutative monoid with zero. The multiplication operation extends the monoid multiplication with the rule that any product involving zero is zero, while preserving the multiplicative identity and commutativity from $\alpha$.

WithZero.inv instance

: Inv (WithZero α)

Full source

/-- Extend the inverse operation on `α` to `WithZero α` by sending `0` to `0`. -/
instance inv : Inv (WithZero α) where inv a := Option.map (·⁻¹) a

Inverse Operation on a Group with Zero

Informal description

For any group $\alpha$, the type `WithZero α` (obtained by adjoining a zero element to $\alpha$) has an inverse operation that extends the inverse operation on $\alpha$ by sending $0$ to $0$.

WithZero.coe_inv theorem

(a : α) : ((a⁻¹ : α) : WithZero α) = (↑a)⁻¹

Full source

@[simp, norm_cast] lemma coe_inv (a : α) : ((a⁻¹ : α) : WithZero α) = (↑a)⁻¹ := rfl

Inclusion of Inverse Equals Inverse of Inclusion in $\text{WithZero}\,\alpha$

Informal description

For any element $a$ in a group $\alpha$, the canonical inclusion of the inverse $a^{-1}$ into $\text{WithZero}\,\alpha$ equals the inverse of the inclusion of $a$, i.e., $(a^{-1} : \text{WithZero}\,\alpha) = (a : \text{WithZero}\,\alpha)^{-1}$.

WithZero.inv_zero theorem

: (0 : WithZero α)⁻¹ = 0

Full source

@[simp] protected lemma inv_zero : (0 : WithZero α)⁻¹ = 0 := rfl

Inverse of Zero in a Group with Adjoined Zero

Informal description

For any group $\alpha$ with an adjoined zero element (denoted as `WithZero α`), the inverse of zero is zero, i.e., $0^{-1} = 0$.

WithZero.invOneClass instance

[InvOneClass α] : InvOneClass (WithZero α)

Full source

instance invOneClass [InvOneClass α] : InvOneClass (WithZero α) where
  inv_one := show ((1⁻¹ : α) : WithZero α) = 1 by simp

Inverse of One is One in a Group with Adjoined Zero

Informal description

For any group $\alpha$ where the inverse of the identity element is itself (i.e., $1^{-1} = 1$), the type `WithZero α` (obtained by adjoining a zero element to $\alpha$) also satisfies this property. In other words, the inverse of the identity element in `WithZero α` is the identity element itself.

WithZero.div instance

: Div (WithZero α)

Full source

instance div : Div (WithZero α) where div := Option.map₂ (· / ·)

Division Operation on a Group with Adjoined Zero

Informal description

The type `WithZero α` (obtained by adjoining a zero element to a group α) has a division operation extending the division operation from α, where division by zero is defined to be zero.

WithZero.coe_div theorem

(a b : α) : ↑(a / b : α) = (a / b : WithZero α)

Full source

@[norm_cast] lemma coe_div (a b : α) : ↑(a / b : α) = (a / b : WithZero α) := rfl

Inclusion Map Preserves Division in Group with Adjoined Zero

Informal description

For any elements $a$ and $b$ in a group $\alpha$, the canonical inclusion map from $\alpha$ to $\alpha$ with an adjoined zero element preserves division, i.e., the image of $a / b$ in $\alpha$ under the inclusion map equals the division of the images of $a$ and $b$ in $\alpha$ with zero.

WithZero.instPowInt instance

: Pow (WithZero α) ℤ

Full source

instance : Pow (WithZero α) ℤ where
  pow
    | none, Int.ofNat 0 => 1
    | none, Int.ofNat (Nat.succ _) => 0
    | none, Int.negSucc _ => 0
    | some x, n => ↑(x ^ n)

Integer Power Operation on a Group with Adjoined Zero

Informal description

For any group $\alpha$, the type $\alpha$ with an adjoined zero element has a power operation with integer exponents, extending the power operation from $\alpha$.

WithZero.coe_zpow theorem

(a : α) (n : ℤ) : ↑(a ^ n) = (↑a : WithZero α) ^ n

Full source

@[simp, norm_cast] lemma coe_zpow (a : α) (n : ℤ) : ↑(a ^ n) = (↑a : WithZero α) ^ n := rfl

Inclusion Map Preserves Integer Powers in Group with Adjoined Zero

Informal description

For any element $a$ in a group $\alpha$ and any integer exponent $n$, the canonical inclusion map from $\alpha$ to $\alpha$ with an adjoined zero element preserves integer powers, i.e., the image of $a^n$ under the inclusion map equals the $n$-th power of the image of $a$ in $\alpha$ with zero.

WithZero.instDivInvMonoid instance

[DivInvMonoid α] : DivInvMonoid (WithZero α)

Full source

instance instDivInvMonoid [DivInvMonoid α] : DivInvMonoid (WithZero α) where
  div_eq_mul_inv
    | none, _ => rfl
    | some _, none => rfl
    | some a, some b => congr_arg some (div_eq_mul_inv a b)
  zpow n a := a ^ n
  zpow_zero'
    | none => rfl
    | some _ => congr_arg some (zpow_zero _)
  zpow_succ'
    | n, none => by change 0 ^ _ = 0 ^ _ * 0; simp only [mul_zero]; rfl
    | n, some _ => congr_arg some (DivInvMonoid.zpow_succ' _ _)
  zpow_neg'
    | n, none => rfl
    | n, some _ => congr_arg some (DivInvMonoid.zpow_neg' _ _)

Division-Inversion Monoid Structure on a Group with Adjoined Zero

Informal description

For any division-inversion monoid $\alpha$, the type $\text{WithZero}\,\alpha$ obtained by adjoining a zero element to $\alpha$ forms a division-inversion monoid. This structure extends the division and inversion operations from $\alpha$ by defining division by zero and the inverse of zero to be zero.

WithZero.instDivInvOneMonoid instance

[DivInvOneMonoid α] : DivInvOneMonoid (WithZero α)

Full source

instance instDivInvOneMonoid [DivInvOneMonoid α] : DivInvOneMonoid (WithZero α) where

Division-Inversion Monoid with One Structure on a Group with Adjoined Zero

Informal description

For any division-inversion monoid with one $\alpha$, the type $\text{WithZero}\,\alpha$ obtained by adjoining a zero element to $\alpha$ forms a division-inversion monoid with one. This structure extends the division and inversion operations from $\alpha$ while preserving the property that the inverse of the multiplicative identity is itself.

WithZero.instInvolutiveInv instance

[InvolutiveInv α] : InvolutiveInv (WithZero α)

Full source

instance instInvolutiveInv [InvolutiveInv α] : InvolutiveInv (WithZero α) where
  inv_inv a := (Option.map_map _ _ _).trans <| by simp [Function.comp]

Involutive Inversion on a Group with Zero

Informal description

For any group $\alpha$ with an involutive inversion operation, the type `WithZero α` (obtained by adjoining a zero element to $\alpha$) also has an involutive inversion operation, where the inversion operation on $\alpha$ is extended by sending $0$ to $0$.

WithZero.instDivisionMonoid instance

[DivisionMonoid α] : DivisionMonoid (WithZero α)

Full source

instance instDivisionMonoid [DivisionMonoid α] : DivisionMonoid (WithZero α) where
  mul_inv_rev
    | none, none => rfl
    | none, some _ => rfl
    | some _, none => rfl
    | some _, some _ => congr_arg some (mul_inv_rev _ _)
  inv_eq_of_mul
    | none, none, _ => rfl
    | some _, some _, h =>
      congr_arg some <| inv_eq_of_mul_eq_one_right <| Option.some_injective _ h

Division Monoid Structure on a Group with Adjoined Zero

Informal description

For any division monoid $\alpha$, the type $\text{WithZero}\,\alpha$ obtained by adjoining a zero element to $\alpha$ forms a division monoid. This structure extends the division and inversion operations from $\alpha$ by defining division by zero and the inverse of zero to be zero.

WithZero.instDivisionCommMonoid instance

[DivisionCommMonoid α] : DivisionCommMonoid (WithZero α)

Full source

instance instDivisionCommMonoid [DivisionCommMonoid α] : DivisionCommMonoid (WithZero α) where

Commutative Division Monoid Structure on a Group with Adjoined Zero

Informal description

For any commutative division monoid $\alpha$, the type $\text{WithZero}\,\alpha$ obtained by adjoining a zero element to $\alpha$ forms a commutative division monoid. This structure extends the division and inversion operations from $\alpha$ by defining division by zero and the inverse of zero to be zero, while preserving the commutativity of the binary operation for nonzero elements.

WithZero.instGroupWithZero instance

: GroupWithZero (WithZero α)

Full source

/-- If `α` is a group then `WithZero α` is a group with zero. -/
instance instGroupWithZero : GroupWithZero (WithZero α) where
  inv_zero := WithZero.inv_zero
  mul_inv_cancel a ha := by
    lift a to α using ha
    norm_cast
    apply mul_inv_cancel

Group with Zero Structure on Adjoined Zero Group

Informal description

For any group $\alpha$, the type $\text{WithZero}\,\alpha$ obtained by adjoining a zero element to $\alpha$ forms a group with zero. This structure extends the group operations from $\alpha$ by defining division by zero and the inverse of zero to be zero, while preserving the group properties for nonzero elements.

WithZero.unitsWithZeroEquiv definition

: (WithZero α)ˣ ≃* α

Full source

/-- Any group is isomorphic to the units of itself adjoined with `0`. -/
def unitsWithZeroEquiv : (WithZero α)ˣ(WithZero α)ˣ ≃* α where
  toFun a := unzero a.ne_zero
  invFun a := Units.mk0 a coe_ne_zero
  left_inv _ := Units.ext <| by simp only [coe_unzero, Units.mk0_val]
  right_inv _ := rfl
  map_mul' _ _ := coe_inj.mp <| by simp only [Units.val_mul, coe_unzero, coe_mul]

Multiplicative equivalence between units of adjoined-zero group and original group

Informal description

The multiplicative equivalence between the group of units of $\text{WithZero}\,\alpha$ and the group $\alpha$ itself. Specifically: - The forward map sends each unit $u$ in $\text{WithZero}\,\alpha$ to its underlying nonzero value in $\alpha$. - The inverse map sends each element $a$ in $\alpha$ to the unit $\text{Units.mk0 } a$, which is the element $a$ viewed as a unit in $\text{WithZero}\,\alpha$ (with proof that $a \neq 0$). This equivalence preserves the multiplicative structure, meaning that for any units $u, v$ in $\text{WithZero}\,\alpha$, the image of $u \cdot v$ in $\alpha$ equals the product of their individual images.

WithZero.coe_unitsWithZeroEquiv_eq_units_val theorem

(γ : (WithZero α)ˣ) : ↑(unitsWithZeroEquiv γ) = γ.val

Full source

theorem coe_unitsWithZeroEquiv_eq_units_val (γ : (WithZero α)ˣ) :
    ↑(unitsWithZeroEquiv γ) = γ.val := by
  simp only [WithZero.unitsWithZeroEquiv, MulEquiv.coe_mk, Equiv.coe_fn_mk, WithZero.coe_unzero]

Equality of Unit Values in Adjoined-Zero Group and Original Group

Informal description

For any unit $\gamma$ in the group of units of $\text{WithZero}\,\alpha$, the underlying value of $\gamma$ in $\alpha$ (obtained via the multiplicative equivalence $\text{unitsWithZeroEquiv}$) equals the value of $\gamma$ itself.

WithZero.withZeroUnitsEquiv definition

{G : Type*} [GroupWithZero G] [DecidablePred (fun a : G ↦ a = 0)] : WithZero Gˣ ≃* G

Full source

/-- Any group with zero is isomorphic to adjoining `0` to the units of itself. -/
def withZeroUnitsEquiv {G : Type*} [GroupWithZero G]
    [DecidablePred (fun a : G ↦ a = 0)] :
    WithZeroWithZero Gˣ ≃* G where
  toFun := WithZero.recZeroCoe 0 Units.val
  invFun a := if h : a = 0 then 0 else (Units.mk0 a h : Gˣ)
  left_inv := (by induction · <;> simp)
  right_inv _ := by simp only; split <;> simp_all
  map_mul' := (by induction · <;> induction · <;> simp [← WithZero.coe_mul])

Multiplicative equivalence between adjoined-zero units and group with zero

Informal description

For any group with zero $G$ and a decidable predicate on whether an element is zero, there is a multiplicative equivalence between the type obtained by adjoining a zero to the group of units of $G$ and $G$ itself. The equivalence is defined by: - The forward map sends the adjoined zero to $0$ and any unit $u$ to its underlying value in $G$ - The inverse map sends $0$ to the adjoined zero and any nonzero element $a$ to the unit $\text{Units.mk0 } a \text{ h}$ (where $h$ is the proof that $a \neq 0$)

MulEquiv.withZero definition

[Group β] (e : α ≃* β) : WithZero α ≃* WithZero β

Full source

/-- A version of `Equiv.optionCongr` for `WithZero`. -/
noncomputable def _root_.MulEquiv.withZero [Group β] (e : α ≃* β) :
    WithZeroWithZero α ≃* WithZero β where
  toFun := map' e.toMonoidHom
  invFun := map' e.symm.toMonoidHom
  left_inv := (by induction · <;> simp)
  right_inv := (by induction · <;> simp)
  map_mul' := (by induction · <;> induction · <;> simp)

Multiplicative equivalence induced by adjoining a zero to groups

Informal description

Given a multiplicative equivalence (isomorphism) $ e \colon \alpha \simeq^* \beta $ between groups $\alpha$ and $\beta$, the function `MulEquiv.withZero` constructs a multiplicative equivalence $\text{WithZero}\,\alpha \simeq^* \text{WithZero}\,\beta$ between the types obtained by adjoining a zero element to $\alpha$ and $\beta$. The equivalence is defined by: - The forward map sends $0$ to $0$ and any $a \in \alpha$ to $e(a) \in \beta$ - The inverse map sends $0$ to $0$ and any $b \in \beta$ to $e^{-1}(b) \in \alpha$ - The equivalence preserves multiplication and satisfies the left and right inverse properties.

MulEquiv.unzero definition

[Group β] (e : WithZero α ≃* WithZero β) : α ≃* β

Full source

/-- The inverse of `MulEquiv.withZero`. -/
protected noncomputable def _root_.MulEquiv.unzero [Group β] (e : WithZeroWithZero α ≃* WithZero β) :
    α ≃* β where
  toFun x := unzero (x := e x) (by simp [ne_eq, ← e.eq_symm_apply])
  invFun x := unzero (x := e.symm x) (by simp [e.symm_apply_eq])
  left_inv _ := by simp
  right_inv _ := by simp
  map_mul' _ _ := by
    simp only [coe_mul, map_mul]
    generalize_proofs A B C
    suffices ((unzero A : β) : WithZero β) = (unzero B) * (unzero C) by
      rwa [← WithZero.coe_mul, WithZero.coe_inj] at this
    simp

Restriction of multiplicative equivalence to non-zero elements

Informal description

Given a multiplicative equivalence $e : \text{WithZero}(\alpha) \simeq^* \text{WithZero}(\beta)$ between types obtained by adjoining a zero element to groups $\alpha$ and $\beta$, the function constructs a multiplicative equivalence $\alpha \simeq^* \beta$ by restricting $e$ to the non-zero elements. The construction ensures that: 1. The function maps $x \in \alpha$ to the non-zero part of $e(x) \in \text{WithZero}(\beta)$ 2. The inverse function maps $y \in \beta$ to the non-zero part of $e^{-1}(y) \in \text{WithZero}(\alpha)$ 3. The resulting map preserves multiplication and satisfies the left and right inverse properties.

WithZero.instCommGroupWithZero instance

[CommGroup α] : CommGroupWithZero (WithZero α)

Full source

instance instCommGroupWithZero [CommGroup α] : CommGroupWithZero (WithZero α) where

Commutative Group with Zero Structure on Adjoined Zero Commutative Group

Informal description

For any commutative group $\alpha$, the type $\text{WithZero}\,\alpha$ obtained by adjoining a zero element to $\alpha$ forms a commutative group with zero. This structure extends the group operations from $\alpha$ by defining division by zero and the inverse of zero to be zero, while preserving the commutativity and group properties for nonzero elements.

WithZero.instAddMonoidWithOne instance

[AddMonoidWithOne α] : AddMonoidWithOne (WithZero α)

Full source

instance instAddMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (WithZero α) where
  natCast n := if n = 0 then 0 else (n : α)
  natCast_zero := rfl
  natCast_succ n := by cases n <;> simp

Adjoining Zero Preserves Additive Monoid with One Structure

Informal description

For any additive monoid with one $\alpha$, the type $\text{WithZero}(\alpha)$ obtained by adjoining a zero element to $\alpha$ is also an additive monoid with one.

Main definitions