algebra.free - mathlib3 docs

def free_magma.rec_on_mul {α : Type u} {C : free_magma α → Sort l} (x : free_magma α) (ih1 : Π (x : α), C (free_magma.of x)) (ih2 : Π (x y : free_magma α), C x → C y → C (x * y)) :

C x

Recursor for free_magma using x * y instead of free_magma.mul x y.

Equations

x.rec_on_mul ih1 ih2 = x.rec_on ih1 ih2

source

@[ext]

theorem free_add_magma.hom_ext {α : Type u} {β : Type v} [has_add β] {f g : add_hom (free_add_magma α) β} (h : ⇑f ∘ free_add_magma.of = ⇑g ∘ free_add_magma.of) :

f = g

source

@[ext]

theorem free_magma.hom_ext {α : Type u} {β : Type v} [has_mul β] {f g : free_magma α →ₙ* β} (h : ⇑f ∘ free_magma.of = ⇑g ∘ free_magma.of) :

f = g

source

def free_magma.lift_aux {α : Type u} {β : Type v} [has_mul β] (f : α → β) :

free_magma α → β

Lifts a function α → β to a magma homomorphism free_magma α → β given a magma β.

Equations

free_magma.lift_aux f (x * y) = free_magma.lift_aux f x * free_magma.lift_aux f y
free_magma.lift_aux f (free_magma.of x) = f x

source

def free_add_magma.lift_aux {α : Type u} {β : Type v} [has_add β] (f : α → β) :

free_add_magma α → β

Lifts a function α → β to an additive magma homomorphism free_add_magma α → β given an additive magma β.

Equations

free_add_magma.lift_aux f (x + y) = free_add_magma.lift_aux f x + free_add_magma.lift_aux f y
free_add_magma.lift_aux f (free_add_magma.of x) = f x

source

@[simp]

theorem free_add_magma.lift_symm_apply {α : Type u} {β : Type v} [has_add β] (F : add_hom (free_add_magma α) β) (ᾰ : α) :

⇑(free_add_magma.lift.symm) F ᾰ = (⇑F ∘ free_add_magma.of) ᾰ

source

@[simp]

theorem free_magma.lift_symm_apply {α : Type u} {β : Type v} [has_mul β] (F : free_magma α →ₙ* β) (ᾰ : α) :

⇑(free_magma.lift.symm) F ᾰ = (⇑F ∘ free_magma.of) ᾰ

source

def free_add_magma.lift {α : Type u} {β : Type v} [has_add β] :

(α → β) ≃ add_hom (free_add_magma α) β

The universal property of the free additive magma expressing its adjointness.

Equations

