More operations on WithOne and WithZero

This file defines various bundled morphisms on WithOne and WithZero that were not available in Algebra/Group/WithOne/Defs.

Main definitions

• WithOne.lift, WithZero.lift
• WithOne.map, WithZero.map

theorem WithZero.involutiveNeg.proof_1 {α : Type u_1} [InvolutiveNeg α] (a : WithZero α) : Option.map Neg.neg (Option.map Neg.neg a) = a

instance WithZero.involutiveNeg {α : Type u} [InvolutiveNeg α] : InvolutiveNeg (WithZero α)

Equations

• WithZero.involutiveNeg = let src := WithZero.neg; InvolutiveNeg.mk (_ : ∀ (a : WithZero α), Option.map Neg.neg (Option.map Neg.neg a) = a)

instance WithOne.involutiveInv {α : Type u} [InvolutiveInv α] : InvolutiveInv (WithOne α)

Equations

• WithOne.involutiveInv = let src := WithOne.inv; InvolutiveInv.mk (_ : ∀ (a : WithOne α), Option.map Inv.inv (Option.map Inv.inv a) = a)

theorem WithZero.coeAddHom.proof_1 {α : Type u_1} [Add α] : ∀ (x x_1 : α), ↑(x + x_1) = ↑(x + x_1)

def WithZero.coeAddHom {α : Type u} [Add α] : AddHom α (WithZero α)

WithZero.coe as a bundled morphism

Equations

