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 : α →* β.

source

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

One (WithZero α)

Equations

source

@[simp]

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

↑1 = 1

source

instance WithZero.instMulZeroClass {α : Type u_1} [Mul α] :

MulZeroClass (WithZero α)

Equations

source

@[simp]

theorem WithZero.coe_mul {α : Type u_1} [Mul α] (a b : α) :

↑(a * b) = ↑a * ↑b

source

theorem WithZero.unzero_mul {α : Type u_1} [Mul α] {x y : WithZero α} (hxy : x * y ≠ 0) :

unzero hxy = unzero ⋯ * unzero ⋯

source

instance WithZero.instNoZeroDivisors {α : Type u_1} [Mul α] :

NoZeroDivisors (WithZero α)

source

instance WithZero.instSemigroupWithZero {α : Type u_1} [Semigroup α] :

SemigroupWithZero (WithZero α)

Equations

source

instance WithZero.instCommSemigroup {α : Type u_1} [CommSemigroup α] :

CommSemigroup (WithZero α)

Equations

source

instance WithZero.instMulZeroOneClass {α : Type u_1} [MulOneClass α] :

MulZeroOneClass (WithZero α)

Equations

source

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

α →* WithZero α

Coercion as a monoid hom.

Equations

Instances For

source

@[simp]

theorem WithZero.coeMonoidHom_apply {α : Type u_1} [MulOneClass α] (a✝ : α) :

coeMonoidHom a✝ = ↑a✝

source

theorem WithZero.monoidWithZeroHom_ext {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] ⦃f g : WithZero α →*₀ β⦄ (h : (↑f).comp coeMonoidHom = (↑g).comp coeMonoidHom) :

f = g

source

theorem WithZero.monoidWithZeroHom_ext_iff {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] {f g : WithZero α →*₀ β} :

f = g ↔ (↑f).comp coeMonoidHom = (↑g).comp coeMonoidHom

source

noncomputable def WithZero.lift' {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] :

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

The (multiplicative) universal property of WithZero.

Equations

Instances For

source

@[simp]

theorem WithZero.lift'_symm_apply_apply {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (F : WithZero α →*₀ β) (a✝ : α) :

(lift'.symm F) a✝ = F ↑a✝

source

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

(lift' f) 0 = 0

source

@[simp]

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

(lift' f) ↑x = f x

source

theorem WithZero.lift'_unique {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : WithZero α →*₀ β) :

f = lift' ((↑f).comp coeMonoidHom)

source

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

Instances For

source

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

(map' f) 0 = 0

source

@[simp]

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

(map' f) ↑x = ↑(f x)

source

@[simp]

theorem WithZero.map'_id {β : Type u_2} [MulOneClass β] :

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

source

theorem WithZero.map'_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) (x : WithZero α) :

(map' g) ((map' f) x) = (map' (g.comp f)) x

source

@[simp]

theorem WithZero.map'_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) :

map' (g.comp f) = (map' g).comp (map' f)

source

instance WithZero.pow {α : Type u_1} [One α] [Pow α ℕ] :

Pow (WithZero α) ℕ

Equations

source

@[simp]

theorem WithZero.coe_pow {α : Type u_1} [One α] [Pow α ℕ] (a : α) (n : ℕ) :

↑(a ^ n) = ↑a ^ n

source

instance WithZero.instMonoidWithZero {α : Type u_1} [Monoid α] :

MonoidWithZero (WithZero α)

Equations

source

instance WithZero.instCommMonoidWithZero {α : Type u_1} [CommMonoid α] :

CommMonoidWithZero (WithZero α)

Equations

source

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

Inv (WithZero α)

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

Equations

source

@[simp]

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

↑a⁻¹ = (↑a)⁻¹

source

@[simp]

theorem WithZero.inv_zero {α : Type u_1} [Inv α] :

0⁻¹ = 0

source

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

InvOneClass (WithZero α)

Equations

source

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

Div (WithZero α)

Equations

source

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

↑(a / b) = ↑a / ↑b

source

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

Pow (WithZero α) ℤ

Equations

source

@[simp]

theorem WithZero.coe_zpow {α : Type u_1} [One α] [Pow α ℤ] (a : α) (n : ℤ) :

↑(a ^ n) = ↑a ^ n

source

instance WithZero.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :

DivInvMonoid (WithZero α)

Equations

source

instance WithZero.instDivInvOneMonoid {α : Type u_1} [DivInvOneMonoid α] :

DivInvOneMonoid (WithZero α)

Equations

source

instance WithZero.instInvolutiveInv {α : Type u_1} [InvolutiveInv α] :

InvolutiveInv (WithZero α)

Equations

source

instance WithZero.instDivisionMonoid {α : Type u_1} [DivisionMonoid α] :

DivisionMonoid (WithZero α)

Equations

source

instance WithZero.instDivisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] :

DivisionCommMonoid (WithZero α)

Equations

source

instance WithZero.instGroupWithZero {α : Type u_1} [Group α] :

GroupWithZero (WithZero α)

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

Equations

source

def WithZero.unitsWithZeroEquiv {α : Type u_1} [Group α] :

(WithZero α)ˣ ≃* α

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

Equations

Instances For

source

theorem WithZero.coe_unitsWithZeroEquiv_eq_units_val {α : Type u_1} [Group α] (γ : (WithZero α)ˣ) :

↑(unitsWithZeroEquiv γ) = ↑γ

source

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

Instances For

source

noncomputable def MulEquiv.withZero {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : α ≃* β) :

WithZero α ≃* WithZero β

A version of Equiv.optionCongr for WithZero.

Equations

Instances For

source

noncomputable def MulEquiv.unzero {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) :

α ≃* β

The inverse of MulEquiv.withZero.

Equations

Instances For

source

instance WithZero.instCommGroupWithZero {α : Type u_1} [CommGroup α] :

CommGroupWithZero (WithZero α)

Equations

source

instance WithZero.instAddMonoidWithOne {α : Type u_1} [AddMonoidWithOne α] :

AddMonoidWithOne (WithZero α)

Equations

Documentation

Mathlib.Algebra.GroupWithZero.WithZero

Adjoining a zero to a group #

Main definitions #