From c64b92243ad6b33ca4f565c87ed99b59d1d2a7ff Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 6 Nov 2022 07:48:39 +0000 Subject: [PATCH] refactor(algebra/free): review API, redefine `free_semigroup` (#17144) --- src/algebra/free.lean | 376 +++++++++++++++++++------------------ src/algebra/hom/equiv.lean | 17 ++ 2 files changed, 213 insertions(+), 180 deletions(-) diff --git a/src/algebra/free.lean b/src/algebra/free.lean index 4e94ee31c8e30..f02c2609008c7 100644 --- a/src/algebra/free.lean +++ b/src/algebra/free.lean @@ -7,6 +7,7 @@ import algebra.hom.group import control.applicative import control.traversable.basic import logic.equiv.defs +import data.list.basic /-! # Free constructions @@ -15,10 +16,11 @@ import logic.equiv.defs * `free_magma α`: free magma (structure with binary operation without any axioms) over alphabet `α`, defined inductively, with traversable instance and decidable equality. -* `magma.free_semigroup α`: free semigroup over magma `α`. -* `free_semigroup α`: free semigroup over alphabet `α`, defined as a synonym for `α × list α` - (i.e. nonempty lists), with traversable instance and decidable equality. -* `free_semigroup_free_magma α`: isomorphism between `magma.free_semigroup (free_magma α)` and +* `magma.assoc_quotient α`: quotient of a magma `α` by the associativity equivalence relation. +* `free_semigroup α`: free semigroup over alphabet `α`, defined as a structure with two fields + `head : α` and `tail : list α` (i.e. nonempty lists), with traversable instance and decidable + equality. +* `free_magma_assoc_quotient_equiv α`: isomorphism between `magma.assoc_quotient (free_magma α)` and `free_semigroup α`. * `free_magma.lift`: the universal property of the free magma, expressing its adjointness. -/ @@ -62,6 +64,10 @@ def rec_on_mul {C : free_magma α → Sort l} (x) C x := free_magma.rec_on x ih1 ih2 +@[ext, to_additive] +lemma hom_ext {β : Type v} [has_mul β] {f g : free_magma α →ₙ* β} (h : f ∘ of = g ∘ of) : f = g := +fun_like.ext _ _ $ λ x, rec_on_mul x (congr_fun h) $ by { intros, simp only [map_mul, *] } + end free_magma /-- Lifts a function `α → β` to a magma homomorphism `free_magma α → β` given a magma `β`. -/ @@ -79,56 +85,47 @@ attribute [to_additive free_add_magma.lift_aux] free_magma.lift_aux namespace free_magma -variables {α : Type u} {β : Type v} [has_mul β] (f : α → β) +section lift -@[to_additive] -theorem lift_aux_unique (F : free_magma α →ₙ* β) : ⇑F = lift_aux (F ∘ of) := -funext $ λ x, free_magma.rec_on x (λ x, rfl) $ λ x y ih1 ih2, -(F.map_mul x y).trans $ congr (congr_arg _ ih1) ih2 +variables {α : Type u} {β : Type v} [has_mul β] (f : α → β) /-- The universal property of the free magma expressing its adjointness. -/ -@[to_additive "The universal property of the free additive magma expressing its adjointness."] +@[to_additive "The universal property of the free additive magma expressing its adjointness.", + simps symm_apply] def lift : (α → β) ≃ (free_magma α →ₙ* β) := { to_fun := λ f, { to_fun := lift_aux f, map_mul' := λ x y, rfl, }, inv_fun := λ F, F ∘ of, - left_inv := λ f, by { ext, simp only [lift_aux, mul_hom.coe_mk, function.comp_app], }, - right_inv := λ F, by { ext, rw [mul_hom.coe_mk, lift_aux_unique], } } + left_inv := λ f, by { ext, refl }, + right_inv := λ F, by { ext, refl } } @[simp, to_additive] lemma lift_of (x) : lift f (of x) = f x := rfl +@[simp, to_additive] lemma lift_comp_of : lift f ∘ of = f := rfl -end free_magma - -/-- The unique magma homomorphism `free_magma α → free_magma β` that sends -each `of x` to `of (f x)`. -/ -def free_magma.map {α : Type u} {β : Type v} (f : α → β) : free_magma α → free_magma β -| (free_magma.of x) := free_magma.of (f x) -| (x * y) := x.map * y.map - -/-- The unique additive magma homomorphism `free_add_magma α → free_add_magma β` that sends -each `of x` to `of (f x)`. -/ -def free_add_magma.map {α : Type u} {β : Type v} (f : α → β) : free_add_magma α → free_add_magma β -| (free_add_magma.of x) := free_add_magma.of (f x) -| (x + y) := x.map + y.map +@[simp, to_additive] lemma lift_comp_of' (f : free_magma α →ₙ* β) : lift (f ∘ of) = f := +lift.apply_symm_apply f -attribute [to_additive free_add_magma.map] free_magma.map - -namespace free_magma - -variables {α : Type u} +end lift section map -variables {β : Type v} (f : α → β) +variables {α : Type u} {β : Type v} (f : α → β) + +/-- The unique magma homomorphism `free_magma α →ₙ* free_magma β` that sends +each `of x` to `of (f x)`. -/ +@[to_additive "The unique additive magma homomorphism `free_add_magma α → free_add_magma β` that +sends each `of x` to `of (f x)`."] +def map (f : α → β) : free_magma α →ₙ* free_magma β := lift (of ∘ f) @[simp, to_additive] lemma map_of (x) : map f (of x) = of (f x) := rfl -@[simp, to_additive] lemma map_mul (x y) : map f (x * y) = map f x * map f y := rfl end map section category +variables {α β : Type u} + @[to_additive] instance : monad free_magma := { pure := λ _, of, @@ -141,8 +138,6 @@ protected def rec_on_pure {C : free_magma α → Sort l} (x) C x := free_magma.rec_on_mul x ih1 ih2 -variables {β : Type u} - @[simp, to_additive] lemma map_pure (f : α → β) (x) : (f <$> pure x : free_magma β) = pure (f x) := rfl @@ -261,128 +256,124 @@ attribute [to_additive free_add_magma.repr] free_magma.repr instance {α : Type u} [has_repr α] : has_repr (free_magma α) := ⟨free_magma.repr⟩ /-- Length of an element of a free magma. -/ -def free_magma.length {α : Type u} : free_magma α → ℕ +@[simp] def free_magma.length {α : Type u} : free_magma α → ℕ | (free_magma.of x) := 1 | (x * y) := x.length + y.length /-- Length of an element of a free additive magma. -/ -def free_add_magma.length {α : Type u} : free_add_magma α → ℕ +@[simp] def free_add_magma.length {α : Type u} : free_add_magma α → ℕ | (free_add_magma.of x) := 1 | (x + y) := x.length + y.length attribute [to_additive free_add_magma.length] free_magma.length -/-- Associativity relations for a magma. -/ -inductive magma.free_semigroup.r (α : Type u) [has_mul α] : α → α → Prop -| intro : ∀ x y z, magma.free_semigroup.r ((x * y) * z) (x * (y * z)) -| left : ∀ w x y z, magma.free_semigroup.r (w * ((x * y) * z)) (w * (x * (y * z))) - /-- Associativity relations for an additive magma. -/ -inductive add_magma.free_add_semigroup.r (α : Type u) [has_add α] : α → α → Prop -| intro : ∀ x y z, add_magma.free_add_semigroup.r ((x + y) + z) (x + (y + z)) -| left : ∀ w x y z, add_magma.free_add_semigroup.r (w + ((x + y) + z)) (w + (x + (y + z))) +inductive add_magma.assoc_rel (α : Type u) [has_add α] : α → α → Prop +| intro : ∀ x y z, add_magma.assoc_rel ((x + y) + z) (x + (y + z)) +| left : ∀ w x y z, add_magma.assoc_rel (w + ((x + y) + z)) (w + (x + (y + z))) -attribute [to_additive add_magma.free_add_semigroup.r] magma.free_semigroup.r +/-- Associativity relations for a magma. -/ +@[to_additive add_magma.assoc_rel "Associativity relations for an additive magma."] +inductive magma.assoc_rel (α : Type u) [has_mul α] : α → α → Prop +| intro : ∀ x y z, magma.assoc_rel ((x * y) * z) (x * (y * z)) +| left : ∀ w x y z, magma.assoc_rel (w * ((x * y) * z)) (w * (x * (y * z))) namespace magma -/-- Free semigroup over a magma. -/ -@[to_additive add_magma.free_add_semigroup "Free additive semigroup over an additive magma."] -def free_semigroup (α : Type u) [has_mul α] : Type u := -quot $ free_semigroup.r α +/-- Semigroup quotient of a magma. -/ +@[to_additive add_magma.free_add_semigroup "Additive semigroup quotient of an additive magma."] +def assoc_quotient (α : Type u) [has_mul α] : Type u := quot $ assoc_rel α -namespace free_semigroup +namespace assoc_quotient variables {α : Type u} [has_mul α] -/-- Embedding from magma to its free semigroup. -/ -@[to_additive "Embedding from additive magma to its free additive semigroup."] -def of : α → free_semigroup α := quot.mk _ - @[to_additive] -instance [inhabited α] : inhabited (free_semigroup α) := ⟨of default⟩ - -@[elab_as_eliminator, to_additive] -protected lemma induction_on {C : free_semigroup α → Prop} (x : free_semigroup α) - (ih : ∀ x, C (of x)) : C x := -quot.induction_on x ih +lemma quot_mk_assoc (x y z : α) : quot.mk (assoc_rel α) (x * y * z) = quot.mk _ (x * (y * z)) := +quot.sound (assoc_rel.intro _ _ _) @[to_additive] -theorem of_mul_assoc (x y z : α) : of ((x * y) * z) = of (x * (y * z)) := -quot.sound $ r.intro x y z +lemma quot_mk_assoc_left (x y z w : α) : + quot.mk (assoc_rel α) (x * (y * z * w)) = quot.mk _ (x * (y * (z * w))) := +quot.sound (assoc_rel.left _ _ _ _) @[to_additive] -theorem of_mul_assoc_left (w x y z : α) : of (w * ((x * y) * z)) = of (w * (x * (y * z))) := -quot.sound $ r.left w x y z +instance : semigroup (assoc_quotient α) := +{ mul := λ x y, + begin + refine quot.lift_on₂ x y (λ x y, quot.mk _ (x * y)) _ _, + { rintro a b₁ b₂ (⟨c, d, e⟩ | ⟨c, d, e, f⟩); simp only, + { exact quot_mk_assoc_left _ _ _ _ }, + { rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc] } }, + { rintro a₁ a₂ b (⟨c, d, e⟩ | ⟨c, d, e, f⟩); simp only, + { simp only [quot_mk_assoc, quot_mk_assoc_left] }, + { rw [quot_mk_assoc, quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc_left, + quot_mk_assoc_left, ← quot_mk_assoc c d, ← quot_mk_assoc c d, quot_mk_assoc_left] } } + end, + mul_assoc := λ x y z, quot.induction_on₃ x y z $ λ p q r, quot_mk_assoc p q r } -@[to_additive] -theorem of_mul_assoc_right (w x y z : α) : of (((w * x) * y) * z) = of ((w * (x * y)) * z) := -by rw [of_mul_assoc, of_mul_assoc, of_mul_assoc, of_mul_assoc_left] +/-- Embedding from magma to its free semigroup. -/ +@[to_additive "Embedding from additive magma to its free additive semigroup."] +def of : α →ₙ* assoc_quotient α := ⟨quot.mk _, λ x y, rfl⟩ @[to_additive] -instance : semigroup (free_semigroup α) := -{ mul := λ x y, begin - refine quot.lift_on x (λ p, quot.lift_on y (λ q, (quot.mk _ $ p * q : free_semigroup α)) _) _, - { rintros a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩); change of _ = of _, - { rw of_mul_assoc_left }, - { rw [← of_mul_assoc, of_mul_assoc_left, of_mul_assoc] } }, - { refine quot.induction_on y (λ q, _), - rintros a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩); change of _ = of _, - { rw of_mul_assoc_right }, - { rw [of_mul_assoc, of_mul_assoc, of_mul_assoc_left, of_mul_assoc_left, of_mul_assoc_left, - ← of_mul_assoc c d, ← of_mul_assoc c d, of_mul_assoc_left] } } - end, - mul_assoc := λ x y z, quot.induction_on x $ λ p, quot.induction_on y $ λ q, - quot.induction_on z $ λ r, of_mul_assoc p q r } +instance [inhabited α] : inhabited (assoc_quotient α) := ⟨of default⟩ -@[to_additive] -theorem of_mul (x y : α) : of (x * y) = of x * of y := rfl +@[elab_as_eliminator, to_additive] +protected lemma induction_on {C : assoc_quotient α → Prop} (x : assoc_quotient α) + (ih : ∀ x, C (of x)) : C x := +quot.induction_on x ih section lift -variables {β : Type v} [semigroup β] (f : α → β) +variables {β : Type v} [semigroup β] (f : α →ₙ* β) -/-- Lifts a magma homomorphism `α → β` to a semigroup homomorphism `magma.free_semigroup α → β` +@[ext, to_additive] +lemma hom_ext {f g : assoc_quotient α →ₙ* β} (h : f.comp of = g.comp of) : f = g := +fun_like.ext _ _ $ λ x, assoc_quotient.induction_on x $ fun_like.congr_fun h + +/-- Lifts a magma homomorphism `α → β` to a semigroup homomorphism `magma.assoc_quotient α → β` given a semigroup `β`. -/ @[to_additive "Lifts an additive magma homomorphism `α → β` to an additive semigroup homomorphism -`add_magma.free_add_semigroup α → β` given an additive semigroup `β`."] -def lift (hf : ∀ x y, f (x * y) = f x * f y) : free_semigroup α → β := -quot.lift f $ by rintros a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩); simp only [hf, mul_assoc] +`add_magma.assoc_quotient α → β` given an additive semigroup `β`.", simps symm_apply] +def lift : (α →ₙ* β) ≃ (assoc_quotient α →ₙ* β) := +{ to_fun := λ f, + { to_fun := λ x, quot.lift_on x f $ + by rintros a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩); simp only [map_mul, mul_assoc], + map_mul' := λ x y, quot.induction_on₂ x y (map_mul f) }, + inv_fun := λ f, f.comp of, + left_inv := λ f, fun_like.ext _ _ $ λ x, rfl, + right_inv := λ f, hom_ext $ fun_like.ext _ _ $ λ x, rfl } -@[simp, to_additive] lemma lift_of {hf} (x : α) : lift f hf (of x) = f x := rfl +@[simp, to_additive] lemma lift_of (x : α) : lift f (of x) = f x := rfl -@[simp, to_additive] lemma lift_mul {hf} (x y) : lift f hf (x * y) = lift f hf x * lift f hf y := -quot.induction_on x $ λ p, quot.induction_on y $ λ q, hf p q +@[simp, to_additive] lemma lift_comp_of : (lift f).comp of = f := lift.symm_apply_apply f -@[to_additive] -theorem lift_unique (f : free_semigroup α → β) (hf : ∀ x y, f (x * y) = f x * f y) : - f = lift (f ∘ of) (λ p q, hf (of p) (of q)) := -funext $ λ x, quot.induction_on x $ λ p, rfl +@[simp, to_additive] lemma lift_comp_of' (f : assoc_quotient α →ₙ* β) : + lift (f.comp of) = f := +lift.apply_symm_apply f end lift -variables {β : Type v} [has_mul β] (f : α → β) +variables {β : Type v} [has_mul β] (f : α →ₙ* β) -/-- From a magma homomorphism `α → β` to a semigroup homomorphism -`magma.free_semigroup α → magma.free_semigroup β`. -/ +/-- From a magma homomorphism `α →ₙ* β` to a semigroup homomorphism +`magma.assoc_quotient α →ₙ* magma.assoc_quotient β`. -/ @[to_additive "From an additive magma homomorphism `α → β` to an additive semigroup homomorphism -`add_magma.free_add_semigroup α → add_magma.free_add_semigroup β`."] -def map (hf : ∀ x y, f (x * y) = f x * f y) : free_semigroup α → free_semigroup β := -lift (of ∘ f) (λ x y, congr_arg of $ hf x y) +`add_magma.assoc_quotient α → add_magma.assoc_quotient β`."] +def map : assoc_quotient α →ₙ* assoc_quotient β := lift (of.comp f) -@[simp, to_additive] lemma map_of {hf} (x) : map f hf (of x) = of (f x) := rfl -@[simp, to_additive] lemma map_mul {hf} (x y) : map f hf (x * y) = map f hf x * map f hf y := -lift_mul _ _ _ +@[simp, to_additive] lemma map_of (x) : map f (of x) = of (f x) := rfl -end free_semigroup +end assoc_quotient end magma -/-- Free semigroup over a given alphabet. -(Note: In this definition, the free semigroup does not contain the empty word.) -/ -@[to_additive "Free additive semigroup over a given alphabet."] -def free_semigroup (α : Type u) : Type u := -α × list α +/-- Free additive semigroup over a given alphabet. -/ +@[ext] structure free_add_semigroup (α : Type u) := (head : α) (tail : list α) + +/-- Free semigroup over a given alphabet. -/ +@[ext, to_additive] structure free_semigroup (α : Type u) := (head : α) (tail : list α) namespace free_semigroup @@ -390,42 +381,45 @@ variables {α : Type u} @[to_additive] instance : semigroup (free_semigroup α) := -{ mul := λ L1 L2, (L1.1, L1.2 ++ L2.1 :: L2.2), - mul_assoc := λ L1 L2 L3, prod.ext rfl $ list.append_assoc _ _ _ } +{ mul := λ L1 L2, ⟨L1.1, L1.2 ++ L2.1 :: L2.2⟩, + mul_assoc := λ L1 L2 L3, ext _ _ rfl $ list.append_assoc _ _ _ } -/-- The embedding `α → free_semigroup α`. -/ -@[to_additive "The embedding `α → free_add_semigroup α`."] -def of (x : α) : free_semigroup α := -(x, []) +@[simp, to_additive] lemma head_mul (x y : free_semigroup α) : (x * y).1 = x.1 := rfl -@[to_additive] -instance [inhabited α] : inhabited (free_semigroup α) := ⟨of default⟩ +@[simp, to_additive] lemma tail_mul (x y : free_semigroup α) : (x * y).2 = x.2 ++ (y.1 :: y.2) := +rfl -/-- Recursor for free semigroup using `of` and `*`. -/ -@[elab_as_eliminator, to_additive "Recursor for free additive semigroup using `of` and `+`."] -protected def rec_on {C : free_semigroup α → Sort l} (x) - (ih1 : ∀ x, C (of x)) (ih2 : ∀ x y, C (of x) → C y → C (of x * y)) : - C x := -prod.rec_on x $ λ f s, list.rec_on s ih1 (λ hd tl ih f, ih2 f (hd, tl) (ih1 f) (ih hd)) f +@[simp, to_additive] lemma mk_mul_mk (x y : α) (L1 L2 : list α) : + mk x L1 * mk y L2 = mk x (L1 ++ y :: L2) := rfl -end free_semigroup +/-- The embedding `α → free_semigroup α`. -/ +@[to_additive "The embedding `α → free_add_semigroup α`.", simps] +def of (x : α) : free_semigroup α := ⟨x, []⟩ -/-- Auxiliary function for `free_semigroup.lift`. -/ -def free_semigroup.lift' {α : Type u} {β : Type v} [semigroup β] (f : α → β) : α → list α → β -| x [] := f x -| x (hd::tl) := f x * free_semigroup.lift' hd tl +/-- Length of an element of free semigroup. -/ +@[to_additive "Length of an element of free additive semigroup"] +def length (x : free_semigroup α) : ℕ := x.tail.length + 1 -/-- Auxiliary function for `free_semigroup.lift`. -/ -def free_add_semigroup.lift' {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) : - α → list α → β -| x [] := f x -| x (hd::tl) := f x + free_add_semigroup.lift' hd tl +@[simp, to_additive] lemma length_mul (x y : free_semigroup α) : + (x * y).length = x.length + y.length := +by simp [length, ← add_assoc, add_right_comm] -attribute [to_additive free_add_semigroup.lift'] free_semigroup.lift' +@[simp, to_additive] lemma length_of (x : α) : (of x).length = 1 := rfl -namespace free_semigroup +@[to_additive] instance [inhabited α] : inhabited (free_semigroup α) := ⟨of default⟩ -variables {α : Type u} +/-- Recursor for free semigroup using `of` and `*`. -/ +@[elab_as_eliminator, to_additive "Recursor for free additive semigroup using `of` and `+`."] +protected def rec_on_mul {C : free_semigroup α → Sort l} (x) + (ih1 : ∀ x, C (of x)) (ih2 : ∀ x y, C (of x) → C y → C (of x * y)) : + C x := +free_semigroup.rec_on x $ λ f s, list.rec_on s ih1 (λ hd tl ih f, ih2 f ⟨hd, tl⟩ (ih1 f) (ih hd)) f + +@[ext, to_additive] +lemma hom_ext {β : Type v} [has_mul β] {f g : free_semigroup α →ₙ* β} (h : f ∘ of = g ∘ of) : + f = g := +fun_like.ext _ _ $ λ x, free_semigroup.rec_on_mul x (congr_fun h) $ + λ x y hx hy, by simp only [map_mul, *] section lift @@ -434,22 +428,24 @@ variables {β : Type v} [semigroup β] (f : α → β) /-- Lifts a function `α → β` to a semigroup homomorphism `free_semigroup α → β` given a semigroup `β`. -/ @[to_additive "Lifts a function `α → β` to an additive semigroup homomorphism -`free_add_semigroup α → β` given an additive semigroup `β`."] -def lift (x : free_semigroup α) : β := -lift' f x.1 x.2 +`free_add_semigroup α → β` given an additive semigroup `β`.", simps symm_apply] +def lift : (α → β) ≃ (free_semigroup α →ₙ* β) := +{ to_fun := λ f, + { to_fun := λ x, x.2.foldl (λ a b, a * f b) (f x.1), + map_mul' := λ x y, by simp only [head_mul, tail_mul, ← list.foldl_map f, list.foldl_append, + list.foldl_cons, list.foldl_assoc] }, + inv_fun := λ f, f ∘ of, + left_inv := λ f, rfl, + right_inv := λ f, hom_ext rfl } @[simp, to_additive] lemma lift_of (x : α) : lift f (of x) = f x := rfl -@[to_additive] lemma lift_of_mul (x y) : lift f (of x * y) = f x * lift f y := rfl +@[simp, to_additive] lemma lift_comp_of : lift f ∘ of = f := rfl -@[simp, to_additive] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y := -free_semigroup.rec_on x (λ p, rfl) - (λ p x ih1 ih2, by rw [mul_assoc, lift_of_mul, lift_of_mul, mul_assoc, ih2]) +@[simp, to_additive] lemma lift_comp_of' (f : free_semigroup α →ₙ* β) : lift (f ∘ of) = f := +hom_ext rfl -@[to_additive] -theorem lift_unique (f : free_semigroup α → β) (hf : ∀ x y, f (x * y) = f x * f y) : - f = lift (f ∘ of) := -funext $ λ ⟨x, L⟩, list.rec_on L (λ x, rfl) (λ hd tl ih x, - (hf (of x) (hd, tl)).trans $ congr_arg _ $ ih _) x +@[to_additive] lemma lift_of_mul (x y) : lift f (of x * y) = f x * lift f y := +by rw [map_mul, lift_of] end lift @@ -459,12 +455,13 @@ variables {β : Type v} (f : α → β) /-- The unique semigroup homomorphism that sends `of x` to `of (f x)`. -/ @[to_additive "The unique additive semigroup homomorphism that sends `of x` to `of (f x)`."] -def map : free_semigroup α → free_semigroup β := +def map : free_semigroup α →ₙ* free_semigroup β := lift $ of ∘ f @[simp, to_additive] lemma map_of (x) : map f (of x) = of (f x) := rfl -@[simp, to_additive] lemma map_mul (x y) : map f (x * y) = map f x * map f y := -lift_mul _ _ _ + +@[simp, to_additive] lemma length_map (x) : (map f x).length = x.length := +free_semigroup.rec_on_mul x (λ x, rfl) $ λ x y hx hy, by simp only [map_mul, length_mul, *] end map @@ -482,7 +479,7 @@ instance : monad free_semigroup := def rec_on_pure {C : free_semigroup α → Sort l} (x) (ih1 : ∀ x, C (pure x)) (ih2 : ∀ x y, C (pure x) → C y → C (pure x * y)) : C x := -free_semigroup.rec_on x ih1 ih2 +free_semigroup.rec_on_mul x ih1 ih2 @[simp, to_additive] lemma map_pure (f : α → β) (x) : (f <$> pure x : free_semigroup β) = pure (f x) := rfl @@ -490,7 +487,7 @@ lemma map_pure (f : α → β) (x) : (f <$> pure x : free_semigroup β) = pure ( @[simp, to_additive] lemma map_mul' (f : α → β) (x y : free_semigroup α) : (f <$> (x * y)) = (f <$> x * f <$> y) := -map_mul _ _ _ +map_mul (map f) _ _ @[simp, to_additive] lemma pure_bind (f : α → free_semigroup β) (x) : (pure x >>= f) = f x := rfl @@ -498,7 +495,7 @@ map_mul _ _ _ @[simp, to_additive] lemma mul_bind (f : α → free_semigroup β) (x y : free_semigroup α) : (x * y >>= f) = ((x >>= f) * (y >>= f)) := -lift_mul _ _ _ +map_mul (lift f) _ _ @[simp, to_additive] lemma pure_seq {f : α → β} {x : free_semigroup α} : pure f <*> x = f <$> x := rfl @@ -537,8 +534,8 @@ variables [is_lawful_applicative m] traverse F (x * y) = (*) <$> traverse F x <*> traverse F y := let ⟨x, L1⟩ := x, ⟨y, L2⟩ := y in list.rec_on L1 (λ x, rfl) (λ hd tl ih x, - show (*) <$> pure <$> F x <*> traverse F ((hd, tl) * (y, L2) : free_semigroup α) = - (*) <$> ((*) <$> pure <$> F x <*> traverse F (hd, tl)) <*> traverse F (y, L2), + show (*) <$> pure <$> F x <*> traverse F ((mk hd tl) * (mk y L2)) = + (*) <$> ((*) <$> pure <$> F x <*> traverse F (mk hd tl)) <*> traverse F (mk y L2), by rw ih; simp only [(∘), (mul_assoc _ _ _).symm] with functor_norm) x @[simp, to_additive] lemma traverse_mul' : @@ -554,7 +551,7 @@ end @[to_additive] instance : is_lawful_traversable free_semigroup.{u} := -{ id_traverse := λ α x, free_semigroup.rec_on x (λ x, rfl) +{ id_traverse := λ α x, free_semigroup.rec_on_mul x (λ x, rfl) (λ x y ih1 ih2, by rw [traverse_mul, ih1, ih2, mul_map_seq]), comp_traverse := λ F G hf1 hg1 hf2 hg2 α β γ f g x, rec_on_pure x (λ x, by resetI; simp only [traverse_pure, traverse_pure'] with functor_norm) @@ -563,35 +560,54 @@ instance : is_lawful_traversable free_semigroup.{u} := naturality := λ F G hf1 hg1 hf2 hg2 η α β f x, rec_on_pure x (λ x, by simp only [traverse_pure] with functor_norm) (λ x y ih1 ih2, by resetI; simp only [traverse_mul] with functor_norm; rw [ih1, ih2]), - traverse_eq_map_id := λ α β f x, free_semigroup.rec_on x (λ _, rfl) + traverse_eq_map_id := λ α β f x, free_semigroup.rec_on_mul x (λ _, rfl) (λ x y ih1 ih2, by rw [traverse_mul, ih1, ih2, map_mul', mul_map_seq]; refl), .. free_semigroup.is_lawful_monad } end category @[to_additive] -instance [decidable_eq α] : decidable_eq (free_semigroup α) := prod.decidable_eq +instance [decidable_eq α] : decidable_eq (free_semigroup α) := +λ x y, decidable_of_iff' _ (ext_iff _ _) end free_semigroup -/-- Isomorphism between `magma.free_semigroup (free_magma α)` and `free_semigroup α`. -/ +namespace free_magma + +variables {α : Type u} {β : Type v} + +/-- The canonical multiplicative morphism from `free_magma α` to `free_semigroup α`. -/ +@[to_additive "The canonical additive morphism from `free_add_magma α` to `free_add_semigroup α`."] +def to_free_semigroup : free_magma α →ₙ* free_semigroup α := free_magma.lift free_semigroup.of + +@[simp, to_additive] lemma to_free_semigroup_of (x : α) : + to_free_semigroup (of x) = free_semigroup.of x := +rfl + +@[simp, to_additive] lemma to_free_semigroup_comp_of : + @to_free_semigroup α ∘ of = free_semigroup.of := +rfl + +@[to_additive] lemma to_free_semigroup_comp_map (f : α → β) : + to_free_semigroup.comp (map f) = (free_semigroup.map f).comp to_free_semigroup := +by { ext1, refl } + +@[to_additive] lemma to_free_semigroup_map (f : α → β) (x : free_magma α) : + (map f x).to_free_semigroup = free_semigroup.map f x.to_free_semigroup := +fun_like.congr_fun (to_free_semigroup_comp_map f) x + +@[simp, to_additive] lemma length_to_free_semigroup (x : free_magma α) : + x.to_free_semigroup.length = x.length := +free_magma.rec_on_mul x (λ x, rfl) $ λ x y hx hy, + by rw [map_mul, free_semigroup.length_mul, length, hx, hy] + +end free_magma + +/-- Isomorphism between `magma.assoc_quotient (free_magma α)` and `free_semigroup α`. -/ @[to_additive "Isomorphism between -`add_magma.free_add_semigroup (free_add_magma α)` and `free_add_semigroup α`."] -def free_semigroup_free_magma (α : Type u) : - magma.free_semigroup (free_magma α) ≃ free_semigroup α := -{ to_fun := - magma.free_semigroup.lift (free_magma.lift free_semigroup.of) (free_magma.lift _).map_mul, - inv_fun := free_semigroup.lift (magma.free_semigroup.of ∘ free_magma.of), - left_inv := λ x, magma.free_semigroup.induction_on x $ λ p, by rw magma.free_semigroup.lift_of; - exact free_magma.rec_on_mul p - (λ x, by rw [free_magma.lift_of, free_semigroup.lift_of]) - (λ x y ihx ihy, by rw [mul_hom.map_mul, free_semigroup.lift_mul, ihx, ihy, - magma.free_semigroup.of_mul]), - right_inv := λ x, free_semigroup.rec_on x - (λ x, by rw [free_semigroup.lift_of, magma.free_semigroup.lift_of, free_magma.lift_of]) - (λ x y ihx ihy, by rw [free_semigroup.lift_mul, magma.free_semigroup.lift_mul, ihx, ihy]) } - -@[simp, to_additive] lemma free_semigroup_free_magma_mul {α : Type u} (x y) : - free_semigroup_free_magma α (x * y) = free_semigroup_free_magma α x * - free_semigroup_free_magma α y := -magma.free_semigroup.lift_mul _ _ _ +`add_magma.assoc_quotient (free_add_magma α)` and `free_add_semigroup α`."] +def free_magma_assoc_quotient_equiv (α : Type u) : + magma.assoc_quotient (free_magma α) ≃* free_semigroup α := +(magma.assoc_quotient.lift free_magma.to_free_semigroup).to_mul_equiv + (free_semigroup.lift (magma.assoc_quotient.of ∘ free_magma.of)) + (by { ext, refl }) (by { ext1, refl }) diff --git a/src/algebra/hom/equiv.lean b/src/algebra/hom/equiv.lean index b3b89a0c53361..8d3d4bcd95c3b 100644 --- a/src/algebra/hom/equiv.lean +++ b/src/algebra/hom/equiv.lean @@ -491,6 +491,23 @@ map_div h x y end mul_equiv +/-- Given a pair of multiplicative homomorphisms `f`, `g` such that `g.comp f = id` and +`f.comp g = id`, returns an multiplicative equivalence with `to_fun = f` and `inv_fun = g`. This +constructor is useful if the underlying type(s) have specialized `ext` lemmas for multiplicative +homomorphisms. -/ +@[to_additive /-"Given a pair of additive homomorphisms `f`, `g` such that `g.comp f = id` and +`f.comp g = id`, returns an additive equivalence with `to_fun = f` and `inv_fun = g`. This +constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive +homomorphisms."-/, simps {fully_applied := ff}] +def mul_hom.to_mul_equiv [has_mul M] [has_mul N] (f : M →ₙ* N) (g : N →ₙ* M) + (h₁ : g.comp f = mul_hom.id _) (h₂ : f.comp g = mul_hom.id _) : + M ≃* N := +{ to_fun := f, + inv_fun := g, + left_inv := mul_hom.congr_fun h₁, + right_inv := mul_hom.congr_fun h₂, + map_mul' := f.map_mul } + /-- Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`, returns an multiplicative equivalence with `to_fun = f` and `inv_fun = g`. This constructor is useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms. -/