Documentation

Mathlib.Algebra.Group.WithOne.Defs

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

WithZero α = Option α

def WithOne (α : Type u_1) :

Type u_1

Add an extra element 1 to a type

Equations

WithOne α = Option α

instance WithOne.instReprWithZero {α : Type u} [inst : Repr α] :

Repr (WithZero α)

Equations

WithOne.instReprWithZero = { reprPrec := fun o x => match o with | none => Std.Format.text "0" | some a => Std.Format.text "↑" ++ repr a }

instance WithZero.instReprWithZero {α : Type u} [inst : Repr α] :

Repr (WithZero α)

Equations

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

abbrev WithZero.instReprWithZero.match_1 {α : Type u_1} (motive : WithZero α → Sort u_2) :

(o : WithZero α) → (Unit → motive none) → ((a : α) → motive (some a)) → motive o

Equations

WithZero.instReprWithZero.match_1 motive o h_1 h_2 = Option.casesOn o (h_1 ()) fun val => h_2 val

instance WithOne.instReprWithOne {α : Type u} [inst : Repr α] :

Repr (WithOne α)

Equations

WithOne.instReprWithOne = { reprPrec := fun o x => match o with | none => Std.Format.text "1" | some a => Std.Format.text "↑" ++ repr a }

instance WithZero.monad :

Equations

WithZero.monad = instMonadOption

instance WithOne.monad :

Equations

WithOne.monad = instMonadOption

instance WithZero.zero {α : Type u} :

Zero (WithZero α)

Equations

WithZero.zero = { zero := none }

instance WithOne.one {α : Type u} :

One (WithOne α)

Equations

WithOne.one = { one := none }

instance WithZero.add {α : Type u} [inst : Add α] :

Add (WithZero α)

Equations

WithZero.add = { add := Option.liftOrGet fun x x_1 => x + x_1 }

instance WithOne.mul {α : Type u} [inst : Mul α] :

Mul (WithOne α)

Equations

WithOne.mul = { mul := Option.liftOrGet fun x x_1 => x * x_1 }

instance WithZero.neg {α : Type u} [inst : Neg α] :

Neg (WithZero α)

Equations

WithZero.neg = { neg := fun a => Option.map Neg.neg a }

instance WithOne.inv {α : Type u} [inst : Inv α] :

Inv (WithOne α)

Equations

WithOne.inv = { inv := fun a => Option.map Inv.inv a }

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

InvolutiveNeg (WithZero α)

Equations

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

def WithZero.involutiveNeg.proof_1 {α : Type u_1} [inst : InvolutiveNeg α] (a : WithZero α) :

Option.map Neg.neg (Option.map Neg.neg a) = a

Equations

(_ : Option.map Neg.neg (Option.map Neg.neg a) = a) = (_ : Option.map Neg.neg (Option.map Neg.neg a) = a)

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

InvolutiveInv (WithOne α)

Equations

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

def WithZero.negZeroClass.proof_1 {α : Type u_1} [inst : Neg α] :

-0 = -0

Equations

(_ : -0 = -0) = (_ : -0 = -0)

instance WithZero.negZeroClass {α : Type u} [inst : Neg α] :

NegZeroClass (WithZero α)

Equations

WithZero.negZeroClass = let src := WithZero.zero; let src_1 := WithZero.neg; NegZeroClass.mk (_ : -0 = -0)

instance WithOne.invOneClass {α : Type u} [inst : Inv α] :

InvOneClass (WithOne α)

Equations

WithOne.invOneClass = let src := WithOne.one; let src_1 := WithOne.inv; InvOneClass.mk (_ : 1⁻¹ = 1⁻¹)

instance WithZero.inhabited {α : Type u} :

Inhabited (WithZero α)

Equations

WithZero.inhabited = { default := 0 }

instance WithOne.inhabited {α : Type u} :

Inhabited (WithOne α)

Equations

WithOne.inhabited = { default := 1 }

instance WithZero.nontrivial {α : Type u} [inst : Nonempty α] :

Nontrivial (WithZero α)

Equations

@WithZero.nontrivial = @WithZero.nontrivial.proof_1

def WithZero.nontrivial.proof_1 {α : Type u_1} [inst : Nonempty α] :

Nontrivial (Option α)

Equations

(_ : Nontrivial (Option α)) = (_ : Nontrivial (Option α))

