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.

In valuation theory, valuations have codomain {0} ∪ {c ^ n | n : ℤ} for some c > 1, which we can formalise as ℤᵐ⁰ := WithZero (Multiplicative ℤ). It is important to be able to talk about the maps n ↦ c ^ n and c ^ n ↦ n. We define these as exp : ℤ → ℤᵐ⁰ and log : ℤᵐ⁰ → ℤ with junk value log 0 = 0. Junkless versions are defined as expEquiv : ℤ ≃ ℤᵐ⁰ˣ and logEquiv : ℤᵐ⁰ˣ ≃ ℤ.

Notation

In locale WithZero:

• Mᵐ⁰ for WithZero (Multiplicative M)

Main definitions

• WithZero.map': the MonoidWithZero homomorphism WithZero α →* WithZero β induced by a monoid homomorphism f : α →* β.
• WithZero.exp: The "exponential map" M → Mᵐ⁰
• WithZero.exp: The "logarithm" Mᵐ⁰ → M

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

@[simp]

theorem WithZero.recZeroCoe_one {M : Type u_4} {N : Type u_5} [One M] (f : M → N) (z : N) : recZeroCoe z f 1 = f 1

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

Equations

• WithZero.instMulZeroClass = { mul := Option.map₂ fun (x1 x2 : α) => x1 * x2, toZero := WithZero.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[simp]

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

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

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

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

Equations

• WithZero.instSemigroupWithZero = { toMul := WithZero.instMulZeroClass.toMul, mul_assoc := ⋯, toZero := WithZero.instMulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

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

Equations

• WithZero.instCommSemigroup = { toSemigroup := WithZero.instSemigroupWithZero.toSemigroup, mul_comm := ⋯ }

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

Equations

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

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

Coercion as a monoid hom.

Equations

• WithZero.coeMonoidHom = { toFun := WithZero.coe, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

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

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

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

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.

@[simp]

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

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

@[simp]

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

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

theorem WithZero.lift'_surjective {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] {f : α →* β} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(lift' f)

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 : α →* β) : (map' f) 0 = 0

@[simp]

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

@[simp]

theorem WithZero.map'_id {β : Type u_2} [MulOneClass β] : ↑(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 α) : (map' g) ((map' f) x) = (map' (g.comp f)) x

@[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)

theorem WithZero.map'_injective_iff {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] {f : α →* β} : Function.Injective ⇑(map' f) ↔ Function.Injective ⇑f

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

Alias of the reverse direction of WithZero.map'_injective_iff.

theorem WithZero.map'_surjective_iff {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] {f : α →* β} : Function.Surjective ⇑(map' f) ↔ Function.Surjective ⇑f

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

Alias of the reverse direction of WithZero.map'_surjective_iff.

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

Equations

• WithZero.pow = { pow := fun (x : WithZero α) (x_1 : ℕ) => match x, x_1 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.instMonoidWithZero {α : Type u_1} [Monoid α] : MonoidWithZero (WithZero α)

Equations

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

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

Equations

• WithZero.instCommMonoidWithZero = { toMonoid := WithZero.instMonoidWithZero.toMonoid, mul_comm := ⋯, toZero := WithZero.instMonoidWithZero.toZero, zero_mul := ⋯, mul_zero := ⋯ }

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 = { toOne := WithZero.one, toInv := WithZero.inv, inv_one := ⋯ }

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.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] : DivInvMonoid (WithZero α)

Equations

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

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

Equations

• WithZero.instDivInvOneMonoid = { toDivInvMonoid := WithZero.instDivInvMonoid, inv_one := ⋯ }

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

Equations

• WithZero.instInvolutiveInv = { toInv := WithZero.inv, inv_inv := ⋯ }

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

Equations

• WithZero.instDivisionMonoid = { toDivInvMonoid := WithZero.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }

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

Equations

• WithZero.instDivisionCommMonoid = { toDivisionMonoid := WithZero.instDivisionMonoid, mul_comm := ⋯ }

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

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

Equations

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

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

@[simp]

theorem WithZero.unitsWithZeroEquiv_symm_apply {α : Type u_1} [Group α] (a : α) : unitsWithZeroEquiv.symm a = Units.mk0 ↑a ⋯

@[simp]

