Documentation

Mathlib.Algebra.Group.WithOne.Defs

Adjoining a zero/one to semigroups and related algebraic structures #

This file contains different results about adjoining an element to an algebraic structure which then behaves like a zero or a one. An example is adjoining a one to a semigroup to obtain a monoid. That this provides an example of an adjunction is proved in Algebra.Category.MonCat.Adjunctions.

Another result says that adjoining to a group an element zero gives a GroupWithZero. For more information about these structures (which are not that standard in informal mathematics, see Algebra.GroupWithZero.Basic)

Porting notes #

In Lean 3, we use id here and there to get correct types of proofs. This is required because with_one and with_zero are marked as irreducible at the end of algebra.group.with_one.defs, so proofs that use option α instead of with_one α no longer typecheck. In Lean 4, both types are plain defs, so we don't need these ids.

def WithZero (α : Type u_1) :
Type u_1

Add an extra element 0 to a type

Equations
def WithOne (α : Type u_1) :
Type u_1

Add an extra element 1 to a type

Equations
instance WithOne.instReprWithZero {α : Type u} [inst : Repr α] :
Repr ()
Equations
• WithOne.instReprWithZero = { reprPrec := fun o x => match o with | none => | some a => ++ repr a }
instance WithZero.instReprWithZero {α : Type u} [inst : Repr α] :
Repr ()
Equations
• One or more equations did not get rendered due to their size.
abbrev WithZero.instReprWithZero.match_1 {α : Type u_1} (motive : Sort u_2) :
(o : ) → (Unitmotive none) → ((a : α) → motive (some a)) → motive o
Equations
instance WithOne.instReprWithOne {α : Type u} [inst : Repr α] :
Repr ()
Equations
• WithOne.instReprWithOne = { reprPrec := fun o x => match o with | none => | some a => ++ repr a }
Equations
Equations
instance WithZero.zero {α : Type u} :
Zero ()
Equations
• WithZero.zero = { zero := none }
instance WithOne.one {α : Type u} :
One ()
Equations
• WithOne.one = { one := none }
Equations
instance WithOne.mul {α : Type u} [inst : Mul α] :
Mul ()
Equations
instance WithZero.neg {α : Type u} [inst : Neg α] :
Neg ()
Equations
• WithZero.neg = { neg := fun a => Option.map Neg.neg a }
instance WithOne.inv {α : Type u} [inst : Inv α] :
Inv ()
Equations
instance WithZero.involutiveNeg {α : Type u} [inst : ] :
Equations
def WithZero.involutiveNeg.proof_1 {α : Type u_1} [inst : ] (a : ) :
Option.map Neg.neg (Option.map Neg.neg a) = a
Equations
instance WithOne.involutiveInv {α : Type u} [inst : ] :
Equations
def WithZero.negZeroClass.proof_1 {α : Type u_1} [inst : Neg α] :
-0 = -0
Equations
instance WithZero.negZeroClass {α : Type u} [inst : Neg α] :
Equations
• WithZero.negZeroClass = let src := WithZero.zero; let src_1 := WithZero.neg; NegZeroClass.mk (_ : -0 = -0)
instance WithOne.invOneClass {α : Type u} [inst : Inv α] :
Equations
instance WithZero.inhabited {α : Type u} :
Equations
• WithZero.inhabited = { default := 0 }
instance WithOne.inhabited {α : Type u} :
Equations
• WithOne.inhabited = { default := 1 }
instance WithZero.nontrivial {α : Type u} [inst : ] :
Equations
def WithZero.nontrivial.proof_1 {α : Type u_1} [inst : ] :
Equations
instance WithOne.nontrivial {α : Type u} [inst : ] :
Equations
def WithZero.coe {α : Type u} :
α

The canonical map from α into WithZero α

Equations
• WithZero.coe = some
def WithOne.coe {α : Type u} :
α

The canonical map from α into WithOne α