instance WithOne.nontrivial {α : Type u} [inst : Nonempty α] :

Nontrivial (WithOne α)

Equations

@WithOne.nontrivial = @WithOne.nontrivial.proof_1

def WithZero.coe {α : Type u} :

α → WithZero α

The canonical map from α into WithZero α

Equations

WithZero.coe = some

def WithOne.coe {α : Type u} :

α → WithOne α

The canonical map from α into WithOne α

Equations

WithOne.coe = some

instance WithZero.coeTC {α : Type u} :

CoeTC α (WithZero α)

Equations

WithZero.coeTC = { coe := WithZero.coe }

instance WithOne.coeTC {α : Type u} :

CoeTC α (WithOne α)

Equations

WithOne.coeTC = { coe := WithOne.coe }

def WithZero.recZeroCoe {α : Type u} {C : WithZero α → Sort u_1} (h₁ : C 0) (h₂ : (a : α) → C ↑a) (n : WithZero α) :

C n

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

Equations

WithZero.recZeroCoe h₁ h₂ x = WithZero.instReprWithZero.match_1 (fun x => C x) x (fun _ => h₁) fun x => h₂ x

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

C n

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

Equations

WithOne.recOneCoe h₁ h₂ x = match x with | none => h₁ | some x => h₂ x

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

α

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

Equations

WithZero.unzero hx = WithBot.unbot x hx

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

α

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

Equations

WithOne.unone hx = WithBot.unbot x hx

@[simp]

theorem WithZero.unzero_coe {α : Type u} {x : α} (hx : ↑x ≠ 0) :

WithZero.unzero hx = x

@[simp]

theorem WithOne.unone_coe {α : Type u} {x : α} (hx : ↑x ≠ 1) :

WithOne.unone hx = x

@[simp]

theorem WithZero.coe_unzero {α : Type u} {x : WithZero α} (hx : x ≠ 0) :

↑(WithZero.unzero hx) = x

@[simp]

theorem WithOne.coe_unone {α : Type u} {x : WithOne α} (hx : x ≠ 1) :

↑(WithOne.unone hx) = 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 : WithZero α} :

x ≠ 0 ↔ ∃ a, ↑a = x

theorem WithOne.ne_one_iff_exists {α : Type u} {x : WithOne α} :

x ≠ 1 ↔ ∃ a, ↑a = x

instance WithZero.canLift {α : Type u} :

CanLift (WithZero α) α WithZero.coe fun a => a ≠ 0

Equations

WithZero.canLift = { prf := (_ : ∀ (x : WithZero α), x ≠ 0 → ∃ a, ↑a = x) }

def WithZero.canLift.proof_1 {α : Type u_1} :

∀ (x : WithZero α), x ≠ 0 → ∃ a, ↑a = x

Equations

(_ : x ≠ 0 → ∃ a, ↑a = x) = (_ : x ≠ 0 → ∃ a, ↑a = x)

instance WithOne.canLift {α : Type u} :

CanLift (WithOne α) α WithOne.coe fun a => a ≠ 1

Equations

WithOne.canLift = { prf := (_ : ∀ (x : WithOne α), x ≠ 1 → ∃ a, ↑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 : WithZero α → Prop} (x : WithZero α) :

P 0 → ((a : α) → P ↑a) → P x

theorem WithOne.cases_on {α : Type u} {P : WithOne α → Prop} (x : WithOne α) :

P 1 → ((a : α) → P ↑a) → P x

def WithZero.addZeroClass.proof_2 {α : Type u_1} [inst : Add α] (a : Option α) :

Option.liftOrGet (fun x x_1 => x + x_1) a none = a

Equations

(_ : ∀ (a : Option α), Option.liftOrGet (fun x x_1 => x + x_1) a none = a) = (_ : ∀ (a : Option α), Option.liftOrGet (fun x x_1 => x + x_1) a none = a)

def WithZero.addZeroClass.proof_1 {α : Type u_1} [inst : Add α] (a : Option α) :

Option.liftOrGet (fun x x_1 => x + x_1) none a = a

Equations

(_ : ∀ (a : Option α), Option.liftOrGet (fun x x_1 => x + x_1) none a = a) = (_ : ∀ (a : Option α), Option.liftOrGet (fun x x_1 => x + x_1) none a = a)

instance WithZero.addZeroClass {α : Type u} [inst : Add α] :

AddZeroClass (WithZero α)

Equations

WithZero.addZeroClass = AddZeroClass.mk (_ : ∀ (a : Option α), Option.liftOrGet (fun x x_1 => x + x_1) none a = a) (_ : ∀ (a : Option α), Option.liftOrGet (fun x x_1 => x + x_1) a none = a)

instance WithOne.mulOneClass {α : Type u} [inst : Mul α] :

MulOneClass (WithOne α)

Equations

WithOne.mulOneClass = MulOneClass.mk (_ : ∀ (a : Option α), Option.liftOrGet (fun x x_1 => x * x_1) none a = a) (_ : ∀ (a : Option α), Option.liftOrGet (fun x x_1 => x * x_1) a none = a)

def WithZero.addMonoid.proof_5 {α : Type u_1} [inst : AddSemigroup α] :

∀ (n : ℕ) (x : WithZero α), 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 : AddSemigroup α] :

