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ᵐ⁰
forWithZero (Multiplicative M)
Main definitions #
WithZero.map'
: theMonoidWithZero
homomorphismWithZero α →* WithZero β
induced by a monoid homomorphismf : α →* β
.WithZero.exp
: The "exponential map"M → Mᵐ⁰
WithZero.exp
: The "logarithm"Mᵐ⁰ → M
Equations
- WithZero.instMulZeroClass = { mul := Option.map₂ fun (x1 x2 : α) => x1 * x2, toZero := WithZero.instZero, zero_mul := ⋯, mul_zero := ⋯ }
Equations
- WithZero.instSemigroupWithZero = { toMul := WithZero.instMulZeroClass.toMul, mul_assoc := ⋯, toZero := WithZero.instMulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }
Equations
- WithZero.instCommSemigroup = { toSemigroup := WithZero.instSemigroupWithZero.toSemigroup, mul_comm := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Coercion as a monoid hom.
Equations
- WithZero.coeMonoidHom = { toFun := WithZero.coe, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The (multiplicative) universal property of WithZero
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The MonoidWithZero
homomorphism WithZero α →* WithZero β
induced by a monoid homomorphism
f : α →* β
.
Equations
Instances For
Alias of the reverse direction of WithZero.map'_injective_iff
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- WithZero.instCommMonoidWithZero = { toMonoid := WithZero.instMonoidWithZero.toMonoid, mul_comm := ⋯, toZero := WithZero.instMonoidWithZero.toZero, zero_mul := ⋯, mul_zero := ⋯ }
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 }
Equations
- WithZero.invOneClass = { toOne := WithZero.one, toInv := WithZero.inv, inv_one := ⋯ }
Equations
- WithZero.div = { div := Option.map₂ fun (x1 x2 : α) => x1 / x2 }
Equations
- One or more equations did not get rendered due to their size.
Equations
- WithZero.instDivInvOneMonoid = { toDivInvMonoid := WithZero.instDivInvMonoid, inv_one := ⋯ }
Equations
- WithZero.instInvolutiveInv = { toInv := WithZero.inv, inv_inv := ⋯ }
Equations
- WithZero.instDivisionMonoid = { toDivInvMonoid := WithZero.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }
Equations
- WithZero.instDivisionCommMonoid = { toDivisionMonoid := WithZero.instDivisionMonoid, mul_comm := ⋯ }
If α
is a group then WithZero α
is a group with zero.
Equations
- One or more equations did not get rendered due to their size.
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' := ⋯ }
Instances For
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.
Instances For
The inverse of MulEquiv.withZero
.
Equations
- e.unzero = MulEquiv.withZero.symm e
Instances For
Equations
- One or more equations did not get rendered due to their size.
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 #
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 "ᵐ⁰")
Instances For
The exponential map as a function M → Mᵐ⁰
.
Equations
- WithZero.exp a = ↑(Multiplicative.ofAdd a)
Instances For
The logarithm as a function Mᵐ⁰ → M
with junk value log 0 = 0
.
Equations
- x.log = WithZero.recZeroCoe 0 (⇑Multiplicative.toAdd) x
Instances For
The exponential map as an equivalence between G
and (Gᵐ⁰)ˣ
.
Instances For
The logarithm as an equivalence between (Gᵐ⁰)ˣ
and G
.
Instances For
The trivial group-with-zero hom is absorbing for composition.
The trivial group-with-zero hom is absorbing for composition.