Documentation

Mathlib.Algebra.GroupWithZero.WithZero

Adjoining a zero to a group #

This file proves that one can adjoin a new zero element to a group and get a group with zero.

Main definitions #

instance WithZero.one {α : Type u_1} [One α] :
Equations
  • WithZero.one = { one := One.one }
@[simp]
theorem WithZero.coe_one {α : Type u_1} [One α] :
1 = 1
instance WithZero.mulZeroClass {α : Type u_1} [Mul α] :
Equations
@[simp]
theorem WithZero.coe_mul {α : Type u_1} [Mul α] (a : α) (b : α) :
(a * b) = a * b
theorem WithZero.unzero_mul {α : Type u_1} [Mul α] {x : WithZero α} {y : WithZero α} (hxy : x * y 0) :
instance WithZero.noZeroDivisors {α : Type u_1} [Mul α] :
Equations
  • =
Equations
Equations
Equations
@[simp]
theorem WithZero.coeMonoidHom_apply {α : Type u_1} [MulOneClass α] :
∀ (a : α), WithZero.coeMonoidHom a = a

Coercion as a monoid hom.

Equations
  • WithZero.coeMonoidHom = { toFun := WithZero.coe, map_one' := , map_mul' := }
theorem WithZero.monoidWithZeroHom_ext_iff {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] {f : WithZero α →*₀ β} {g : WithZero α →*₀ β} :
f = g (↑f).comp WithZero.coeMonoidHom = (↑g).comp WithZero.coeMonoidHom
theorem WithZero.monoidWithZeroHom_ext {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] ⦃f : WithZero α →*₀ β ⦃g : WithZero α →*₀ β (h : (↑f).comp WithZero.coeMonoidHom = (↑g).comp WithZero.coeMonoidHom) :
f = g
@[simp]
theorem WithZero.lift'_symm_apply_apply {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (F : WithZero α →*₀ β) :
∀ (a : α), (WithZero.lift'.symm F) a = F a
noncomputable def WithZero.lift' {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] :
(α →* β) (WithZero α →*₀ β)

The (multiplicative) universal property of WithZero.

Equations
  • One or more equations did not get rendered due to their size.
theorem WithZero.lift'_zero {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : α →* β) :
(WithZero.lift' f) 0 = 0
@[simp]
theorem WithZero.lift'_coe {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : α →* β) (x : α) :
(WithZero.lift' f) x = f x
theorem WithZero.lift'_unique {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : WithZero α →*₀ β) :
f = WithZero.lift' ((↑f).comp WithZero.coeMonoidHom)
noncomputable def WithZero.map' {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) :

The MonoidWithZero homomorphism WithZero α →* WithZero β induced by a monoid homomorphism f : α →* β.

Equations
theorem WithZero.map'_zero {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) :
@[simp]
theorem WithZero.map'_coe {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (x : α) :
(WithZero.map' f) x = (f x)
theorem WithZero.map'_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) (x : WithZero α) :
(WithZero.map' g) ((WithZero.map' f) x) = (WithZero.map' (g.comp f)) x
@[simp]
theorem WithZero.map'_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) :
WithZero.map' (g.comp f) = (WithZero.map' g).comp (WithZero.map' f)
instance WithZero.pow {α : Type u_1} [One α] [Pow α ] :
Equations
  • WithZero.pow = { pow := fun (x : WithZero α) (n : ) => match x, n with | none, 0 => 1 | none, n.succ => 0 | some x, n => (x ^ n) }
@[simp]
theorem WithZero.coe_pow {α : Type u_1} [One α] [Pow α ] (a : α) (n : ) :
(a ^ n) = a ^ n
Equations
Equations
instance WithZero.inv {α : Type u_1} [Inv α] :

Extend the inverse operation on α to WithZero α by sending 0 to 0.

Equations
@[simp]
theorem WithZero.coe_inv {α : Type u_1} [Inv α] (a : α) :
a⁻¹ = (↑a)⁻¹
@[simp]
theorem WithZero.inv_zero {α : Type u_1} [Inv α] :
0⁻¹ = 0
Equations
instance WithZero.div {α : Type u_1} [Div α] :
Equations
theorem WithZero.coe_div {α : Type u_1} [Div α] (a : α) (b : α) :
(a / b) = a / b
instance WithZero.instPowInt {α : Type u_1} [One α] [Pow α ] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem WithZero.coe_zpow {α : Type u_1} [One α] [Pow α ] (a : α) (n : ) :
(a ^ n) = a ^ n
Equations
Equations
Equations
Equations
Equations
instance WithZero.groupWithZero {α : Type u_1} [Group α] :

If α is a group then WithZero α is a group with zero.

Equations

Any group is isomorphic to the units of itself adjoined with 0.

Equations
  • WithZero.unitsWithZeroEquiv = { toFun := fun (a : (WithZero α)ˣ) => WithZero.unzero , invFun := fun (a : α) => Units.mk0 a , left_inv := , right_inv := , map_mul' := }
def WithZero.withZeroUnitsEquiv {G : Type u_4} [GroupWithZero G] [DecidablePred fun (a : G) => a = 0] :

Any group with zero is isomorphic to adjoining 0 to the units of itself.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def MulEquiv.withZero {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : α ≃* β) :

A version of Equiv.optionCongr for WithZero.

Equations
  • e.withZero = { toFun := (WithZero.map' e.toMonoidHom), invFun := (WithZero.map' e.symm.toMonoidHom), left_inv := , right_inv := , map_mul' := }
noncomputable def MulEquiv.unzero {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) :
α ≃* β

The inverse of MulEquiv.withZero.

Equations
  • e.unzero = { toFun := fun (x : α) => WithZero.unzero , invFun := fun (x : β) => WithZero.unzero , left_inv := , right_inv := , map_mul' := }
Equations
Equations