∀ (x : WithZero α), 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 : AddSemigroup α] :

AddMonoid (WithZero α)

Equations

WithZero.addMonoid = let src := WithZero.addZeroClass; AddMonoid.mk (_ : ∀ (a : WithZero α), 0 + a = a) (_ : ∀ (a : WithZero α), a + 0 = a) nsmulRec

def WithZero.addMonoid.proof_1 {α : Type u_1} [inst : AddSemigroup α] (a : Option α) (b : Option α) (c : Option α) :

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 : AddSemigroup α] (a : WithZero α) :

a + 0 = a

Equations

(_ : ∀ (a : WithZero α), a + 0 = a) = (_ : ∀ (a : WithZero α), a + 0 = a)

def WithZero.addMonoid.proof_2 {α : Type u_1} [inst : AddSemigroup α] (a : WithZero α) :

0 + a = a

Equations

(_ : ∀ (a : WithZero α), 0 + a = a) = (_ : ∀ (a : WithZero α), 0 + a = a)

instance WithOne.monoid {α : Type u} [inst : Semigroup α] :

Monoid (WithOne α)

Equations

WithOne.monoid = let src := WithOne.mulOneClass; Monoid.mk (_ : ∀ (a : WithOne α), 1 * a = a) (_ : ∀ (a : WithOne α), a * 1 = a) npowRec

def WithZero.addCommMonoid.proof_4 {α : Type u_1} [inst : AddCommSemigroup α] (n : ℕ) (x : WithZero α) :

AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

(_ : ∀ (n : ℕ) (x : WithZero α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : WithZero α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

def WithZero.addCommMonoid.proof_2 {α : Type u_1} [inst : AddCommSemigroup α] (a : WithZero α) :

a + 0 = a

Equations

(_ : ∀ (a : WithZero α), a + 0 = a) = (_ : ∀ (a : WithZero α), a + 0 = a)

def WithZero.addCommMonoid.proof_1 {α : Type u_1} [inst : AddCommSemigroup α] (a : WithZero α) :

0 + a = a

Equations

(_ : ∀ (a : WithZero α), 0 + a = a) = (_ : ∀ (a : WithZero α), 0 + a = a)

def WithZero.addCommMonoid.proof_5 {α : Type u_1} [inst : AddCommSemigroup α] (a : Option α) (b : Option α) :

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 : AddCommSemigroup α] :

AddCommMonoid (WithZero α)

Equations

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

def WithZero.addCommMonoid.proof_3 {α : Type u_1} [inst : AddCommSemigroup α] (x : WithZero α) :

AddMonoid.nsmul 0 x = 0

Equations

(_ : ∀ (x : WithZero α), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : WithZero α), AddMonoid.nsmul 0 x = 0)

instance WithOne.commMonoid {α : Type u} [inst : CommSemigroup α] :

CommMonoid (WithOne α)

Equations

WithOne.commMonoid = let src := WithOne.monoid; CommMonoid.mk (_ : ∀ (a b : Option α), Option.liftOrGet (fun x x_1 => x * x_1) a b = Option.liftOrGet (fun x x_1 => x * x_1) b a)

@[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 (WithZero α)

Equations

WithZero.one = { one := ↑One.one }

@[simp]

theorem WithZero.coe_one {α : Type u} [inst : One α] :

↑1 = 1

instance WithZero.mulZeroClass {α : Type u} [inst : Mul α] :

MulZeroClass (WithZero α)

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 α] :