Equations
• WithOne.coe = some
instance WithZero.coeTC {α : Type u} :
CoeTC α ()
Equations
• WithZero.coeTC = { coe := WithZero.coe }
instance WithOne.coeTC {α : Type u} :
CoeTC α ()
Equations
• WithOne.coeTC = { coe := WithOne.coe }
def WithZero.recZeroCoe {α : Type u} {C : Sort u_1} (h₁ : C 0) (h₂ : (a : α) → C a) (n : ) :
C n

Recursor for WithZero using the preferred forms 0 and ↑a.

Equations
def WithOne.recOneCoe {α : Type u} {C : Sort u_1} (h₁ : C 1) (h₂ : (a : α) → C a) (n : ) :
C n

Recursor for WithOne using the preferred forms 1 and ↑a.

Equations
def WithZero.unzero {α : Type u} {x : } (hx : x 0) :
α

Deconstruct a x : WithZero α to the underlying value in α, given a proof that x ≠ 0.

Equations
def WithOne.unone {α : Type u} {x : } (hx : x 1) :
α

Deconstruct a x : WithOne α to the underlying value in α, given a proof that x ≠ 1.

Equations
@[simp]
theorem WithZero.unzero_coe {α : Type u} {x : α} (hx : x 0) :
= x
@[simp]
theorem WithOne.unone_coe {α : Type u} {x : α} (hx : x 1) :
= x
@[simp]
theorem WithZero.coe_unzero {α : Type u} {x : } (hx : x 0) :
↑() = x
@[simp]
theorem WithOne.coe_unone {α : Type u} {x : } (hx : x 1) :
↑() = x
@[simp]
theorem WithZero.coe_ne_zero {α : Type u} {a : α} :
a 0
@[simp]
theorem WithOne.coe_ne_one {α : Type u} {a : α} :
a 1
@[simp]
theorem WithZero.zero_ne_coe {α : Type u} {a : α} :
0 a
@[simp]
theorem WithOne.one_ne_coe {α : Type u} {a : α} :
1 a
theorem WithZero.ne_zero_iff_exists {α : Type u} {x : } :
x 0 a, a = x
theorem WithOne.ne_one_iff_exists {α : Type u} {x : } :
x 1 a, a = x
instance WithZero.canLift {α : Type u} :
CanLift () α WithZero.coe fun a => a 0
Equations
• WithZero.canLift = { prf := (_ : ∀ (x : ), x 0a, a = x) }
def WithZero.canLift.proof_1 {α : Type u_1} :
∀ (x : ), x 0a, a = x
Equations
• (_ : x 0a, a = x) = (_ : x 0a, a = x)
instance WithOne.canLift {α : Type u} :
CanLift () α WithOne.coe fun a => a 1
Equations
• WithOne.canLift = { prf := (_ : ∀ (x : ), x 1a, a = x) }
@[simp]
theorem WithZero.coe_inj {α : Type u} {a : α} {b : α} :
a = b a = b
@[simp]
theorem WithOne.coe_inj {α : Type u} {a : α} {b : α} :
a = b a = b
theorem WithZero.cases_on {α : Type u} {P : Prop} (x : ) :
P 0((a : α) → P a) → P x
theorem WithOne.cases_on {α : Type u} {P : Prop} (x : ) :
P 1((a : α) → P a) → P x
def WithZero.addZeroClass.proof_2 {α : Type u_1} [inst : Add α] (a : ) :
Option.liftOrGet (fun x x_1 => x + x_1) a none = a
Equations
def WithZero.addZeroClass.proof_1 {α : Type u_1} [inst : Add α] (a : ) :
Option.liftOrGet (fun x x_1 => x + x_1) none a = a
Equations
Equations
instance WithOne.mulOneClass {α : Type u} [inst : Mul α] :
Equations
def WithZero.addMonoid.proof_5 {α : Type u_1} [inst : ] :
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
Equations
• (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)
def WithZero.addMonoid.proof_4 {α : Type u_1} [inst : ] :
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x
Equations
• (_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)
instance WithZero.addMonoid {α : Type u} [inst : ] :
Equations
• WithZero.addMonoid = let src := WithZero.addZeroClass; AddMonoid.mk (_ : ∀ (a : ), 0 + a = a) (_ : ∀ (a : ), a + 0 = a) nsmulRec
def WithZero.addMonoid.proof_1 {α : Type u_1} [inst : ] (a : ) (b : ) (c : ) :
Option.liftOrGet (fun x x_1 => x + x_1) (Option.liftOrGet (fun x x_1 => x + x_1) a b) c = Option.liftOrGet (fun x x_1 => x + x_1) a (Option.liftOrGet (fun x x_1 => x + x_1) b c)
Equations
• One or more equations did not get rendered due to their size.
def WithZero.addMonoid.proof_3 {α : Type u_1} [inst : ] (a : ) :
a + 0 = a
Equations
• (_ : ∀ (a : ), a + 0 = a) = (_ : ∀ (a : ), a + 0 = a)
def WithZero.addMonoid.proof_2 {α : Type u_1} [inst : ] (a : ) :
0 + a = a
Equations
• (_ : ∀ (a : ), 0 + a = a) = (_ : ∀ (a : ), 0 + a = a)
instance WithOne.monoid {α : Type u} [inst : ] :
Equations
• WithOne.monoid = let src := WithOne.mulOneClass; Monoid.mk (_ : ∀ (a : ), 1 * a = a) (_ : ∀ (a : ), a * 1 = a) npowRec
def WithZero.addCommMonoid.proof_4 {α : Type u_1} [inst : ] (n : ) (x : ) :
AddMonoid.nsmul (n + 1) x = x +
Equations
def WithZero.addCommMonoid.proof_2 {α : Type u_1} [inst : ] (a : ) :
a + 0 = a
Equations
• (_ : ∀ (a : ), a + 0 = a) = (_ : ∀ (a : ), a + 0 = a)
def WithZero.addCommMonoid.proof_1 {α : Type u_1} [inst : ] (a : ) :
0 + a = a
Equations
• (_ : ∀ (a : ), 0 + a = a) = (_ : ∀ (a : ), 0 + a = a)
def WithZero.addCommMonoid.proof_5 {α : Type u_1} [inst : ] (a : ) (b : ) :
Option.liftOrGet (fun x x_1 => x + x_1) a b = Option.liftOrGet (fun x x_1 => x + x_1) b a
Equations
• One or more equations did not get rendered due to their size.
instance WithZero.addCommMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def WithZero.addCommMonoid.proof_3 {α : Type u_1} [inst : ] (x : ) :
= 0
Equations
• (_ : ∀ (x : ), = 0) = (_ : ∀ (x : ), = 0)
instance WithOne.commMonoid {α : Type u} [inst : ] :
Equations
@[simp]
theorem WithZero.coe_add {α : Type u} [inst : Add α] (a : α) (b : α) :
↑(a + b) = a + b
@[simp]
theorem WithOne.coe_mul {α : Type u} [inst : Mul α] (a : α) (b : α) :
↑(a * b) = a * b
@[simp]
theorem WithZero.coe_neg {α : Type u} [inst : Neg α] (a : α) :
↑(-a) = -a
@[simp]
theorem WithOne.coe_inv {α : Type u} [inst : Inv α] (a : α) :
a⁻¹ = (a)⁻¹
instance WithZero.one {α : Type u} [one : One α] :
One ()
Equations
• WithZero.one = { one := One.one }
@[simp]
theorem WithZero.coe_one {α : Type u} [inst : One α] :
1 = 1
instance WithZero.mulZeroClass {α : Type u} [inst : Mul α] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithZero.coe_mul {α : Type u} [inst : Mul α] {a : α} {b : α} :
↑(a * b) = a * b
instance WithZero.noZeroDivisors {α : Type u} [inst : Mul α] :
Equations
instance WithZero.semigroupWithZero {α : Type u} [inst : ] :
Equations
• WithZero.semigroupWithZero = let src := WithZero.mulZeroClass; SemigroupWithZero.mk (_ : ∀ (a : ), 0 * a = 0) (_ : ∀ (a : ), a * 0 = 0)
instance WithZero.commSemigroup {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance WithZero.mulZeroOneClass {α : Type u} [inst : ] :
Equations
• WithZero.mulZeroOneClass = let src := WithZero.mulZeroClass; let src_1 := WithZero.one; MulZeroOneClass.mk (_ : ∀ (a : ), 0 * a = 0) (_ : ∀ (a : ), a * 0 = 0)
instance WithZero.pow {α : Type u} [inst : One α] [inst : Pow α ] :
Pow ()
Equations
• WithZero.pow = { pow := fun x n => match x, n with | none, 0 => 1 | none, => 0 | some x, n => ↑(x ^ n) }
@[simp]
theorem WithZero.coe_pow {α : Type u} [inst : One α] [inst : Pow α ] {a : α} (n : ) :
↑(a ^ n) = a ^ n
instance WithZero.monoidWithZero {α : Type u} [inst : ] :
Equations
• WithZero.monoidWithZero = let src := WithZero.mulZeroOneClass; let src_1 := WithZero.semigroupWithZero; MonoidWithZero.mk (_ : ∀ (a : ), 0 * a = 0) (_ : ∀ (a : ), a * 0 = 0)
instance WithZero.commMonoidWithZero {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance WithZero.inv {α : Type u} [inst : Inv α] :
Inv ()

Given an inverse operation on α there is an inverse operation on WithZero α sending 0 to 0.

Equations
• WithZero.inv = { inv := fun a => Option.map Inv.inv a }
@[simp]
theorem WithZero.coe_inv {α : Type u} [inst : Inv α] (a : α) :
a⁻¹ = (a)⁻¹
@[simp]
theorem WithZero.inv_zero {α : Type u} [inst : Inv α] :
0⁻¹ = 0
instance WithZero.involutiveInv {α : Type u} [inst : ] :
Equations
instance WithZero.invOneClass {α : Type u} [inst : ] :
Equations
• WithZero.invOneClass = let src := WithZero.one; let src_1 := WithZero.inv; InvOneClass.mk (_ : 1⁻¹ = 1)
instance WithZero.div {α : Type u} [inst : Div α] :
Div ()
Equations
theorem WithZero.coe_div {α : Type u} [inst : Div α] (a : α) (b : α) :
↑(a / b) = a / b
instance WithZero.instPowWithZeroInt {α : Type u} [inst : One α] [inst : Pow α ] :
Pow ()
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithZero.coe_zpow {α : Type u} [inst : ] {a : α} (n : ) :
↑(a ^ n) = a ^ n
instance WithZero.divInvMonoid {α : Type u} [inst : ] :
Equations
• WithZero.divInvMonoid = let src := WithZero.div; let src_1 := WithZero.inv; let src_2 := WithZero.monoidWithZero; DivInvMonoid.mk fun n x => x ^ n
instance WithZero.divInvOneMonoid {α : Type u} [inst : ] :
Equations
• WithZero.divInvOneMonoid = let src := WithZero.divInvMonoid; let src_1 := WithZero.invOneClass; DivInvOneMonoid.mk (_ : 1⁻¹ = 1)
instance WithZero.divisionMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance WithZero.divisionCommMonoid {α : Type u} [inst : ] :
Equations
• WithZero.divisionCommMonoid = let src := WithZero.divisionMonoid; let src_1 := WithZero.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : ), a * b = b * a)
instance WithZero.groupWithZero {α : Type u} [inst : ] :

if G is a group then WithZero G is a group with zero.

Equations
• One or more equations did not get rendered due to their size.
instance WithZero.commGroupWithZero {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance WithZero.addMonoidWithOne {α : Type u} [inst : ] :
Equations