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 #

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 = let __spread.0 := inst; { 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 = let __spread.0 := WithZero.mulZeroClass; SemigroupWithZero.mk ⋯ ⋯

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

CommSemigroup (WithZero α)

Equations

WithZero.commSemigroup = let __spread.0 := WithZero.semigroupWithZero; CommSemigroup.mk ⋯

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

MulZeroOneClass (WithZero α)

Equations

WithZero.mulZeroOneClass = let __spread.0 := WithZero.mulZeroClass; 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 = { toOneHom := { toFun := WithZero.coe, map_one' := ⋯ }, map_mul' := ⋯ }

Instances For

theorem WithZero.monoidWithZeroHom_ext {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] ⦃f : WithZero α →*₀ β⦄ ⦃g : WithZero α →*₀ β⦄ (h : MonoidHom.comp (↑f) WithZero.coeMonoidHom = MonoidHom.comp (↑g) 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.

Instances For

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' (MonoidHom.comp (↑f) 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' (MonoidHom.comp WithZero.coeMonoidHom f)

Instances For

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' (MonoidHom.comp g f)) x

@[simp]

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

WithZero.map' (MonoidHom.comp g f) = MonoidWithZeroHom.comp (WithZero.map' g) (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, Nat.succ n => 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 = let __spread.0 := WithZero.mulZeroOneClass; let __spread.1 := WithZero.semigroupWithZero; MonoidWithZero.mk ⋯ ⋯

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

CommMonoidWithZero (WithZero α)

Equations

WithZero.commMonoidWithZero = let __src := WithZero.monoidWithZero; let __src_1 := WithZero.commSemigroup; 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 α] :

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 (x x_1 : α) => x / x_1 }

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

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

instance WithZero.instPowWithZeroInt {α : 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 = let __spread.0 := WithZero.monoidWithZero; DivInvMonoid.mk ⋯ (fun (n : ℤ) (a : WithZero α) => a ^ n) ⋯ ⋯ ⋯

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

DivInvOneMonoid (WithZero α)

Equations

WithZero.divInvOneMonoid = let __spread.0 := WithZero.divInvMonoid; let __spread.1 := WithZero.invOneClass; 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 = let __spread.0 := WithZero.divInvMonoid; let __spread.1 := WithZero.involutiveInv; DivisionMonoid.mk ⋯ ⋯ ⋯

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

DivisionCommMonoid (WithZero α)

Equations

WithZero.divisionCommMonoid = let __spread.0 := WithZero.divisionMonoid; let __spread.1 := WithZero.commSemigroup; 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 = let __spread.0 := WithZero.monoidWithZero; let __spread.1 := WithZero.divInvMonoid; let __spread.2 := ⋯; 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

One or more equations did not get rendered due to their size.

Instances For

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

CommGroupWithZero (WithZero α)

Equations

WithZero.commGroupWithZero = let __src := WithZero.groupWithZero; let __src_1 := WithZero.commMonoidWithZero; CommGroupWithZero.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯

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

AddMonoidWithOne (WithZero α)

Equations

WithZero.addMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