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 Mathlib.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 Mathlib.Algebra.GroupWithZero.Basic)

Porting notes #

In Lean 3, we use id here and there to get correct types of proofs. This is required because WithOne and WithZero are marked as irreducible at the end of Mathlib.Algebra.Group.WithOne.Defs, so proofs that use Option α instead of WithOne α no longer typecheck. In Lean 4, both types are plain defs, so we don't need these ids.

TODO #

WithOne.coe_mul and WithZero.coe_mul have inconsistent use of implicit parameters

def WithZero (α : Type u_1) :

Type u_1

Add an extra element 0 to a type

Equations

WithZero α = Option α

Instances For

def WithOne (α : Type u_1) :

Type u_1

Add an extra element 1 to a type

Equations

WithOne α = Option α

Instances For

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

Repr (WithZero α)

Equations

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

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

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

Equations

WithZero.instRepr.match_1 motive o h_1 h_2 = Option.casesOn o (h_1 ()) fun (val : α) => h_2 val

Instances For

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

Repr (WithZero α)

Equations

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

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

Repr (WithOne α)

Equations

WithOne.instRepr = { reprPrec := fun (o : WithOne α) (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} [Add α] :

Add (WithZero α)

Equations

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

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

Mul (WithOne α)

Equations

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

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

Neg (WithZero α)

Equations

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

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

Inv (WithOne α)

Equations

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

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

NegZeroClass (WithZero α)

Equations

WithZero.negZeroClass = let __src := WithZero.zero; let __src_1 := WithZero.neg; NegZeroClass.mk ⋯

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

-0 = -0

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

InvOneClass (WithOne α)

Equations

WithOne.invOneClass = let __src := WithOne.one; let __src_1 := WithOne.inv; InvOneClass.mk ⋯

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} [Nonempty α] :

Nontrivial (WithZero α)

Equations

⋯ = ⋯

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

Nontrivial (WithOne α)

Equations

⋯ = ⋯

def WithZero.coe {α : Type u} :

α → WithZero α

The canonical map from α into WithZero α

Equations

WithZero.coe = some

Instances For

def WithOne.coe {α : Type u} :

α → WithOne α

The canonical map from α into WithOne α

Equations

WithOne.coe = some

Instances For

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.instRepr.match_1 (fun (x : WithZero α) => C x) x (fun (_ : Unit) => h₁) fun (x : α) => h₂ x

Instances For

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

Instances For

def WithZero.unzero {α : Type u} {x : WithZero α} :

x ≠ 0 → α

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

Equations

WithZero.unzero x = WithZero.unzero.match_1 (fun (x : WithZero α) (x : x ≠ 0) => α) x✝ x fun (x : α) (x_1 : ↑x ≠ 0) => x

Instances For

abbrev WithZero.unzero.match_1 {α : Type u_1} (motive : (x : WithZero α) → x ≠ 0 → Sort u_2) :

(x : WithZero α) → (x_1 : x ≠ 0) → ((x : α) → (x_2 : ↑x ≠ 0) → motive (some x) x_2) → motive x x_1

Equations

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

Instances For

def WithOne.unone {α : Type u} {x : WithOne α} :

x ≠ 1 → α

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

Equations

WithOne.unone x = match x✝, x with | some x, x_1 => x

Instances For

@[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

abbrev WithZero.coe_unzero.match_1 {α : Type u_1} (motive : (x : WithZero α) → x ≠ 0 → Prop) :

∀ (x : WithZero α) (x_1 : x ≠ 0), (∀ (x : α) (x_2 : ↑x ≠ 0), motive (some x) x_2) → motive x x_1

Equations

⋯ = ⋯

Instances For

@[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 : WithZero α) => a ≠ 0

Equations

⋯ = ⋯

instance WithOne.canLift {α : Type u} :

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

Equations

⋯ = ⋯

@[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

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

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

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

AddZeroClass (WithZero α)

Equations

WithZero.addZeroClass = AddZeroClass.mk ⋯ ⋯

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

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

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

MulOneClass (WithOne α)

Equations

WithOne.mulOneClass = MulOneClass.mk ⋯ ⋯

@[simp]

theorem WithZero.coe_add {α : Type u} [Add α] (a : α) (b : α) :

↑(a + b) = ↑a + ↑b

@[simp]

theorem WithOne.coe_mul {α : Type u} [Mul α] (a : α) (b : α) :

↑(a * b) = ↑a * ↑b

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

∀ (n : ℕ) (x : WithZero α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

abbrev WithZero.addMonoid.match_1 {α : Type u_1} (motive : WithZero α → WithZero α → WithZero α → Prop) :

∀ (a b c : WithZero α), (∀ (b c : WithZero α), motive none b c) → (∀ (a : α) (c : WithZero α), motive (some a) none c) → (∀ (a b : α), motive (some a) (some b) none) → (∀ (a b c : α), motive (some a) (some b) (some c)) → motive a b c

Equations

⋯ = ⋯

Instances For

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

0 + a = a

theorem WithZero.addMonoid.proof_4 {α : Type u_1} [AddSemigroup α] :

∀ (x : WithZero α), nsmulRec 0 x = nsmulRec 0 x

theorem WithZero.addMonoid.proof_3 {α : Type u_1} [AddSemigroup α] (a : WithZero α) :

a + 0 = a

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

a + b + c = a + (b + c)

instance WithZero.addMonoid {α : Type u} [AddSemigroup α] :

AddMonoid (WithZero α)

Equations

WithZero.addMonoid = let __spread.0 := WithZero.addZeroClass; AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

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

Monoid (WithOne α)

Equations

WithOne.monoid = let __spread.0 := WithOne.mulOneClass; Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

abbrev WithZero.addCommMonoid.match_1 {α : Type u_1} (motive : WithZero α → WithZero α → Prop) :

∀ (a b : WithZero α), (∀ (a b : α), motive (some a) (some b)) → (∀ (val : α), motive (some val) none) → (∀ (val : α), motive none (some val)) → (Unit → motive none none) → motive a b

Equations

⋯ = ⋯

Instances For

instance WithZero.addCommMonoid {α : Type u} [AddCommSemigroup α] :

AddCommMonoid (WithZero α)

Equations

WithZero.addCommMonoid = AddCommMonoid.mk ⋯

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

a + b = b + a

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

CommMonoid (WithOne α)

Equations

WithOne.commMonoid = CommMonoid.mk ⋯

@[simp]

theorem WithZero.coe_neg {α : Type u} [Neg α] (a : α) :

↑(-a) = -↑a

@[simp]

theorem WithOne.coe_inv {α : Type u} [Inv α] (a : α) :

↑a⁻¹ = (↑a)⁻¹