free_add_magma.lift = {to_fun := λ (f : α → β), {to_fun := free_add_magma.lift_aux f, map_add' := _}, inv_fun := λ (F : add_hom (free_add_magma α) β), ⇑F ∘ free_add_magma.of, left_inv := _, right_inv := _}

source

def free_magma.lift {α : Type u} {β : Type v} [has_mul β] :

(α → β) ≃ (free_magma α →ₙ* β)

The universal property of the free magma expressing its adjointness.

Equations

free_magma.lift = {to_fun := λ (f : α → β), {to_fun := free_magma.lift_aux f, map_mul' := _}, inv_fun := λ (F : free_magma α →ₙ* β), ⇑F ∘ free_magma.of, left_inv := _, right_inv := _}

source

@[simp]

theorem free_add_magma.lift_of {α : Type u} {β : Type v} [has_add β] (f : α → β) (x : α) :

⇑(⇑free_add_magma.lift f) (free_add_magma.of x) = f x

source

@[simp]

theorem free_magma.lift_of {α : Type u} {β : Type v} [has_mul β] (f : α → β) (x : α) :

⇑(⇑free_magma.lift f) (free_magma.of x) = f x

source

@[simp]

theorem free_magma.lift_comp_of {α : Type u} {β : Type v} [has_mul β] (f : α → β) :

⇑(⇑free_magma.lift f) ∘ free_magma.of = f

source

@[simp]

theorem free_add_magma.lift_comp_of {α : Type u} {β : Type v} [has_add β] (f : α → β) :

⇑(⇑free_add_magma.lift f) ∘ free_add_magma.of = f

source

@[simp]

theorem free_add_magma.lift_comp_of' {α : Type u} {β : Type v} [has_add β] (f : add_hom (free_add_magma α) β) :

⇑free_add_magma.lift (⇑f ∘ free_add_magma.of) = f

source

@[simp]

theorem free_magma.lift_comp_of' {α : Type u} {β : Type v} [has_mul β] (f : free_magma α →ₙ* β) :

⇑free_magma.lift (⇑f ∘ free_magma.of) = f

source

def free_add_magma.map {α : Type u} {β : Type v} (f : α → β) :

add_hom (free_add_magma α) (free_add_magma β)

The unique additive magma homomorphism free_add_magma α → free_add_magma β that sends each of x to of (f x).

Equations

free_add_magma.map f = ⇑free_add_magma.lift (free_add_magma.of ∘ f)

source

def free_magma.map {α : Type u} {β : Type v} (f : α → β) :

free_magma α →ₙ* free_magma β

The unique magma homomorphism free_magma α →ₙ* free_magma β that sends each of x to of (f x).

Equations

free_magma.map f = ⇑free_magma.lift (free_magma.of ∘ f)

source

@[simp]

theorem free_add_magma.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :

⇑(free_add_magma.map f) (free_add_magma.of x) = free_add_magma.of (f x)

source

@[simp]

theorem free_magma.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :

⇑(free_magma.map f) (free_magma.of x) = free_magma.of (f x)

source

@[protected, instance]

def free_add_magma.monad :

monad free_add_magma

Equations

free_add_magma.monad = monad.mk

source

@[protected, instance]

def free_magma.monad :

monad free_magma

Equations

free_magma.monad = monad.mk

source

@[protected]

def free_add_magma.rec_on_pure {α : Type u} {C : free_add_magma α → Sort l} (x : free_add_magma α) (ih1 : Π (x : α), C (has_pure.pure x)) (ih2 : Π (x y : free_add_magma α), C x → C y → C (x + y)) :

C x

Recursor on free_add_magma using pure instead of of.

Equations

x.rec_on_pure ih1 ih2 = x.rec_on_add ih1 ih2

source

@[protected]

def free_magma.rec_on_pure {α : Type u} {C : free_magma α → Sort l} (x : free_magma α) (ih1 : Π (x : α), C (has_pure.pure x)) (ih2 : Π (x y : free_magma α), C x → C y → C (x * y)) :

C x

Recursor on free_magma using pure instead of of.

Equations

x.rec_on_pure ih1 ih2 = x.rec_on_mul ih1 ih2

source

@[simp]

theorem free_magma.map_pure {α β : Type u} (f : α → β) (x : α) :

f <$> has_pure.pure x = has_pure.pure (f x)

source

@[simp]

theorem free_add_magma.map_pure {α β : Type u} (f : α → β) (x : α) :

f <$> has_pure.pure x = has_pure.pure (f x)

source

@[simp]

theorem free_magma.map_mul' {α β : Type u} (f : α → β) (x y : free_magma α) :

f <$> (x * y) = f <$> x * f <$> y

source

@[simp]

theorem free_add_magma.map_add' {α β : Type u} (f : α → β) (x y : free_add_magma α) :

f <$> (x + y) = f <$> x + f <$> y

source

@[simp]

theorem free_add_magma.pure_bind {α β : Type u} (f : α → free_add_magma β) (x : α) :

has_pure.pure x >>= f = f x

source

@[simp]

theorem free_magma.pure_bind {α β : Type u} (f : α → free_magma β) (x : α) :

has_pure.pure x >>= f = f x

source

@[simp]

theorem free_add_magma.add_bind {α β : Type u} (f : α → free_add_magma β) (x y : free_add_magma α) :

x + y >>= f = (x >>= f) + (y >>= f)

source

@[simp]

theorem free_magma.mul_bind {α β : Type u} (f : α → free_magma β) (x y : free_magma α) :

x * y >>= f = (x >>= f) * (y >>= f)

source

@[simp]

theorem free_add_magma.pure_seq {α β : Type u} {f : α → β} {x : free_add_magma α} :

has_pure.pure f <*> x = f <$> x

source

@[simp]

theorem free_magma.pure_seq {α β : Type u} {f : α → β} {x : free_magma α} :

has_pure.pure f <*> x = f <$> x

source

@[simp]

theorem free_add_magma.add_seq {α β : Type u} {f g : free_add_magma (α → β)} {x : free_add_magma α} :

f + g <*> x = (f <*> x) + (g <*> x)

source

@[simp]

theorem free_magma.mul_seq {α β : Type u} {f g : free_magma (α → β)} {x : free_magma α} :

f * g <*> x = (f <*> x) * (g <*> x)

source

@[protected, instance]

def free_add_magma.is_lawful_monad :

is_lawful_monad free_add_magma

source

@[protected, instance]

def free_magma.is_lawful_monad :

is_lawful_monad free_magma

source

@[protected]

def free_magma.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) :

free_magma α → m (free_magma β)

free_magma is traversable.

Equations

free_magma.traverse F (x * y) = has_mul.mul <$> free_magma.traverse F x <*> free_magma.traverse F y
free_magma.traverse F (free_magma.of x) = free_magma.of <$> F x

source

@[protected]

def free_add_magma.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) :

free_add_magma α → m (free_add_magma β)

free_add_magma is traversable.

Equations

free_add_magma.traverse F (x + y) = has_add.add <$> free_add_magma.traverse F x <*> free_add_magma.traverse F y
free_add_magma.traverse F (free_add_magma.of x) = free_add_magma.of <$> F x

source

@[protected, instance]

def free_magma.traversable :

traversable free_magma

Equations

free_magma.traversable = {to_functor := applicative.to_functor monad.to_applicative, traverse := free_magma.traverse}

source

@[protected, instance]

def free_add_magma.traversable :

traversable free_add_magma

Equations

free_add_magma.traversable = {to_functor := applicative.to_functor monad.to_applicative, traverse := free_add_magma.traverse}

source

@[simp]

theorem free_magma.traverse_pure {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : α) :

traversable.traverse F (has_pure.pure x) = has_pure.pure <$> F x

source

@[simp]

theorem free_add_magma.traverse_pure {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : α) :

traversable.traverse F (has_pure.pure x) = has_pure.pure <$> F x

source

@[simp]

theorem free_add_magma.traverse_pure' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :

traversable.traverse F ∘ has_pure.pure = λ (x : α), has_pure.pure <$> F x

source

@[simp]

theorem free_magma.traverse_pure' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :

traversable.traverse F ∘ has_pure.pure = λ (x : α), has_pure.pure <$> F x

source

@[simp]

theorem free_add_magma.traverse_add {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x y : free_add_magma α) :

traversable.traverse F (x + y) = has_add.add <$> traversable.traverse F x <*> traversable.traverse F y

source

@[simp]

theorem free_magma.traverse_mul {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x y : free_magma α) :

traversable.traverse F (x * y) = has_mul.mul <$> traversable.traverse F x <*> traversable.traverse F y

source

@[simp]

theorem free_magma.traverse_mul' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :

function.comp (traversable.traverse F) ∘ has_mul.mul = λ (x y : free_magma α), has_mul.mul <$> traversable.traverse F x <*> traversable.traverse F y

source

@[simp]

theorem free_add_magma.traverse_add' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :

function.comp (traversable.traverse F) ∘ has_add.add = λ (x y : free_add_magma α), has_add.add <$> traversable.traverse F x <*> traversable.traverse F y

source

@[simp]

theorem free_magma.traverse_eq {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : free_magma α) :

free_magma.traverse F x = traversable.traverse F x

source

@[simp]

theorem free_add_magma.traverse_eq {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : free_add_magma α) :

free_add_magma.traverse F x = traversable.traverse F x

source

@[simp]

theorem free_add_magma.add_map_seq {α : Type u} (x y : free_add_magma α) :

has_add.add <$> x <*> y = x + y

source

@[simp]

theorem free_magma.mul_map_seq {α : Type u} (x y : free_magma α) :

has_mul.mul <$> x <*> y = x * y

source

@[protected, instance]

def free_magma.is_lawful_traversable :

is_lawful_traversable free_magma

Equations

free_magma.is_lawful_traversable = {to_is_lawful_functor := free_magma.is_lawful_traversable._proof_1, id_traverse := free_magma.is_lawful_traversable._proof_2, comp_traverse := free_magma.is_lawful_traversable._proof_3, traverse_eq_map_id := free_magma.is_lawful_traversable._proof_4, naturality := free_magma.is_lawful_traversable._proof_5}

source

@[protected, instance]

def free_add_magma.is_lawful_traversable :

is_lawful_traversable free_add_magma

Equations

free_add_magma.is_lawful_traversable = {to_is_lawful_functor := free_add_magma.is_lawful_traversable._proof_1, id_traverse := free_add_magma.is_lawful_traversable._proof_2, comp_traverse := free_add_magma.is_lawful_traversable._proof_3, traverse_eq_map_id := free_add_magma.is_lawful_traversable._proof_4, naturality := free_add_magma.is_lawful_traversable._proof_5}

source

@[protected]

def free_magma.repr {α : Type u} [has_repr α] :

free_magma α → string

Representation of an element of a free magma.

Equations

(x * y).repr = "( " ++ x.repr ++ " * " ++ y.repr ++ " )"
(free_magma.of x).repr = repr x

source

@[protected]

def free_add_magma.repr {α : Type u} [has_repr α] :

free_add_magma α → string

Representation of an element of a free additive magma.

Equations

(x + y).repr = "( " ++ x.repr ++ " + " ++ y.repr ++ " )"
(free_add_magma.of x).repr = repr x

source

@[protected, instance]

def free_magma.has_repr {α : Type u} [has_repr α] :

has_repr (free_magma α)

Equations

free_magma.has_repr = {repr := free_magma.repr _inst_1}

source

@[protected, instance]

def free_add_magma.has_repr {α : Type u} [has_repr α] :

has_repr (free_add_magma α)

Equations

free_add_magma.has_repr = {repr := free_add_magma.repr _inst_1}

source

@[simp]

def free_magma.length {α : Type u} :

free_magma α → ℕ

Length of an element of a free magma.

Equations

(x * y).length = x.length + y.length
(free_magma.of x).length = 1

source

@[simp]

def free_add_magma.length {α : Type u} :

free_add_magma α → ℕ

Length of an element of a free additive magma.

Equations

(x + y).length = x.length + y.length
(free_add_magma.of x).length = 1

source

inductive add_magma.assoc_rel (α : Type u) [has_add α] :

α → α → Prop

intro : ∀ {α : Type u} [_inst_1 : has_add α] (x y z : α), add_magma.assoc_rel α (x + y + z) (x + (y + z))
left : ∀ {α : Type u} [_inst_1 : has_add α] (w x y z : α), add_magma.assoc_rel α (w + (x + y + z)) (w + (x + (y + z)))

Associativity relations for an additive magma.

source

inductive magma.assoc_rel (α : Type u) [has_mul α] :

α → α → Prop

intro : ∀ {α : Type u} [_inst_1 : has_mul α] (x y z : α), magma.assoc_rel α (x * y * z) (x * (y * z))
left : ∀ {α : Type u} [_inst_1 : has_mul α] (w x y z : α), magma.assoc_rel α (w * (x * y * z)) (w * (x * (y * z)))

Associativity relations for a magma.

source

def magma.assoc_quotient (α : Type u) [has_mul α] :

Type u

Semigroup quotient of a magma.

Equations

magma.assoc_quotient α = quot (magma.assoc_rel α)

Instances for magma.assoc_quotient

source

def add_magma.free_add_semigroup (α : Type u) [has_add α] :

Type u

Additive semigroup quotient of an additive magma.

Equations

add_magma.free_add_semigroup α = quot (add_magma.assoc_rel α)

Instances for add_magma.free_add_semigroup

source

theorem add_magma.free_add_semigroup.quot_mk_assoc {α : Type u} [has_add α] (x y z : α) :

quot.mk (add_magma.assoc_rel α) (x + y + z) = quot.mk (add_magma.assoc_rel α) (x + (y + z))

source

theorem magma.assoc_quotient.quot_mk_assoc {α : Type u} [has_mul α] (x y z : α) :

quot.mk (magma.assoc_rel α) (x * y * z) = quot.mk (magma.assoc_rel α) (x * (y * z))

source

theorem magma.assoc_quotient.quot_mk_assoc_left {α : Type u} [has_mul α] (x y z w : α) :

quot.mk (magma.assoc_rel α) (x * (y * z * w)) = quot.mk (magma.assoc_rel α) (x * (y * (z * w)))

source

theorem add_magma.free_add_semigroup.quot_mk_assoc_left {α : Type u} [has_add α] (x y z w : α) :

quot.mk (add_magma.assoc_rel α) (x + (y + z + w)) = quot.mk (add_magma.assoc_rel α) (x + (y + (z + w)))

source

@[protected, instance]

def add_magma.free_add_semigroup.add_semigroup {α : Type u} [has_add α] :

add_semigroup (add_magma.free_add_semigroup α)

Equations

add_magma.free_add_semigroup.add_semigroup = {add := λ (x y : add_magma.free_add_semigroup α), quot.lift_on₂ x y (λ (x y : α), quot.mk (add_magma.assoc_rel α) (x + y)) add_magma.free_add_semigroup.add_semigroup._proof_1 add_magma.free_add_semigroup.add_semigroup._proof_2, add_assoc := _}

source

@[protected, instance]

def magma.assoc_quotient.semigroup {α : Type u} [has_mul α] :

semigroup (magma.assoc_quotient α)

Equations

magma.assoc_quotient.semigroup = {mul := λ (x y : magma.assoc_quotient α), quot.lift_on₂ x y (λ (x y : α), quot.mk (magma.assoc_rel α) (x * y)) magma.assoc_quotient.semigroup._proof_1 magma.assoc_quotient.semigroup._proof_2, mul_assoc := _}

source

def magma.assoc_quotient.of {α : Type u} [has_mul α] :

α →ₙ* magma.assoc_quotient α

Embedding from magma to its free semigroup.

Equations

magma.assoc_quotient.of = {to_fun := quot.mk (magma.assoc_rel α), map_mul' := _}

source

def add_magma.free_add_semigroup.of {α : Type u} [has_add α] :

add_hom α (add_magma.free_add_semigroup α)

Embedding from additive magma to its free additive semigroup.

Equations

add_magma.free_add_semigroup.of = {to_fun := quot.mk (add_magma.assoc_rel α), map_add' := _}

source

@[protected, instance]

def add_magma.free_add_semigroup.inhabited {α : Type u} [has_add α] [inhabited α] :

inhabited (add_magma.free_add_semigroup α)

Equations

add_magma.free_add_semigroup.inhabited = {default := ⇑add_magma.free_add_semigroup.of inhabited.default}

source

@[protected, instance]

def magma.assoc_quotient.inhabited {α : Type u} [has_mul α] [inhabited α] :

inhabited (magma.assoc_quotient α)

Equations

magma.assoc_quotient.inhabited = {default := ⇑magma.assoc_quotient.of inhabited.default}

source

@[protected]

theorem add_magma.free_add_semigroup.induction_on {α : Type u} [has_add α] {C : add_magma.free_add_semigroup α → Prop} (x : add_magma.free_add_semigroup α) (ih : ∀ (x : α), C (⇑add_magma.free_add_semigroup.of x)) :

C x

source

@[protected]

theorem magma.assoc_quotient.induction_on {α : Type u} [has_mul α] {C : magma.assoc_quotient α → Prop} (x : magma.assoc_quotient α) (ih : ∀ (x : α), C (⇑magma.assoc_quotient.of x)) :

C x

source

@[ext]

theorem magma.assoc_quotient.hom_ext {α : Type u} [has_mul α] {β : Type v} [semigroup β] {f g : magma.assoc_quotient α →ₙ* β} (h : f.comp magma.assoc_quotient.of = g.comp magma.assoc_quotient.of) :

f = g

source

@[ext]

theorem add_magma.free_add_semigroup.hom_ext {α : Type u} [has_add α] {β : Type v} [add_semigroup β] {f g : add_hom (add_magma.free_add_semigroup α) β} (h : f.comp add_magma.free_add_semigroup.of = g.comp add_magma.free_add_semigroup.of) :

f = g

source

def add_magma.free_add_semigroup.lift {α : Type u} [has_add α] {β : Type v} [add_semigroup β] :

add_hom α β ≃ add_hom (add_magma.free_add_semigroup α) β

Lifts an additive magma homomorphism α → β to an additive semigroup homomorphism add_magma.assoc_quotient α → β given an additive semigroup β.

Equations

add_magma.free_add_semigroup.lift = {to_fun := λ (f : add_hom α β), {to_fun := λ (x : add_magma.free_add_semigroup α), quot.lift_on x ⇑f _, map_add' := _}, inv_fun := λ (f : add_hom (add_magma.free_add_semigroup α) β), f.comp add_magma.free_add_semigroup.of, left_inv := _, right_inv := _}

source

@[simp]

theorem add_magma.free_add_semigroup.lift_symm_apply {α : Type u} [has_add α] {β : Type v} [add_semigroup β] (f : add_hom (add_magma.free_add_semigroup α) β) :

⇑(add_magma.free_add_semigroup.lift.symm) f = f.comp add_magma.free_add_semigroup.of

source

@[simp]

theorem magma.assoc_quotient.lift_symm_apply {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : magma.assoc_quotient α →ₙ* β) :

⇑(magma.assoc_quotient.lift.symm) f = f.comp magma.assoc_quotient.of

source

def magma.assoc_quotient.lift {α : Type u} [has_mul α] {β : Type v} [semigroup β] :

(α →ₙ* β) ≃ (magma.assoc_quotient α →ₙ* β)

Lifts a magma homomorphism α → β to a semigroup homomorphism magma.assoc_quotient α → β given a semigroup β.

Equations

magma.assoc_quotient.lift = {to_fun := λ (f : α →ₙ* β), {to_fun := λ (x : magma.assoc_quotient α), quot.lift_on x ⇑f _, map_mul' := _}, inv_fun := λ (f : magma.assoc_quotient α →ₙ* β), f.comp magma.assoc_quotient.of, left_inv := _, right_inv := _}

source

@[simp]

theorem magma.assoc_quotient.lift_of {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : α →ₙ* β) (x : α) :

⇑(⇑magma.assoc_quotient.lift f) (⇑magma.assoc_quotient.of x) = ⇑f x

source

@[simp]

theorem add_magma.free_add_semigroup.lift_of {α : Type u} [has_add α] {β : Type v} [add_semigroup β] (f : add_hom α β) (x : α) :

⇑(⇑add_magma.free_add_semigroup.lift f) (⇑add_magma.free_add_semigroup.of x) = ⇑f x

source

@[simp]

theorem magma.assoc_quotient.lift_comp_of {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : α →ₙ* β) :

(⇑magma.assoc_quotient.lift f).comp magma.assoc_quotient.of = f

source

@[simp]

theorem add_magma.free_add_semigroup.lift_comp_of {α : Type u} [has_add α] {β : Type v} [add_semigroup β] (f : add_hom α β) :

(⇑add_magma.free_add_semigroup.lift f).comp add_magma.free_add_semigroup.of = f

source

@[simp]

theorem add_magma.free_add_semigroup.lift_comp_of' {α : Type u} [has_add α] {β : Type v} [add_semigroup β] (f : add_hom (add_magma.free_add_semigroup α) β) :

⇑add_magma.free_add_semigroup.lift (f.comp add_magma.free_add_semigroup.of) = f

source

@[simp]

theorem magma.assoc_quotient.lift_comp_of' {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : magma.assoc_quotient α →ₙ* β) :

⇑magma.assoc_quotient.lift (f.comp magma.assoc_quotient.of) = f

source

def magma.assoc_quotient.map {α : Type u} [has_mul α] {β : Type v} [has_mul β] (f : α →ₙ* β) :

magma.assoc_quotient α →ₙ* magma.assoc_quotient β

From a magma homomorphism α →ₙ* β to a semigroup homomorphism magma.assoc_quotient α →ₙ* magma.assoc_quotient β.

Equations

magma.assoc_quotient.map f = ⇑magma.assoc_quotient.lift (magma.assoc_quotient.of.comp f)

source

def add_magma.free_add_semigroup.map {α : Type u} [has_add α] {β : Type v} [has_add β] (f : add_hom α β) :

add_hom (add_magma.free_add_semigroup α) (add_magma.free_add_semigroup β)

From an additive magma homomorphism α → β to an additive semigroup homomorphism add_magma.assoc_quotient α → add_magma.assoc_quotient β.

Equations

add_magma.free_add_semigroup.map f = ⇑add_magma.free_add_semigroup.lift (add_magma.free_add_semigroup.of.comp f)

source

@[simp]

theorem add_magma.free_add_semigroup.map_of {α : Type u} [has_add α] {β : Type v} [has_add β] (f : add_hom α β) (x : α) :

⇑(add_magma.free_add_semigroup.map f) (⇑add_magma.free_add_semigroup.of x) = ⇑add_magma.free_add_semigroup.of (⇑f x)

source

@[simp]

theorem magma.assoc_quotient.map_of {α : Type u} [has_mul α] {β : Type v} [has_mul β] (f : α →ₙ* β) (x : α) :

⇑(magma.assoc_quotient.map f) (⇑magma.assoc_quotient.of x) = ⇑magma.assoc_quotient.of (⇑f x)

source

theorem free_add_semigroup.ext {α : Type u} (x y : free_add_semigroup α) (h : x.head = y.head) (h_1 : x.tail = y.tail) :

x = y

source

@[ext]

structure free_add_semigroup (α : Type u) :

Type u

head : α
tail : list α

Free additive semigroup over a given alphabet.

Instances for free_add_semigroup

free_add_semigroup.has_sizeof_inst
free_add_semigroup.add_semigroup
free_add_semigroup.inhabited
free_add_semigroup.monad
free_add_semigroup.is_lawful_monad
free_add_semigroup.traversable
free_add_semigroup.is_lawful_traversable

source

theorem free_add_semigroup.ext_iff {α : Type u} (x y : free_add_semigroup α) :

x = y ↔ x.head = y.head ∧ x.tail = y.tail

source

theorem free_semigroup.ext {α : Type u} (x y : free_semigroup α) (h : x.head = y.head) (h_1 : x.tail = y.tail) :

x = y

source

@[ext]

structure free_semigroup (α : Type u) :

Type u

head : α
tail : list α

Free semigroup over a given alphabet.

Instances for free_semigroup

source

theorem free_semigroup.ext_iff {α : Type u} (x y : free_semigroup α) :

x = y ↔ x.head = y.head ∧ x.tail = y.tail

source

@[protected, instance]

def free_semigroup.semigroup {α : Type u} :

semigroup (free_semigroup α)

Equations

free_semigroup.semigroup = {mul := λ (L1 L2 : free_semigroup α), {head := L1.head, tail := L1.tail ++ L2.head :: L2.tail}, mul_assoc := _}

source

@[protected, instance]

def free_add_semigroup.add_semigroup {α : Type u} :

add_semigroup (free_add_semigroup α)

Equations

free_add_semigroup.add_semigroup = {add := λ (L1 L2 : free_add_semigroup α), {head := L1.head, tail := L1.tail ++ L2.head :: L2.tail}, add_assoc := _}

source

@[simp]

theorem free_semigroup.head_mul {α : Type u} (x y : free_semigroup α) :

(x * y).head = x.head

source

@[simp]

theorem free_add_semigroup.head_add {α : Type u} (x y : free_add_semigroup α) :

(x + y).head = x.head

source

@[simp]

theorem free_add_semigroup.tail_add {α : Type u} (x y : free_add_semigroup α) :

(x + y).tail = x.tail ++ y.head :: y.tail

source

@[simp]

theorem free_semigroup.tail_mul {α : Type u} (x y : free_semigroup α) :

(x * y).tail = x.tail ++ y.head :: y.tail

source

@[simp]

theorem free_add_semigroup.mk_add_mk {α : Type u} (x y : α) (L1 L2 : list α) :

{head := x, tail := L1} + {head := y, tail := L2} = {head := x, tail := L1 ++ y :: L2}

source

@[simp]

theorem free_semigroup.mk_mul_mk {α : Type u} (x y : α) (L1 L2 : list α) :

{head := x, tail := L1} * {head := y, tail := L2} = {head := x, tail := L1 ++ y :: L2}

source

def free_semigroup.of {α : Type u} (x : α) :

free_semigroup α

The embedding α → free_semigroup α.

Equations

free_semigroup.of x = {head := x, tail := list.nil α}

source

@[simp]

theorem free_add_semigroup.of_tail {α : Type u} (x : α) :

(free_add_semigroup.of x).tail = list.nil

source

@[simp]

theorem free_add_semigroup.of_head {α : Type u} (x : α) :

(free_add_semigroup.of x).head = x

source

@[simp]

theorem free_semigroup.of_head {α : Type u} (x : α) :

(free_semigroup.of x).head = x

source

def free_add_semigroup.of {α : Type u} (x : α) :

free_add_semigroup α

The embedding α → free_add_semigroup α.

Equations

free_add_semigroup.of x = {head := x, tail := list.nil α}

source

@[simp]

theorem free_semigroup.of_tail {α : Type u} (x : α) :

(free_semigroup.of x).tail = list.nil

source

def free_semigroup.length {α : Type u} (x : free_semigroup α) :

ℕ

Length of an element of free semigroup.

Equations

x.length = x.tail.length + 1

source

def free_add_semigroup.length {α : Type u} (x : free_add_semigroup α) :

ℕ

Length of an element of free additive semigroup

Equations

x.length = x.tail.length + 1

source

@[simp]

theorem free_semigroup.length_mul {α : Type u} (x y : free_semigroup α) :

(x * y).length = x.length + y.length

source

@[simp]

theorem free_add_semigroup.length_add {α : Type u} (x y : free_add_semigroup α) :

(x + y).length = x.length + y.length

source

@[simp]

theorem free_semigroup.length_of {α : Type u} (x : α) :

(free_semigroup.of x).length = 1

source

@[simp]

theorem free_add_semigroup.length_of {α : Type u} (x : α) :

(free_add_semigroup.of x).length = 1

source

@[protected, instance]

def free_add_semigroup.inhabited {α : Type u} [inhabited α] :

inhabited (free_add_semigroup α)

Equations

free_add_semigroup.inhabited = {default := free_add_semigroup.of inhabited.default}

source

@[protected, instance]

def free_semigroup.inhabited {α : Type u} [inhabited α] :

inhabited (free_semigroup α)

Equations

free_semigroup.inhabited = {default := free_semigroup.of inhabited.default}

source

@[protected]

def free_add_semigroup.rec_on_add {α : Type u} {C : free_add_semigroup α → Sort l} (x : free_add_semigroup α) (ih1 : Π (x : α), C (free_add_semigroup.of x)) (ih2 : Π (x : α) (y : free_add_semigroup α), C (free_add_semigroup.of x) → C y → C (free_add_semigroup.of x + y)) :

C x

Recursor for free additive semigroup using of and +.

Equations

x.rec_on_add ih1 ih2 = x.rec_on (λ (f : α) (s : list α), s.rec_on ih1 (λ (hd : α) (tl : list α) (ih : Π (_a : α), C {head := _a, tail := tl}) (f : α), ih2 f {head := hd, tail := tl} (ih1 f) (ih hd)) f)

source

@[protected]

def free_semigroup.rec_on_mul {α : Type u} {C : free_semigroup α → Sort l} (x : free_semigroup α) (ih1 : Π (x : α), C (free_semigroup.of x)) (ih2 : Π (x : α) (y : free_semigroup α), C (free_semigroup.of x) → C y → C (free_semigroup.of x * y)) :

C x

Recursor for free semigroup using of and *.

Equations

x.rec_on_mul ih1 ih2 = x.rec_on (λ (f : α) (s : list α), s.rec_on ih1 (λ (hd : α) (tl : list α) (ih : Π (_a : α), C {head := _a, tail := tl}) (f : α), ih2 f {head := hd, tail := tl} (ih1 f) (ih hd)) f)

source

@[ext]

theorem free_semigroup.hom_ext {α : Type u} {β : Type v} [has_mul β] {f g : free_semigroup α →ₙ* β} (h : ⇑f ∘ free_semigroup.of = ⇑g ∘ free_semigroup.of) :

f = g

source

@[ext]

theorem free_add_semigroup.hom_ext {α : Type u} {β : Type v} [has_add β] {f g : add_hom (free_add_semigroup α) β} (h : ⇑f ∘ free_add_semigroup.of = ⇑g ∘ free_add_semigroup.of) :

f = g

source

@[simp]

theorem free_semigroup.lift_symm_apply {α : Type u} {β : Type v} [semigroup β] (f : free_semigroup α →ₙ* β) (ᾰ : α) :

⇑(free_semigroup.lift.symm) f ᾰ = (⇑f ∘ free_semigroup.of) ᾰ

source

@[simp]

theorem free_add_semigroup.lift_symm_apply {α : Type u} {β : Type v} [add_semigroup β] (f : add_hom (free_add_semigroup α) β) (ᾰ : α) :

⇑(free_add_semigroup.lift.symm) f ᾰ = (⇑f ∘ free_add_semigroup.of) ᾰ

source

def free_semigroup.lift {α : Type u} {β : Type v} [semigroup β] :

(α → β) ≃ (free_semigroup α →ₙ* β)

Lifts a function α → β to a semigroup homomorphism free_semigroup α → β given a semigroup β.

Equations

free_semigroup.lift = {to_fun := λ (f : α → β), {to_fun := λ (x : free_semigroup α), list.foldl (λ (a : β) (b : α), a * f b) (f x.head) x.tail, map_mul' := _}, inv_fun := λ (f : free_semigroup α →ₙ* β), ⇑f ∘ free_semigroup.of, left_inv := _, right_inv := _}

source

def free_add_semigroup.lift {α : Type u} {β : Type v} [add_semigroup β] :

(α → β) ≃ add_hom (free_add_semigroup α) β

Lifts a function α → β to an additive semigroup homomorphism free_add_semigroup α → β given an additive semigroup β.

Equations

free_add_semigroup.lift = {to_fun := λ (f : α → β), {to_fun := λ (x : free_add_semigroup α), list.foldl (λ (a : β) (b : α), a + f b) (f x.head) x.tail, map_add' := _}, inv_fun := λ (f : add_hom (free_add_semigroup α) β), ⇑f ∘ free_add_semigroup.of, left_inv := _, right_inv := _}

source

@[simp]

theorem free_semigroup.lift_of {α : Type u} {β : Type v} [semigroup β] (f : α → β) (x : α) :

⇑(⇑free_semigroup.lift f) (free_semigroup.of x) = f x

source

@[simp]

theorem free_add_semigroup.lift_of {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) (x : α) :

⇑(⇑free_add_semigroup.lift f) (free_add_semigroup.of x) = f x

source

@[simp]

theorem free_add_semigroup.lift_comp_of {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) :

⇑(⇑free_add_semigroup.lift f) ∘ free_add_semigroup.of = f

source

@[simp]

theorem free_semigroup.lift_comp_of {α : Type u} {β : Type v} [semigroup β] (f : α → β) :

⇑(⇑free_semigroup.lift f) ∘ free_semigroup.of = f

source

@[simp]

theorem free_semigroup.lift_comp_of' {α : Type u} {β : Type v} [semigroup β] (f : free_semigroup α →ₙ* β) :

⇑free_semigroup.lift (⇑f ∘ free_semigroup.of) = f

source

@[simp]

theorem free_add_semigroup.lift_comp_of' {α : Type u} {β : Type v} [add_semigroup β] (f : add_hom (free_add_semigroup α) β) :

⇑free_add_semigroup.lift (⇑f ∘ free_add_semigroup.of) = f

source

theorem free_add_semigroup.lift_of_add {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) (x : α) (y : free_add_semigroup α) :

⇑(⇑free_add_semigroup.lift f) (free_add_semigroup.of x + y) = f x + ⇑(⇑free_add_semigroup.lift f) y

source

theorem free_semigroup.lift_of_mul {α : Type u} {β : Type v} [semigroup β] (f : α → β) (x : α) (y : free_semigroup α) :

⇑(⇑free_semigroup.lift f) (free_semigroup.of x * y) = f x * ⇑(⇑free_semigroup.lift f) y

source

def free_semigroup.map {α : Type u} {β : Type v} (f : α → β) :

free_semigroup α →ₙ* free_semigroup β

The unique semigroup homomorphism that sends of x to of (f x).

Equations

free_semigroup.map f = ⇑free_semigroup.lift (free_semigroup.of ∘ f)

source

def free_add_semigroup.map {α : Type u} {β : Type v} (f : α → β) :

add_hom (free_add_semigroup α) (free_add_semigroup β)

The unique additive semigroup homomorphism that sends of x to of (f x).

Equations

free_add_semigroup.map f = ⇑free_add_semigroup.lift (free_add_semigroup.of ∘ f)

source

@[simp]

theorem free_add_semigroup.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :

⇑(free_add_semigroup.map f) (free_add_semigroup.of x) = free_add_semigroup.of (f x)

source

@[simp]

theorem free_semigroup.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :

⇑(free_semigroup.map f) (free_semigroup.of x) = free_semigroup.of (f x)

source

@[simp]

theorem free_semigroup.length_map {α : Type u} {β : Type v} (f : α → β) (x : free_semigroup α) :

(⇑(free_semigroup.map f) x).length = x.length

source

@[simp]

theorem free_add_semigroup.length_map {α : Type u} {β : Type v} (f : α → β) (x : free_add_semigroup α) :

(⇑(free_add_semigroup.map f) x).length = x.length

source

@[protected, instance]

def free_semigroup.monad :

monad free_semigroup

Equations

free_semigroup.monad = monad.mk

source

@[protected, instance]

def free_add_semigroup.monad :

monad free_add_semigroup

Equations

free_add_semigroup.monad = monad.mk

source

def free_semigroup.rec_on_pure {α : Type u} {C : free_semigroup α → Sort l} (x : free_semigroup α) (ih1 : Π (x : α), C (has_pure.pure x)) (ih2 : Π (x : α) (y : free_semigroup α), C (has_pure.pure x) → C y → C (has_pure.pure x * y)) :

C x

Recursor that uses pure instead of of.

Equations

x.rec_on_pure ih1 ih2 = x.rec_on_mul ih1 ih2

source

def free_add_semigroup.rec_on_pure {α : Type u} {C : free_add_semigroup α → Sort l} (x : free_add_semigroup α) (ih1 : Π (x : α), C (has_pure.pure x)) (ih2 : Π (x : α) (y : free_add_semigroup α), C (has_pure.pure x) → C y → C (has_pure.pure x + y)) :

C x

Recursor that uses pure instead of of.

Equations

x.rec_on_pure ih1 ih2 = x.rec_on_add ih1 ih2

source

@[simp]

theorem free_semigroup.map_pure {α β : Type u} (f : α → β) (x : α) :

f <$> has_pure.pure x = has_pure.pure (f x)

source

@[simp]

theorem free_add_semigroup.map_pure {α β : Type u} (f : α → β) (x : α) :

f <$> has_pure.pure x = has_pure.pure (f x)

source

@[simp]

theorem free_add_semigroup.map_add' {α β : Type u} (f : α → β) (x y : free_add_semigroup α) :

f <$> (x + y) = f <$> x + f <$> y

source

@[simp]

theorem free_semigroup.map_mul' {α β : Type u} (f : α → β) (x y : free_semigroup α) :

f <$> (x * y) = f <$> x * f <$> y

source

@[simp]

theorem free_add_semigroup.pure_bind {α β : Type u} (f : α → free_add_semigroup β) (x : α) :

has_pure.pure x >>= f = f x

source

@[simp]

theorem free_semigroup.pure_bind {α β : Type u} (f : α → free_semigroup β) (x : α) :

has_pure.pure x >>= f = f x

source

@[simp]

theorem free_add_semigroup.add_bind {α β : Type u} (f : α → free_add_semigroup β) (x y : free_add_semigroup α) :

x + y >>= f = (x >>= f) + (y >>= f)

source

@[simp]

theorem free_semigroup.mul_bind {α β : Type u} (f : α → free_semigroup β) (x y : free_semigroup α) :

x * y >>= f = (x >>= f) * (y >>= f)

source

@[simp]

theorem free_add_semigroup.pure_seq {α β : Type u} {f : α → β} {x : free_add_semigroup α} :

has_pure.pure f <*> x = f <$> x

source

@[simp]

theorem free_semigroup.pure_seq {α β : Type u} {f : α → β} {x : free_semigroup α} :

has_pure.pure f <*> x = f <$> x

source

@[simp]

theorem free_semigroup.mul_seq {α β : Type u} {f g : free_semigroup (α → β)} {x : free_semigroup α} :

f * g <*> x = (f <*> x) * (g <*> x)

source

@[simp]

theorem free_add_semigroup.add_seq {α β : Type u} {f g : free_add_semigroup (α → β)} {x : free_add_semigroup α} :

f + g <*> x = (f <*> x) + (g <*> x)

source

@[protected, instance]

def free_semigroup.is_lawful_monad :

is_lawful_monad free_semigroup

source

@[protected, instance]

def free_add_semigroup.is_lawful_monad :

is_lawful_monad free_add_semigroup

source

@[protected]

def free_add_semigroup.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) (x : free_add_semigroup α) :

m (free_add_semigroup β)

free_add_semigroup is traversable.

Equations

free_add_semigroup.traverse F x = x.rec_on_pure (λ (x : α), has_pure.pure <$> F x) (λ (x : α) (y : free_add_semigroup α) (ihx ihy : m (free_add_semigroup β)), has_add.add <$> ihx <*> ihy)

source

@[protected]

def free_semigroup.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) (x : free_semigroup α) :

m (free_semigroup β)

free_semigroup is traversable.

Equations

free_semigroup.traverse F x = x.rec_on_pure (λ (x : α), has_pure.pure <$> F x) (λ (x : α) (y : free_semigroup α) (ihx ihy : m (free_semigroup β)), has_mul.mul <$> ihx <*> ihy)

source

@[protected, instance]

def free_add_semigroup.traversable :

traversable free_add_semigroup

Equations

free_add_semigroup.traversable = {to_functor := applicative.to_functor monad.to_applicative, traverse := free_add_semigroup.traverse}

source

@[protected, instance]

def free_semigroup.traversable :

traversable free_semigroup

Equations

free_semigroup.traversable = {to_functor := applicative.to_functor monad.to_applicative, traverse := free_semigroup.traverse}

source

@[simp]

theorem free_add_semigroup.traverse_pure {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : α) :

traversable.traverse F (has_pure.pure x) = has_pure.pure <$> F x

source

@[simp]

theorem free_semigroup.traverse_pure {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : α) :

traversable.traverse F (has_pure.pure x) = has_pure.pure <$> F x

source

@[simp]

theorem free_add_semigroup.traverse_pure' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :

traversable.traverse F ∘ has_pure.pure = λ (x : α), has_pure.pure <$> F x

source

@[simp]

theorem free_semigroup.traverse_pure' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :

traversable.traverse F ∘ has_pure.pure = λ (x : α), has_pure.pure <$> F x

source

@[simp]

theorem free_add_semigroup.traverse_add {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) [is_lawful_applicative m] (x y : free_add_semigroup α) :

traversable.traverse F (x + y) = has_add.add <$> traversable.traverse F x <*> traversable.traverse F y

source

@[simp]

theorem free_semigroup.traverse_mul {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) [is_lawful_applicative m] (x y : free_semigroup α) :

traversable.traverse F (x * y) = has_mul.mul <$> traversable.traverse F x <*> traversable.traverse F y

source

@[simp]

theorem free_add_semigroup.traverse_add' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) [is_lawful_applicative m] :

function.comp (traversable.traverse F) ∘ has_add.add = λ (x y : free_add_semigroup α), has_add.add <$> traversable.traverse F x <*> traversable.traverse F y

source

@[simp]

theorem free_semigroup.traverse_mul' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) [is_lawful_applicative m] :

function.comp (traversable.traverse F) ∘ has_mul.mul = λ (x y : free_semigroup α), has_mul.mul <$> traversable.traverse F x <*> traversable.traverse F y

source

@[simp]

theorem free_semigroup.traverse_eq {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : free_semigroup α) :

free_semigroup.traverse F x = traversable.traverse F x

source

@[simp]

theorem free_add_semigroup.traverse_eq {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : free_add_semigroup α) :

free_add_semigroup.traverse F x = traversable.traverse F x

source

@[simp]

theorem free_add_semigroup.add_map_seq {α : Type u} (x y : free_add_semigroup α) :

has_add.add <$> x <*> y = x + y

source

@[simp]

theorem free_semigroup.mul_map_seq {α : Type u} (x y : free_semigroup α) :

has_mul.mul <$> x <*> y = x * y

source

@[protected, instance]

def free_add_semigroup.is_lawful_traversable :

is_lawful_traversable free_add_semigroup

Equations

free_add_semigroup.is_lawful_traversable = {to_is_lawful_functor := free_add_semigroup.is_lawful_traversable._proof_1, id_traverse := free_add_semigroup.is_lawful_traversable._proof_2, comp_traverse := free_add_semigroup.is_lawful_traversable._proof_3, traverse_eq_map_id := free_add_semigroup.is_lawful_traversable._proof_4, naturality := free_add_semigroup.is_lawful_traversable._proof_5}

source

@[protected, instance]

def free_semigroup.is_lawful_traversable :

is_lawful_traversable free_semigroup

Equations

free_semigroup.is_lawful_traversable = {to_is_lawful_functor := free_semigroup.is_lawful_traversable._proof_1, id_traverse := free_semigroup.is_lawful_traversable._proof_2, comp_traverse := free_semigroup.is_lawful_traversable._proof_3, traverse_eq_map_id := free_semigroup.is_lawful_traversable._proof_4, naturality := free_semigroup.is_lawful_traversable._proof_5}