NoZeroDivisors (WithZero α)

Equations

@WithZero.noZeroDivisors = @WithZero.noZeroDivisors.proof_1

instance WithZero.semigroupWithZero {α : Type u} [inst : Semigroup α] :

SemigroupWithZero (WithZero α)

Equations

WithZero.semigroupWithZero = let src := WithZero.mulZeroClass; SemigroupWithZero.mk (_ : ∀ (a : WithZero α), 0 * a = 0) (_ : ∀ (a : WithZero α), a * 0 = 0)

instance WithZero.commSemigroup {α : Type u} [inst : CommSemigroup α] :

CommSemigroup (WithZero α)

Equations

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

instance WithZero.mulZeroOneClass {α : Type u} [inst : MulOneClass α] :

MulZeroOneClass (WithZero α)

Equations

WithZero.mulZeroOneClass = let src := WithZero.mulZeroClass; let src_1 := WithZero.one; MulZeroOneClass.mk (_ : ∀ (a : WithZero α), 0 * a = 0) (_ : ∀ (a : WithZero α), a * 0 = 0)

instance WithZero.pow {α : Type u} [inst : One α] [inst : Pow α ℕ] :

Pow (WithZero α) ℕ

Equations

WithZero.pow = { pow := fun x n => match x, n with | none, 0 => 1 | none, Nat.succ n => 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 : Monoid α] :

MonoidWithZero (WithZero α)

Equations

WithZero.monoidWithZero = let src := WithZero.mulZeroOneClass; let src_1 := WithZero.semigroupWithZero; MonoidWithZero.mk (_ : ∀ (a : WithZero α), 0 * a = 0) (_ : ∀ (a : WithZero α), a * 0 = 0)

instance WithZero.commMonoidWithZero {α : Type u} [inst : CommMonoid α] :

CommMonoidWithZero (WithZero α)

Equations

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

instance WithZero.inv {α : Type u} [inst : Inv α] :

Inv (WithZero α)

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 α] :

instance WithZero.involutiveInv {α : Type u} [inst : 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.invOneClass {α : Type u} [inst : InvOneClass α] :

InvOneClass (WithZero α)

Equations

WithZero.invOneClass = let src := WithZero.one; let src_1 := WithZero.inv; InvOneClass.mk (_ : ↑1⁻¹ = 1)

instance WithZero.div {α : Type u} [inst : Div α] :

Div (WithZero α)

Equations

WithZero.div = { div := Option.map₂ fun x x_1 => x / x_1 }

theorem WithZero.coe_div {α : Type u} [inst : Div α] (a : α) (b : α) :

↑(a / b) = ↑a / ↑b

instance WithZero.instPowWithZeroInt {α : Type u} [inst : One α] [inst : Pow α ℤ] :

Pow (WithZero α) ℤ

Equations

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

@[simp]

theorem WithZero.coe_zpow {α : Type u} [inst : DivInvMonoid α] {a : α} (n : ℤ) :

↑(a ^ n) = ↑a ^ n

instance WithZero.divInvMonoid {α : Type u} [inst : DivInvMonoid α] :

DivInvMonoid (WithZero α)

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 : DivInvOneMonoid α] :

DivInvOneMonoid (WithZero α)

Equations

WithZero.divInvOneMonoid = let src := WithZero.divInvMonoid; let src_1 := WithZero.invOneClass; DivInvOneMonoid.mk (_ : 1⁻¹ = 1)

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

DivisionMonoid (WithZero α)

Equations

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

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

DivisionCommMonoid (WithZero α)

Equations

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

instance WithZero.groupWithZero {α : Type u} [inst : Group α] :

GroupWithZero (WithZero α)

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 : CommGroup α] :

CommGroupWithZero (WithZero α)

Equations

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

instance WithZero.addMonoidWithOne {α : Type u} [inst : AddMonoidWithOne α] :

AddMonoidWithOne (WithZero α)

Equations

WithZero.addMonoidWithOne = let src := WithZero.addMonoid; let src_1 := WithZero.one; AddMonoidWithOne.mk

instance WithZero.semiring {α : Type u} [inst : Semiring α] :

Semiring (WithZero α)

Equations

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