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

• WithZero.map': the MonoidWithZero homomorphism WithZero α →* WithZero β induced by a monoid homomorphism f : α →* β.

instance WithZero.one {α : Type u_1} [One α] : One (WithZero α)

Equations

• WithZero.one = { one := ↑One.one }

@[simp]

theorem WithZero.coe_one {α : Type u_1} [One α] : ↑1 = 1

instance WithZero.mulZeroClass {α : Type u_1} [Mul α] : MulZeroClass (WithZero α)

Equations

• WithZero.mulZeroClass = MulZeroClass.mk ⋯ ⋯

@[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) : WithZero.unzero hxy = WithZero.unzero ⋯ * WithZero.unzero ⋯

instance WithZero.noZeroDivisors {α : Type u_1} [Mul α] : NoZeroDivisors (WithZero α)

Equations

• ⋯ = ⋯

instance WithZero.semigroupWithZero {α : Type u_1} [Semigroup α] : SemigroupWithZero (WithZero α)

Equations

• WithZero.semigroupWithZero = SemigroupWithZero.mk ⋯ ⋯

instance WithZero.commSemigroup {α : Type u_1} [CommSemigroup α] : CommSemigroup (WithZero α)

Equations

• WithZero.commSemigroup = CommSemigroup.mk ⋯

instance WithZero.mulZeroOneClass {α : Type u_1} [MulOneClass α] : MulZeroOneClass (WithZero α)

Equations

• WithZero.mulZeroOneClass = MulZeroOneClass.mk ⋯ ⋯

@[simp]

theorem WithZero.coeMonoidHom_apply {α : Type u_1} [MulOneClass α] : ∀ (a : α), WithZero.coeMonoidHom a = ↑a

def WithZero.coeMonoidHom {α : Type u_1} [MulOneClass α] : α →* WithZero α

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 : α →* β) : WithZero α →*₀ WithZero β

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

Equations

• WithZero.map' f = WithZero.lift' (WithZero.coeMonoidHom.comp f)

theorem WithZero.map'_zero {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) : (WithZero.map' f) 0 = 0

@[simp]

theorem WithZero.map'_coe {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (x : α) : (WithZero.map' f) ↑x = ↑(f x)

@[simp]

theorem WithZero.map'_id {β : Type u_2} [MulOneClass β] : ↑(WithZero.map' (MonoidHom.id β)) = MonoidHom.id (WithZero β)

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 α ℕ] : Pow (WithZero α) ℕ

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

instance WithZero.monoidWithZero {α : Type u_1} [Monoid α] : MonoidWithZero (WithZero α)

Equations

• WithZero.monoidWithZero = MonoidWithZero.mk ⋯ ⋯

instance WithZero.commMonoidWithZero {α : Type u_1} [CommMonoid α] : CommMonoidWithZero (WithZero α)

Equations

• WithZero.commMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯

instance WithZero.inv {α : Type u_1} [Inv α] : Inv (WithZero α)

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

Equations

• WithZero.inv = { inv := fun (a : WithZero α) => Option.map (fun (x : α) => x⁻¹) a }

@[simp]

theorem WithZero.coe_inv {α : Type u_1} [Inv α] (a : α) : ↑a⁻¹ = (↑a)⁻¹

@[simp]

theorem WithZero.inv_zero {α : Type u_1} [Inv α] : 0⁻¹ = 0

instance WithZero.invOneClass {α : Type u_1} [InvOneClass α] : InvOneClass (WithZero α)

Equations

• WithZero.invOneClass = InvOneClass.mk ⋯

instance WithZero.div {α : Type u_1} [Div α] : Div (WithZero α)

Equations

• WithZero.div = { div := Option.map₂ fun (x1 x2 : α) => x1 / x2 }

theorem WithZero.coe_div {α : Type u_1} [Div α] (a : α) (b : α) : ↑(a / b) = ↑a / ↑b

instance WithZero.instPowInt {α : Type u_1} [One α] [Pow α ℤ] : Pow (WithZero α) ℤ

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

instance WithZero.divInvMonoid {α : Type u_1} [DivInvMonoid α] : DivInvMonoid (WithZero α)

Equations

• WithZero.divInvMonoid = DivInvMonoid.mk ⋯ (fun (n : ℤ) (a : WithZero α) => a ^ n) ⋯ ⋯ ⋯

instance WithZero.divInvOneMonoid {α : Type u_1} [DivInvOneMonoid α] : DivInvOneMonoid (WithZero α)

Equations

• WithZero.divInvOneMonoid = DivInvOneMonoid.mk ⋯

instance WithZero.involutiveInv {α : Type u_1} [InvolutiveInv α] : InvolutiveInv (WithZero α)

Equations

• WithZero.involutiveInv = InvolutiveInv.mk ⋯

instance WithZero.divisionMonoid {α : Type u_1} [DivisionMonoid α] : DivisionMonoid (WithZero α)

Equations

• WithZero.divisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯

instance WithZero.divisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] : DivisionCommMonoid (WithZero α)

Equations

• WithZero.divisionCommMonoid = DivisionCommMonoid.mk ⋯

instance WithZero.groupWithZero {α : Type u_1} [Group α] : GroupWithZero (WithZero α)

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

Equations

• WithZero.groupWithZero = GroupWithZero.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯ ⋯ ⋯

def WithZero.unitsWithZeroEquiv {α : Type u_1} [Group α] : (WithZero α)ˣ ≃* α

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] : WithZero Gˣ ≃* G

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 : α ≃* β) : WithZero α ≃* WithZero β

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' := ⋯ }

instance WithZero.commGroupWithZero {α : Type u_1} [CommGroup α] : CommGroupWithZero (WithZero α)

Equations

• WithZero.commGroupWithZero = CommGroupWithZero.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance WithZero.addMonoidWithOne {α : Type u_1} [AddMonoidWithOne α] : AddMonoidWithOne (WithZero α)

Equations

• WithZero.addMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