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'
: theMonoidWithZero
homomorphismWithZero α →* WithZero β
induced by a monoid homomorphismf : α →* β
.
Equations
- WithZero.mulZeroClass = MulZeroClass.mk ⋯ ⋯
theorem
WithZero.unzero_mul
{α : Type u_1}
[Mul α]
{x : WithZero α}
{y : WithZero α}
(hxy : x * y ≠ 0)
:
WithZero.unzero hxy = WithZero.unzero ⋯ * WithZero.unzero ⋯
Equations
- ⋯ = ⋯
Equations
- WithZero.semigroupWithZero = let __spread.0 := WithZero.mulZeroClass; SemigroupWithZero.mk ⋯ ⋯
Equations
- WithZero.commSemigroup = let __spread.0 := WithZero.semigroupWithZero; CommSemigroup.mk ⋯
Equations
- WithZero.mulZeroOneClass = let __spread.0 := WithZero.mulZeroClass; MulZeroOneClass.mk ⋯ ⋯
@[simp]
theorem
WithZero.coeMonoidHom_apply
{α : Type u_1}
[MulOneClass α]
:
∀ (a : α), WithZero.coeMonoidHom a = ↑a
Coercion as a monoid hom.
Equations
- WithZero.coeMonoidHom = { 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 : (↑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 β]
:
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' ((↑f).comp WithZero.coeMonoidHom)
noncomputable def
WithZero.map'
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
:
The MonoidWithZero
homomorphism WithZero α →* WithZero β
induced by a monoid homomorphism
f : α →* β
.
Equations
- WithZero.map' f = WithZero.lift' (WithZero.coeMonoidHom.comp 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' (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)
Equations
- WithZero.monoidWithZero = let __spread.0 := WithZero.mulZeroOneClass; let __spread.1 := WithZero.semigroupWithZero; MonoidWithZero.mk ⋯ ⋯
Equations
- WithZero.commMonoidWithZero = let __src := WithZero.monoidWithZero; let __src_1 := WithZero.commSemigroup; CommMonoidWithZero.mk ⋯ ⋯
Equations
- WithZero.invOneClass = InvOneClass.mk ⋯
Equations
- WithZero.div = { div := Option.map₂ fun (x x_1 : α) => x / x_1 }
Equations
- WithZero.divInvMonoid = let __spread.0 := WithZero.monoidWithZero; DivInvMonoid.mk ⋯ (fun (n : ℤ) (a : WithZero α) => a ^ n) ⋯ ⋯ ⋯
Equations
- WithZero.divInvOneMonoid = let __spread.0 := WithZero.divInvMonoid; let __spread.1 := WithZero.invOneClass; DivInvOneMonoid.mk ⋯
Equations
- WithZero.involutiveInv = InvolutiveInv.mk ⋯
Equations
- WithZero.divisionMonoid = let __spread.0 := WithZero.divInvMonoid; let __spread.1 := WithZero.involutiveInv; DivisionMonoid.mk ⋯ ⋯ ⋯
Equations
- WithZero.divisionCommMonoid = let __spread.0 := WithZero.divisionMonoid; let __spread.1 := WithZero.commSemigroup; DivisionCommMonoid.mk ⋯
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 ⋯ ⋯ ⋯ ⋯ ⋯
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
Equations
- WithZero.commGroupWithZero = let __src := WithZero.groupWithZero; let __src_1 := WithZero.commMonoidWithZero; CommGroupWithZero.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- WithZero.addMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