• WithZero.coeAddHom = { toFun := WithZero.coe, map_add' := (_ : ∀ (x x_1 : α), ↑(x + x_1) = ↑(x + x_1)) }

@[simp]

theorem WithZero.coeAddHom_apply {α : Type u} [Add α] : ∀ (a : α), WithZero.coeAddHom a = ↑a

@[simp]

theorem WithOne.coeMulHom_apply {α : Type u} [Mul α] : ∀ (a : α), WithOne.coeMulHom a = ↑a

def WithOne.coeMulHom {α : Type u} [Mul α] : α →ₙ* WithOne α

WithOne.coe as a bundled morphism

Equations

• WithOne.coeMulHom = { toFun := WithOne.coe, map_mul' := (_ : ∀ (x x_1 : α), ↑(x * x_1) = ↑(x * x_1)) }

def WithZero.lift {α : Type u} {β : Type v} [Add α] [AddZeroClass β] : AddHom α β ≃ (WithZero α →+ β)

Lift an add semigroup homomorphism f to a bundled add monoid homomorphism.

Equations

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

theorem WithZero.lift.proof_1 {α : Type u_2} {β : Type u_1} [Add α] [AddZeroClass β] (f : AddHom α β) : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0

theorem WithZero.lift.proof_4 {α : Type u_2} {β : Type u_1} [Add α] [AddZeroClass β] (F : WithZero α →+ β) : (fun (f : AddHom α β) => { toZeroHom := { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }, map_add' := (_ : ∀ (x y : WithZero α), { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }.toFun (x + y) = { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }.toFun x + { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }.toFun y) }) ((fun (F : WithZero α →+ β) => AddHom.comp (↑F) WithZero.coeAddHom) F) = F

theorem WithZero.lift.proof_3 {α : Type u_2} {β : Type u_1} [Add α] [AddZeroClass β] (f : AddHom α β) : (fun (F : WithZero α →+ β) => AddHom.comp (↑F) WithZero.coeAddHom) ((fun (f : AddHom α β) => { toZeroHom := { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }, map_add' := (_ : ∀ (x y : WithZero α), { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }.toFun (x + y) = { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }.toFun x + { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }.toFun y) }) f) = f

theorem WithZero.lift.proof_2 {α : Type u_1} {β : Type u_2} [Add α] [AddZeroClass β] (f : AddHom α β) (x : WithZero α) (y : WithZero α) : { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }.toFun (x + y) = { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }.toFun x + { toFun := fun (x : WithZero α) => Option.casesOn x 0 ⇑f, map_zero' := (_ : (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0 = (fun (x : WithZero α) => Option.casesOn x 0 ⇑f) 0) }.toFun y

def WithOne.lift {α : Type u} {β : Type v} [Mul α] [MulOneClass β] : (α →ₙ* β) ≃ (WithOne α →* β)

Lift a semigroup homomorphism f to a bundled monoid homomorphism.

Equations

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

@[simp]

theorem WithZero.lift_coe {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : AddHom α β) (x : α) : (WithZero.lift f) ↑x = f x

@[simp]

theorem WithOne.lift_coe {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : α →ₙ* β) (x : α) : (WithOne.lift f) ↑x = f x

theorem WithZero.lift_zero {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : AddHom α β) : (WithZero.lift f) 0 = 0

theorem WithOne.lift_one {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : α →ₙ* β) : (WithOne.lift f) 1 = 1

theorem WithZero.lift_unique {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : WithZero α →+ β) : f = WithZero.lift (AddHom.comp (↑f) WithZero.coeAddHom)

theorem WithOne.lift_unique {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : WithOne α →* β) : f = WithOne.lift (MulHom.comp (↑f) WithOne.coeMulHom)

def WithZero.map {α : Type u} {β : Type v} [Add α] [Add β] (f : AddHom α β) : WithZero α →+ WithZero β

Given an additive map from α → β returns an add monoid homomorphism from WithZero α to WithZero β

Equations

• WithZero.map f = WithZero.lift (AddHom.comp WithZero.coeAddHom f)

def WithOne.map {α : Type u} {β : Type v} [Mul α] [Mul β] (f : α →ₙ* β) : WithOne α →* WithOne β

Given a multiplicative map from α → β returns a monoid homomorphism from WithOne α to WithOne β

Equations

• WithOne.map f = WithOne.lift (MulHom.comp WithOne.coeMulHom f)

@[simp]

theorem WithZero.map_coe {α : Type u} {β : Type v} [Add α] [Add β] (f : AddHom α β) (a : α) : (WithZero.map f) ↑a = ↑(f a)

@[simp]

theorem WithOne.map_coe {α : Type u} {β : Type v} [Mul α] [Mul β] (f : α →ₙ* β) (a : α) : (WithOne.map f) ↑a = ↑(f a)

@[simp]

theorem WithZero.map_id {α : Type u} [Add α] : WithZero.map (AddHom.id α) = AddMonoidHom.id (WithZero α)

@[simp]

theorem WithOne.map_id {α : Type u} [Mul α] : WithOne.map (MulHom.id α) = MonoidHom.id (WithOne α)

theorem WithZero.map_map {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : AddHom α β) (g : AddHom β γ) (x : WithZero α) : (WithZero.map g) ((WithZero.map f) x) = (WithZero.map (AddHom.comp g f)) x

theorem WithOne.map_map {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : WithOne α) : (WithOne.map g) ((WithOne.map f) x) = (WithOne.map (MulHom.comp g f)) x

@[simp]

theorem WithZero.map_comp {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : AddHom α β) (g : AddHom β γ) : WithZero.map (AddHom.comp g f) = AddMonoidHom.comp (WithZero.map g) (WithZero.map f)

@[simp]

theorem WithOne.map_comp {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) : WithOne.map (MulHom.comp g f) = MonoidHom.comp (WithOne.map g) (WithOne.map f)

theorem AddEquiv.withZeroCongr.proof_1 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : ∀ (x : WithZero α), (WithZero.map (AddEquiv.toAddHom (AddEquiv.symm e))) ((WithZero.map (AddEquiv.toAddHom e)) x) = x

theorem AddEquiv.withZeroCongr.proof_2 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (e : α ≃+ β) : ∀ (x : WithZero β), (WithZero.map (AddEquiv.toAddHom e)) ((WithZero.map (AddEquiv.toAddHom (AddEquiv.symm e))) x) = x

theorem AddEquiv.withZeroCongr.proof_3 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) (x : WithZero α) (y : WithZero α) : (↑(WithZero.map (AddEquiv.toAddHom e))).toFun (x + y) = (↑(WithZero.map (AddEquiv.toAddHom e))).toFun x + (↑(WithZero.map (AddEquiv.toAddHom e))).toFun y

def AddEquiv.withZeroCongr {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) : WithZero α ≃+ WithZero β

A version of Equiv.optionCongr for WithZero.

Equations

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

@[simp]

theorem AddEquiv.withZeroCongr_apply {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) (a : WithZero α) : (AddEquiv.withZeroCongr e) a = (WithZero.map (AddEquiv.toAddHom e)) a

@[simp]

theorem MulEquiv.withOneCongr_apply {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) (a : WithOne α) : (MulEquiv.withOneCongr e) a = (WithOne.map (MulEquiv.toMulHom e)) a

def MulEquiv.withOneCongr {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) : WithOne α ≃* WithOne β

A version of Equiv.optionCongr for WithOne.

Equations

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

@[simp]

theorem AddEquiv.withZeroCongr_refl {α : Type u} [Add α] : AddEquiv.withZeroCongr (AddEquiv.refl α) = AddEquiv.refl (WithZero α)

@[simp]

theorem MulEquiv.withOneCongr_refl {α : Type u} [Mul α] : MulEquiv.withOneCongr (MulEquiv.refl α) = MulEquiv.refl (WithOne α)

@[simp]

theorem AddEquiv.withZeroCongr_symm {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) : AddEquiv.symm (AddEquiv.withZeroCongr e) = AddEquiv.withZeroCongr (AddEquiv.symm e)

@[simp]

theorem MulEquiv.withOneCongr_symm {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) : MulEquiv.symm (MulEquiv.withOneCongr e) = MulEquiv.withOneCongr (MulEquiv.symm e)

@[simp]

theorem AddEquiv.withZeroCongr_trans {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) : AddEquiv.trans (AddEquiv.withZeroCongr e₁) (AddEquiv.withZeroCongr e₂) = AddEquiv.withZeroCongr (AddEquiv.trans e₁ e₂)

@[simp]

theorem MulEquiv.withOneCongr_trans {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (e₁ : α ≃* β) (e₂ : β ≃* γ) : MulEquiv.trans (MulEquiv.withOneCongr e₁) (MulEquiv.withOneCongr e₂) = MulEquiv.withOneCongr (MulEquiv.trans e₁ e₂)

instance WithZero.involutiveInv {α : Type u} [InvolutiveInv α] : InvolutiveInv (WithZero α)

Equations

• WithZero.involutiveInv = let src := WithZero.inv; InvolutiveInv.mk (_ : ∀ (a : WithZero α), Option.map Inv.inv (Option.map Inv.inv a) = a)

instance WithZero.divisionMonoid {α : Type u} [DivisionMonoid α] : DivisionMonoid (WithZero α)

Equations

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

instance WithZero.divisionCommMonoid {α : Type u} [DivisionCommMonoid α] : DivisionCommMonoid (WithZero α)

Equations

• WithZero.divisionCommMonoid = let src := WithZero.divisionMonoid; let src_1 := WithZero.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : WithZero α), a * b = b * a)