theorem WithZero.unitsWithZeroEquiv_apply {α : Type u_1} [Group α] (a : (WithZero α)ˣ) : unitsWithZeroEquiv a = unzero ⋯

instance WithZero.instNontrivialUnits {α : Type u_1} [Group α] [Nontrivial α] : Nontrivial (WithZero α)ˣ

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

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.

@[simp]

theorem WithZero.withZeroUnitsEquiv_apply {G : Type u_4} [GroupWithZero G] [DecidablePred fun (a : G) => a = 0] (n : WithZero Gˣ) : withZeroUnitsEquiv n = recZeroCoe 0 Units.val n

@[simp]

theorem WithZero.withZeroUnitsEquiv_symm_apply {G : Type u_4} [GroupWithZero G] [DecidablePred fun (a : G) => a = 0] (a : G) : withZeroUnitsEquiv.symm a = if h : a = 0 then 0 else ↑(Units.mk0 a h)

theorem WithZero.withZeroUnitsEquiv_symm_apply_coe {G : Type u_4} [GroupWithZero G] [DecidablePred fun (a : G) => a = 0] (a : Gˣ) : withZeroUnitsEquiv.symm ↑a = ↑a

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

A version of Equiv.optionCongr for WithZero.

Equations

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

@[simp]

theorem MulEquiv.withZero_symm_apply_apply {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) (x : α) : (withZero.symm e) x = WithZero.unzero ⋯

@[simp]

theorem MulEquiv.withZero_apply_apply {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : α ≃* β) (a : WithZero α) : (withZero e) a = (WithZero.map' ↑e) a

@[simp]

theorem MulEquiv.withZero_apply_symm_apply {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : α ≃* β) (a : WithZero β) : (withZero e).symm a = (WithZero.map' ↑e.symm) a

@[simp]

theorem MulEquiv.withZero_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) (x : β) : (withZero.symm e).symm x = WithZero.unzero ⋯

@[reducible, inline]

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

The inverse of MulEquiv.withZero.

Equations

• e.unzero = MulEquiv.withZero.symm e

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

Equations

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

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

Equations

• WithZero.instAddMonoidWithOne = { natCast := fun (n : ℕ) => if n = 0 then 0 else ↑↑n, toAddMonoid := WithZero.instAddMonoid, toOne := WithZero.one, natCast_zero := ⋯, natCast_succ := ⋯ }

Exponential and logarithm

def WithZero.«term_ᵐ⁰» : Lean.TrailingParserDescr

Mᵐ⁰ is notation for WithZero (Multiplicative M).

This naturally shows up as the codomain of valuations in valuation theory.

Equations

• WithZero.«term_ᵐ⁰» = Lean.ParserDescr.trailingNode `WithZero.«term_ᵐ⁰» 1024 1024 (Lean.ParserDescr.symbol "ᵐ⁰")

def WithZero.exp {M : Type u_4} (a : M) : WithZero (Multiplicative M)

The exponential map as a function M → Mᵐ⁰.

Equations

• WithZero.exp a = ↑(Multiplicative.ofAdd a)

@[simp]

theorem WithZero.exp_ne_zero {M : Type u_4} {a : M} : exp a ≠ 0

def WithZero.log {M : Type u_4} [AddMonoid M] (x : WithZero (Multiplicative M)) : M

The logarithm as a function Mᵐ⁰ → M with junk value log 0 = 0.

Equations

• x.log = WithZero.recZeroCoe 0 (⇑Multiplicative.toAdd) x

@[simp]

theorem WithZero.log_exp {M : Type u_4} [AddMonoid M] (a : M) : (exp a).log = a

@[simp]

theorem WithZero.exp_log {M : Type u_4} [AddMonoid M] {x : WithZero (Multiplicative M)} (hx : x ≠ 0) : exp x.log = x

@[simp]

theorem WithZero.log_zero {M : Type u_4} [AddMonoid M] : log 0 = 0

@[simp]

theorem WithZero.exp_zero {M : Type u_4} [AddMonoid M] : exp 0 = 1

@[simp]

theorem WithZero.log_one {M : Type u_4} [AddMonoid M] : log 1 = 0

theorem WithZero.exp_add {M : Type u_4} [AddMonoid M] (a b : M) : exp (a + b) = exp a * exp b

theorem WithZero.log_mul {M : Type u_4} [AddMonoid M] {x y : WithZero (Multiplicative M)} (hx : x ≠ 0) (hy : y ≠ 0) : (x * y).log = x.log + y.log

theorem WithZero.exp_nsmul {M : Type u_4} [AddMonoid M] (n : ℕ) (a : M) : exp (n • a) = exp a ^ n

theorem WithZero.log_pow {M : Type u_4} [AddMonoid M] (x : WithZero (Multiplicative M)) (n : ℕ) : (x ^ n).log = n • x.log

def WithZero.expEquiv {G : Type u_5} [AddGroup G] : G ≃ (WithZero (Multiplicative G))ˣ

The exponential map as an equivalence between G and (Gᵐ⁰)ˣ.

Equations

• WithZero.expEquiv = Multiplicative.ofAdd.trans WithZero.unitsWithZeroEquiv.symm.toEquiv

def WithZero.logEquiv {G : Type u_5} [AddGroup G] : (WithZero (Multiplicative G))ˣ ≃ G

The logarithm as an equivalence between (Gᵐ⁰)ˣ and G.

Equations

• WithZero.logEquiv = WithZero.unitsWithZeroEquiv.trans Multiplicative.toAdd

@[simp]

theorem WithZero.logEquiv_symm {G : Type u_5} [AddGroup G] : logEquiv.symm = expEquiv

@[simp]

theorem WithZero.expEquiv_symm {G : Type u_5} [AddGroup G] : expEquiv.symm = logEquiv

@[simp]

theorem WithZero.coe_expEquiv_apply {G : Type u_5} [AddGroup G] (a : G) : ↑(expEquiv a) = exp a

@[simp]

theorem WithZero.logEquiv_apply {G : Type u_5} [AddGroup G] (x : (WithZero (Multiplicative G))ˣ) : logEquiv x = (↑x).log

theorem WithZero.logEquiv_unitsMk0 {G : Type u_5} [AddGroup G] (x : WithZero (Multiplicative G)) (hx : x ≠ 0) : logEquiv (Units.mk0 x hx) = x.log

theorem WithZero.exp_sub {G : Type u_5} [AddGroup G] (a b : G) : exp (a - b) = exp a / exp b

theorem WithZero.log_div {G : Type u_5} [AddGroup G] {x y : WithZero (Multiplicative G)} (hx : x ≠ 0) (hy : y ≠ 0) : (x / y).log = x.log - y.log

theorem WithZero.exp_neg {G : Type u_5} [AddGroup G] (a : G) : exp (-a) = (exp a)⁻¹

theorem WithZero.log_inv {G : Type u_5} [AddGroup G] (x : WithZero (Multiplicative G)) : x⁻¹.log = -x.log

theorem WithZero.exp_zsmul {G : Type u_5} [AddGroup G] (n : ℤ) (a : G) : exp (n • a) = exp a ^ n

theorem WithZero.log_zpow {G : Type u_5} [AddGroup G] (x : WithZero (Multiplicative G)) (n : ℤ) : (x ^ n).log = n • x.log

theorem MonoidWithZeroHom.map_eq_zero_iff {G₀ : Type u_1} {G₀' : Type u_2} [GroupWithZero G₀] [MulZeroOneClass G₀'] [Nontrivial G₀'] {f : G₀ →*₀ G₀'} {x : G₀} : f x = 0 ↔ x = 0

@[simp]

theorem MonoidWithZeroHom.one_apply_val_unit {M₀ : Type u_1} {N₀ : Type u_2} [MonoidWithZero M₀] [MulZeroOneClass N₀] [DecidablePred fun (x : M₀) => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] (x : M₀ˣ) : 1 ↑x = 1

@[simp]

theorem MonoidWithZeroHom.apply_one_apply_eq {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀] [MulZeroOneClass N₀] [MulZeroOneClass G₀] [DecidablePred fun (x : M₀) => x = 0] (f : N₀ →*₀ G₀) (x : M₀) : f (1 x) = 1 x

The trivial group-with-zero hom is absorbing for composition.

@[simp]

theorem MonoidWithZeroHom.comp_one {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀] [MulZeroOneClass N₀] [MulZeroOneClass G₀] [DecidablePred fun (x : M₀) => x = 0] (f : N₀ →*₀ G₀) : f.comp 1 = 1

The trivial group-with-zero hom is absorbing for composition.