Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2019 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Yury Kudryashov
! This file was ported from Lean 3 source module algebra.free_monoid.basic
! leanprover-community/mathlib commit 657df4339ae6ceada048c8a2980fb10e393143ec
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.BigOperators.Basic
/-!
# Free monoid over a given alphabet
## Main definitions
* `FreeMonoid α`: free monoid over alphabet `α`; defined as a synonym for `List α`
with multiplication given by `(++)`.
* `FreeMonoid.of`: embedding `α → FreeMonoid α` sending each element `x` to `[x]`;
* `FreeMonoid.lift`: natural equivalence between `α → M` and `FreeMonoid α →* M`
* `FreeMonoid.map`: embedding of `α → β` into `FreeMonoid α →* FreeMonoid β` given by `List.map`.
-/
variable { α : Type _ } { β : Type _ : Type (?u.12678+1)} { γ : Type _ } { M : Type _ } [ Monoid M ] { N : Type _ : Type (?u.55103+1)} [ Monoid N ]
/-- Free monoid over a given alphabet. -/
@[ to_additive "Free nonabelian additive monoid over a given alphabet"]
def FreeMonoid : (α : ?m.44 ) → ?m.48 α
FreeMonoid ( α ) := List α
#align free_monoid FreeMonoid
#align free_add_monoid FreeAddMonoid
namespace FreeMonoid
-- Porting note: TODO. Check this is still needed
@[ to_additive ]
instance [ DecidableEq : Sort ?u.84 → Sort (max1?u.84) α ] : DecidableEq : Sort ?u.93 → Sort (max1?u.93) ( FreeMonoid α ) := instDecidableEqList
/-- The identity equivalence between `FreeMonoid α` and `List α`. -/
@[ to_additive "The identity equivalence between `FreeAddMonoid α` and `List α`."]
def toList : FreeMonoid α ≃ List α := Equiv.refl : (α : Sort ?u.408) → α ≃ α _
#align free_monoid.to_list FreeMonoid.toList
#align free_add_monoid.to_list FreeAddMonoid.toList
/-- The identity equivalence between `List α` and `FreeMonoid α`. -/
@[ to_additive "The identity equivalence between `List α` and `FreeAddMonoid α`."]
def ofList : List α ≃ FreeMonoid α := Equiv.refl : (α : Sort ?u.506) → α ≃ α _
#align free_monoid.of_list FreeMonoid.ofList
#align free_add_monoid.of_list FreeAddMonoid.ofList
@[ to_additive : ∀ {α : Type u_1}, FreeAddMonoid.toList .symm= FreeAddMonoid.ofList to_additive ( attr := simp )]
theorem toList_symm : ∀ {α : Type u_1}, toList .symm= ofList toList_symm : (@ toList α ). symm : {α : Sort ?u.599} → {β : Sort ?u.598} → α ≃ β β ≃ α symm = ofList := rfl : ∀ {α : Sort ?u.646} {a : α }, a = a
#align free_monoid.to_list_symm FreeMonoid.toList_symm : ∀ {α : Type u_1}, toList .symm= ofList
#align free_add_monoid.to_list_symm FreeAddMonoid.toList_symm : ∀ {α : Type u_1}, FreeAddMonoid.toList .symm= FreeAddMonoid.ofList
@[ to_additive : ∀ {α : Type u_1}, FreeAddMonoid.ofList .symm= FreeAddMonoid.toList to_additive ( attr := simp )]
theorem ofList_symm : ∀ {α : Type u_1}, ofList .symm= toList ofList_symm : (@ ofList α ). symm : {α : Sort ?u.713} → {β : Sort ?u.712} → α ≃ β β ≃ α symm = toList := rfl : ∀ {α : Sort ?u.760} {a : α }, a = a
#align free_monoid.of_list_symm FreeMonoid.ofList_symm : ∀ {α : Type u_1}, ofList .symm= toList
#align free_add_monoid.of_list_symm FreeAddMonoid.ofList_symm : ∀ {α : Type u_1}, FreeAddMonoid.ofList .symm= FreeAddMonoid.toList
@[ to_additive : ∀ {α : Type u_1} (l : List α ↑FreeAddMonoid.toList (↑FreeAddMonoid.ofList l ) = l to_additive ( attr := simp )]
theorem toList_ofList : ∀ (l : List α ↑toList (↑ofList l ) = l toList_ofList ( l : List α ) : toList ( ofList l ) = l := rfl : ∀ {α : Sort ?u.992} {a : α }, a = a
#align free_monoid.to_list_of_list FreeMonoid.toList_ofList : ∀ {α : Type u_1} (l : List α ↑toList (↑ofList l ) = l
#align free_add_monoid.to_list_of_list FreeAddMonoid.toList_ofList : ∀ {α : Type u_1} (l : List α ↑FreeAddMonoid.toList (↑FreeAddMonoid.ofList l ) = l
@[ to_additive : ∀ {α : Type u_1} (xs : FreeAddMonoid α ↑FreeAddMonoid.ofList (↑FreeAddMonoid.toList xs ) = xs to_additive ( attr := simp )]
theorem ofList_toList : ∀ (xs : FreeMonoid α ↑ofList (↑toList xs ) = xs ofList_toList ( xs : FreeMonoid α ) : ofList ( toList xs ) = xs := rfl : ∀ {α : Sort ?u.1247} {a : α }, a = a
#align free_monoid.of_list_to_list FreeMonoid.ofList_toList : ∀ {α : Type u_1} (xs : FreeMonoid α ↑ofList (↑toList xs ) = xs
#align free_add_monoid.of_list_to_list FreeAddMonoid.ofList_toList : ∀ {α : Type u_1} (xs : FreeAddMonoid α ↑FreeAddMonoid.ofList (↑FreeAddMonoid.toList xs ) = xs
@[ to_additive : ∀ {α : Type u_1}, ↑FreeAddMonoid.toList ∘ ↑FreeAddMonoid.ofList = id to_additive ( attr := simp )]
theorem toList_comp_ofList : ↑toList ∘ ↑ofList = id toList_comp_ofList : @ toList α ∘ ofList = id : {α : Sort ?u.1504} → α → α := rfl : ∀ {α : Sort ?u.1545} {a : α }, a = a
#align free_monoid.to_list_comp_of_list FreeMonoid.toList_comp_ofList : ∀ {α : Type u_1}, ↑toList ∘ ↑ofList = id
#align free_add_monoid.to_list_comp_of_list FreeAddMonoid.toList_comp_ofList : ∀ {α : Type u_1}, ↑FreeAddMonoid.toList ∘ ↑FreeAddMonoid.ofList = id
@[ to_additive : ∀ {α : Type u_1}, ↑FreeAddMonoid.ofList ∘ ↑FreeAddMonoid.toList = id to_additive ( attr := simp )]
theorem ofList_comp_toList : ↑ofList ∘ ↑toList = id ofList_comp_toList : @ ofList α ∘ toList = id : {α : Sort ?u.1810} → α → α := rfl : ∀ {α : Sort ?u.1852} {a : α }, a = a
#align free_monoid.of_list_comp_to_list FreeMonoid.ofList_comp_toList : ∀ {α : Type u_1}, ↑ofList ∘ ↑toList = id
#align free_add_monoid.of_list_comp_to_list FreeAddMonoid.ofList_comp_toList : ∀ {α : Type u_1}, ↑FreeAddMonoid.ofList ∘ ↑FreeAddMonoid.toList = id
@[ to_additive ]
instance : CancelMonoid : Type ?u.1947 → Type ?u.1947 ( FreeMonoid α )
where
one := ofList []
mul x y := ofList ( toList x ++ toList y )
mul_one := List.append_nil : ∀ {α : Type ?u.3192} (as : List α as ++ [] = as
one_mul := List.nil_append : ∀ {α : Type ?u.3155} (as : List α [] ++ as = as
mul_assoc := List.append_assoc : ∀ {α : Type ?u.2277} (as bs cs : List α as ++ bs ++ cs = as ++ (bs ++ cs
mul_left_cancel _ _ _ := List.append_left_cancel : ∀ {α : Type ?u.2815} {s t₁ t₂ : List α s ++ t₁ = s ++ t₂ t₁ = t₂
mul_right_cancel _ _ _ := List.append_right_cancel : ∀ {α : Type ?u.3273} {s₁ s₂ t : List α s₁ ++ t = s₂ ++ t s₁ = s₂
@[ to_additive ]
instance : Inhabited : Sort ?u.4709 → Sort (max1?u.4709) ( FreeMonoid α ) := ⟨ 1 ⟩
@[ to_additive : ∀ {α : Type u_1}, ↑FreeAddMonoid.toList 0 = [] to_additive ( attr := simp )]
theorem toList_one : ↑toList 1 = [] toList_one : toList ( 1 : FreeMonoid α ) = [] := rfl : ∀ {α : Sort ?u.5610} {a : α }, a = a
#align free_monoid.to_list_one FreeMonoid.toList_one : ∀ {α : Type u_1}, ↑toList 1 = []
#align free_add_monoid.to_list_zero FreeAddMonoid.toList_zero : ∀ {α : Type u_1}, ↑FreeAddMonoid.toList 0 = []
@[ to_additive : ∀ {α : Type u_1}, ↑FreeAddMonoid.ofList [] = 0 to_additive ( attr := simp )]
theorem ofList_nil : ↑ofList [] = 1 ofList_nil : ofList ( [] : List α ) = 1 := rfl : ∀ {α : Sort ?u.6139} {a : α }, a = a
#align free_monoid.of_list_nil FreeMonoid.ofList_nil : ∀ {α : Type u_1}, ↑ofList [] = 1
#align free_add_monoid.of_list_nil FreeAddMonoid.ofList_nil : ∀ {α : Type u_1}, ↑FreeAddMonoid.ofList [] = 0
@[ to_additive : ∀ {α : Type u_1} (xs ys : FreeAddMonoid α ↑FreeAddMonoid.toList (xs + ys = ↑FreeAddMonoid.toList xs ++ ↑FreeAddMonoid.toList ys to_additive ( attr := simp )]
theorem toList_mul : ∀ (xs ys : FreeMonoid α ↑toList (xs * ys = ↑toList xs ++ ↑toList ys toList_mul ( xs ys : FreeMonoid α ) : toList ( xs * ys ) = toList xs ++ toList ys := rfl : ∀ {α : Sort ?u.6941} {a : α }, a = a
#align free_monoid.to_list_mul FreeMonoid.toList_mul : ∀ {α : Type u_1} (xs ys : FreeMonoid α ↑toList (xs * ys = ↑toList xs ++ ↑toList ys
#align free_add_monoid.to_list_add FreeAddMonoid.toList_add : ∀ {α : Type u_1} (xs ys : FreeAddMonoid α ↑FreeAddMonoid.toList (xs + ys = ↑FreeAddMonoid.toList xs ++ ↑FreeAddMonoid.toList ys
@[ to_additive : ∀ {α : Type u_1} (xs ys : List α ↑FreeAddMonoid.ofList (xs ++ ys = ↑FreeAddMonoid.ofList xs + ↑FreeAddMonoid.ofList ys to_additive ( attr := simp )]
theorem ofList_append : ∀ {α : Type u_1} (xs ys : List α ↑ofList (xs ++ ys = ↑ofList xs * ↑ofList ys ofList_append ( xs ys : List α ) : ofList ( xs ++ ys ) = ofList xs * ofList ys := rfl : ∀ {α : Sort ?u.8291} {a : α }, a = a
#align free_monoid.of_list_append FreeMonoid.ofList_append : ∀ {α : Type u_1} (xs ys : List α ↑ofList (xs ++ ys = ↑ofList xs * ↑ofList ys
#align free_add_monoid.of_list_append FreeAddMonoid.ofList_append : ∀ {α : Type u_1} (xs ys : List α ↑FreeAddMonoid.ofList (xs ++ ys = ↑FreeAddMonoid.ofList xs + ↑FreeAddMonoid.ofList ys
@[ to_additive ( attr := simp )]
theorem toList_prod ( xs : List ( FreeMonoid α )) : toList xs . prod : {α : Type ?u.8479} → [inst : Mul α [inst : One α List α α = ( xs . map toList ). join := by
induction xs <;> simp [*, List.join ]
#align free_monoid.to_list_prod FreeMonoid.toList_prod
#align free_add_monoid.to_list_sum FreeAddMonoid.toList_sum
@[ to_additive ( attr := simp )]
theorem ofList_join ( xs : List ( List α )) : ofList xs . join = ( xs . map ofList ). prod : {α : Type ?u.11090} → [inst : Mul α [inst : One α List α α prod :=
toList . injective <| by simp
#align free_monoid.of_list_join FreeMonoid.ofList_join
#align free_add_monoid.of_list_join FreeAddMonoid.ofList_join
/-- Embeds an element of `α` into `FreeMonoid α` as a singleton list. -/
@[ to_additive "Embeds an element of `α` into `FreeAddMonoid α` as a singleton list."]
def of ( x : α ) : FreeMonoid : Type ?u.12113 → Type ?u.12113 α := ofList [ x ]
#align free_monoid.of FreeMonoid.of
#align free_add_monoid.of FreeAddMonoid.of
@[ to_additive ( attr := simp )]
theorem toList_of : ∀ (x : α ), ↑toList (of x = [x ] toList_of ( x : α ) : toList ( of x ) = [ x ] := rfl : ∀ {α : Sort ?u.12474} {a : α }, a = a
#align free_monoid.to_list_of FreeMonoid.toList_of : ∀ {α : Type u_1} (x : α ), ↑toList (of x = [x ]
#align free_add_monoid.to_list_of FreeAddMonoid.toList_of
@[ to_additive ]
theorem ofList_singleton : ∀ {α : Type u_1} (x : α ), ↑ofList [x ] = of x ofList_singleton ( x : α ) : ofList [ x ] = of x := rfl : ∀ {α : Sort ?u.12651} {a : α }, a = a
#align free_monoid.of_list_singleton FreeMonoid.ofList_singleton : ∀ {α : Type u_1} (x : α ), ↑ofList [x ] = of x
#align free_add_monoid.of_list_singleton FreeAddMonoid.ofList_singleton
@[ to_additive ( attr := simp )]
theorem ofList_cons : ∀ (x : α ) (xs : List α ↑ofList (x :: xs = of x * ↑ofList xs ofList_cons ( x : α ) ( xs : List α ) : ofList ( x :: xs ) = of x * ofList xs := rfl : ∀ {α : Sort ?u.13676} {a : α }, a = a
#align free_monoid.of_list_cons FreeMonoid.ofList_cons : ∀ {α : Type u_1} (x : α ) (xs : List α ↑ofList (x :: xs = of x * ↑ofList xs
#align free_add_monoid.of_list_cons FreeAddMonoid.ofList_cons : ∀ {α : Type u_1} (x : α ) (xs : List α ↑FreeAddMonoid.ofList (x :: xs = FreeAddMonoid.of x + ↑FreeAddMonoid.ofList xs
@[ to_additive ]
theorem toList_of_mul : ∀ (x : α ) (xs : FreeMonoid α ↑toList (of x * xs = x :: ↑toList xs toList_of_mul ( x : α ) ( xs : FreeMonoid : Type ?u.13791 → Type ?u.13791 α ) : toList ( of x * xs ) = x :: toList xs := rfl : ∀ {α : Sort ?u.14387} {a : α }, a = a
#align free_monoid.to_list_of_mul FreeMonoid.toList_of_mul : ∀ {α : Type u_1} (x : α ) (xs : FreeMonoid α ↑toList (of x * xs = x :: ↑toList xs
#align free_add_monoid.to_list_of_add FreeAddMonoid.toList_of_add
@[ to_additive ]
theorem of_injective : Function.Injective : {α : Sort ?u.14455} → {β : Sort ?u.14454} → (α → β Prop (@ of α ) := List.singleton_injective
#align free_monoid.of_injective FreeMonoid.of_injective
#align free_add_monoid.of_injective FreeAddMonoid.of_injective
/-- Recursor for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of `[]` and `x :: xs`. -/
@[ to_additive ( attr := elab_as_elim) "Recursor for `FreeAddMonoid` using `0` and
`FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."]
-- Porting note: change from `List.recOn` to `List.rec` since only the latter is computable
def recOn { C : FreeMonoid : Type ?u.14502 → Type ?u.14502 α → Sort _ } ( xs : FreeMonoid : Type ?u.14507 → Type ?u.14507 α ) ( h0 : C 1 )
( ih : ∀ x xs , C xs → C ( of x * xs )) : C xs := List.rec : {α : Type ?u.15210} →
{motive : List α Sort ?u.15211motive [] ((head : α ) → (tail : List α motive tail motive (head :: tail ) → (t : List α motive t h0 ih xs
#align free_monoid.rec_on FreeMonoid.recOn
#align free_add_monoid.rec_on FreeAddMonoid.recOn
@[ to_additive ( attr := simp )]
theorem recOn_one { C : FreeMonoid : Type ?u.15615 → Type ?u.15615 α → Sort _ } ( h0 : C 1 ) ( ih : ∀ x xs , C xs → C ( of x * xs )) :
@ recOn α C 1 h0 ih = h0 := rfl : ∀ {α : Sort ?u.16656} {a : α }, a = a
#align free_monoid.rec_on_one FreeMonoid.recOn_one
#align free_add_monoid.rec_on_zero FreeAddMonoid.recOn_zero
@[ to_additive ( attr := simp )]
theorem recOn_of_mul { C : FreeMonoid : Type ?u.16763 → Type ?u.16763 α → Sort _ } ( x : α ) ( xs : FreeMonoid : Type ?u.16770 → Type ?u.16770 α ) ( h0 : C 1 )
( ih : ∀ x xs , C xs → C ( of x * xs )) : @ recOn α C ( of x * xs ) h0 ih = ih x xs ( recOn xs h0 ih ) :=
rfl : ∀ {α : Sort ?u.18157} {a : α }, a = a
#align free_monoid.rec_on_of_mul FreeMonoid.recOn_of_mul
#align free_add_monoid.rec_on_of_add FreeAddMonoid.recOn_of_add
/-- A version of `List.cases_on` for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of
`[]` and `x :: xs`. -/
@[ to_additive ( attr := elab_as_elim) "A version of `List.casesOn` for `FreeAddMonoid` using `0` and
`FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."]
def casesOn { C : FreeMonoid : Type ?u.18333 → Type ?u.18333 α → Sort _ } ( xs : FreeMonoid : Type ?u.18338 → Type ?u.18338 α ) ( h0 : C 1 )
( ih : ∀ x xs , C ( of x * xs )) : C xs := List.casesOn : {α : Type ?u.19043} →
{motive : List α Sort ?u.19044(t : List α motive [] ((head : α ) → (tail : List α motive (head :: tail ) → motive t xs h0 ih
#align free_monoid.cases_on FreeMonoid.casesOn
#align free_add_monoid.cases_on FreeAddMonoid.casesOn
@[ to_additive ( attr := simp )]
theorem casesOn_one { C : FreeMonoid : Type ?u.19408 → Type ?u.19408 α → Sort _ } ( h0 : C 1 ) ( ih : (x : ?m.19696 ) → (xs : ?m.19747 x C (of x * xs ih : ∀ x xs , C ( of x * xs )) :
@ casesOn α C 1 h0 ih : (x : ?m.19696 ) → (xs : ?m.19747 x C (of x * xs ih = h0 := rfl : ∀ {α : Sort ?u.20448} {a : α }, a = a
#align free_monoid.cases_on_one FreeMonoid.casesOn_one
#align free_add_monoid.cases_on_zero FreeAddMonoid.casesOn_zero
@[ to_additive ( attr := simp )]
theorem casesOn_of_mul { C : FreeMonoid : Type ?u.20549 → Type ?u.20549 α → Sort _ } ( x : α ) ( xs : FreeMonoid : Type ?u.20556 → Type ?u.20556 α ) ( h0 : C 1 )
( ih : (x : ?m.20842 ) → (xs : ?m.20893 x C (of x * xs ih : ∀ x xs , C ( of x * xs )) : @ casesOn α C ( of x * xs ) h0 ih : (x : ?m.20842 ) → (xs : ?m.20893 x C (of x * xs ih = ih : (x : ?m.20842 ) → (xs : ?m.20893 x C (of x * xs ih x xs := rfl : ∀ {α : Sort ?u.21905} {a : α }, a = a
#align free_monoid.cases_on_of_mul FreeMonoid.casesOn_of_mul
#align free_add_monoid.cases_on_of_add FreeAddMonoid.casesOn_of_add
@[ to_additive ( attr := ext )]
theorem hom_eq ⦃ f g : FreeMonoid : Type ?u.22553 → Type ?u.22553 α →* M ⦄ ( h : ∀ (x : α ), ↑f (of x = ↑g (of x h : ∀ x , f ( of x ) = g ( of x )) : f = g :=
MonoidHom.ext fun l ↦ recOn l ( f . map_one . trans : ∀ {α : Sort ?u.23732} {a b c : α }, a = b b = c a = c g . map_one . symm : ∀ {α : Sort ?u.23751} {a b : α }, a = b b = a )
( fun x xs hxs ↦ by simp only [ h : ∀ (x : α ), ↑f (of x = ↑g (of x h , hxs , MonoidHom.map_mul ] )
#align free_monoid.hom_eq FreeMonoid.hom_eq
#align free_add_monoid.hom_eq FreeAddMonoid.hom_eq
/-- A variant of `List.prod` that has `[x].prod = x` true definitionally.
The purpose is to make `FreeMonoid.lift_eval_of` true by `rfl`. -/
@[ to_additive "A variant of `List.sum` that has `[x].sum = x` true definitionally.
The purpose is to make `FreeAddMonoid.lift_eval_of` true by `rfl`."]
def prodAux { M } [ Monoid M ] : List M → M
| [] => 1
| ( x :: xs ) => List.foldl : {α : Type ?u.24574} → {β : Type ?u.24573} → (α → β → α α → List β α (· * ·) x xs
#align free_monoid.prod_aux FreeMonoid.prodAux
#align free_add_monoid.sum_aux FreeAddMonoid.sumAux
@[ to_additive ]
lemma prodAux_eq : ∀ l : List M , FreeMonoid.prodAux : {M : Type ?u.25683} → [inst : Monoid M List M M l = l . prod : {α : Type ?u.25696} → [inst : Mul α [inst : One α List α α
| [] => rfl : ∀ {α : Sort ?u.26301} {a : α }, a = a
| (_ :: xs ) => congr_arg : ∀ {α : Sort ?u.26348} {β : Sort ?u.26347} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ ( fun x => List.foldl : {α : Type ?u.26357} → {β : Type ?u.26356} → (α → β → α α → List β α (· * ·) x xs ) ( one_mul _ ). symm : ∀ {α : Sort ?u.26804} {a b : α }, a = b b = a symm
#align free_monoid.prod_aux_eq FreeMonoid.prodAux_eq
#align free_add_monoid.sum_aux_eq FreeAddMonoid.sumAux_eq
/-- Equivalence between maps `α → M` and monoid homomorphisms `FreeMonoid α →* M`. -/
@[ to_additive "Equivalence between maps `α → A` and additive monoid homomorphisms
`FreeAddMonoid α →+ A`."]
def lift : ( α → M ) ≃ ( FreeMonoid : Type ?u.27424 → Type ?u.27424 α →* M ) where
toFun f :=
{ toFun := fun l ↦ prodAux (( toList l ). map f )
map_one' := rfl : ∀ {α : Sort ?u.28563} {a : α }, a = a
map_mul' := fun _ _ ↦ by simp only [ prodAux_eq , toList_mul : ∀ {α : Type ?u.29576} (xs ys : FreeMonoid α ↑toList (xs * ys = ↑toList xs ++ ↑toList ys , List.map_append , List.prod_append ] }
invFun f x := f ( of x )
left_inv f := rfl : ∀ {α : Sort ?u.28924} {a : α }, a = a
right_inv f := hom_eq fun x ↦ rfl : ∀ {α : Sort ?u.29091} {a : α }, a = a
#align free_monoid.lift FreeMonoid.lift
#align free_add_monoid.lift FreeAddMonoid.lift
-- porting note: new
@[ to_additive ( attr := simp )]
theorem lift_ofList ( f : α → M ) ( l : List α ) : lift f ( ofList l ) = ( l . map f ). prod : {α : Type ?u.31070} → [inst : Mul α [inst : One α List α α prod :=
prodAux_eq _
@[ to_additive ( attr := simp )]
theorem lift_symm_apply ( f : FreeMonoid : Type ?u.31994 → Type ?u.31994 α →* M ) : lift . symm : {α : Sort ?u.32515} → {β : Sort ?u.32514} → α ≃ β β ≃ α f = f ∘ of := rfl : ∀ {α : Sort ?u.32966} {a : α }, a = a
#align free_monoid.lift_symm_apply FreeMonoid.lift_symm_apply
#align free_add_monoid.lift_symm_apply FreeAddMonoid.lift_symm_apply
@[ to_additive ]
theorem lift_apply ( f : α → M ) ( l : FreeMonoid : Type ?u.33096 → Type ?u.33096 α ) : lift f l = (( toList l ). map f ). prod : {α : Type ?u.33642} → [inst : Mul α [inst : One α List α α prod :=
prodAux_eq _
#align free_monoid.lift_apply FreeMonoid.lift_apply
#align free_add_monoid.lift_apply FreeAddMonoid.lift_apply
@[ to_additive : ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M f : α → M ↑(↑FreeAddMonoid.lift f ) ∘ FreeAddMonoid.of = f to_additive ]
theorem lift_comp_of : ∀ (f : α → M ↑(↑lift f ) ∘ of = f lift_comp_of ( f : α → M ) : lift f ∘ of = f := rfl : ∀ {α : Sort ?u.34934} {a : α }, a = a
#align free_monoid.lift_comp_of FreeMonoid.lift_comp_of : ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M f : α → M ↑(↑lift f ) ∘ of = f
#align free_add_monoid.lift_comp_of FreeAddMonoid.lift_comp_of : ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M f : α → M ↑(↑FreeAddMonoid.lift f ) ∘ FreeAddMonoid.of = f
@[ to_additive ( attr := simp )]
theorem lift_eval_of : ∀ (f : α → M x : α ), ↑(↑lift f ) (of x = f x lift_eval_of ( f : α → M ) ( x : α ) : lift f ( of x ) = f x := rfl : ∀ {α : Sort ?u.35510} {a : α }, a = a
#align free_monoid.lift_eval_of FreeMonoid.lift_eval_of : ∀ {α : Type u_2} {M : Type u_1} [inst : Monoid M f : α → M x : α ), ↑(↑lift f ) (of x = f x
#align free_add_monoid.lift_eval_of FreeAddMonoid.lift_eval_of
@[ to_additive ( attr := simp )]
theorem lift_restrict ( f : FreeMonoid : Type ?u.35698 → Type ?u.35698 α →* M ) : lift ( f ∘ of ) = f := lift . apply_symm_apply : ∀ {α : Sort ?u.36661} {β : Sort ?u.36660} (e : α ≃ β x : β ), ↑e (↑e .symmx ) = x f
#align free_monoid.lift_restrict FreeMonoid.lift_restrict
#align free_add_monoid.lift_restrict FreeAddMonoid.lift_restrict
@[ to_additive ]
theorem comp_lift ( g : M →* N ) ( f : α → M ) : g . comp ( lift f ) = lift ( g ∘ f ) :=
-- Porting note: replace ext by FreeMonoid.hom_eq
FreeMonoid.hom_eq ( by simp )
#align free_monoid.comp_lift FreeMonoid.comp_lift
#align free_add_monoid.comp_lift FreeAddMonoid.comp_lift
@[ to_additive ]
theorem hom_map_lift ( g : M →* N ) ( f : α → M ) ( x : FreeMonoid : Type ?u.41174 → Type ?u.41174 α ) : g ( lift f x ) = lift ( g ∘ f ) x :=
FunLike.ext_iff : ∀ {F : Sort ?u.42670} {α : Sort ?u.42672} {β : α → Sort ?u.42671i : FunLike F α β f g : F },
f = g ↔ ∀ (x : α ), ↑f x = ↑g x . 1 : ∀ {a b : Prop }, (a ↔ b a → b ( comp_lift g f ) x
#align free_monoid.hom_map_lift FreeMonoid.hom_map_lift : ∀ {α : Type u_3} {M : Type u_1} [inst : Monoid M N : Type u_2} [inst_1 : Monoid N g : M →* N f : α → M x : FreeMonoid α ↑g (↑(↑lift f ) x ) = ↑(↑lift (↑g ∘ f ) x
#align free_add_monoid.hom_map_lift FreeAddMonoid.hom_map_lift
/-- Define a multiplicative action of `FreeMonoid α` on `β`. -/
@[ to_additive "Define an additive action of `FreeAddMonoid α` on `β`."]
def mkMulAction ( f : α → β → β ) : MulAction : (α : Type ?u.43342) → Type ?u.43341 → [inst : Monoid α Type (max?u.43342?u.43341) ( FreeMonoid : Type ?u.43343 → Type ?u.43343 α ) β where
smul l b := l . toList . foldr : {α : Type ?u.43699} → {β : Type ?u.43698} → (α → β → β β → List α β f b
one_smul _ := rfl : ∀ {α : Sort ?u.43721} {a : α }, a = a
mul_smul _ _ _ := List.foldr_append _ : ?m.43761 → ?m.43762 → ?m.43762
_ _ _
#align free_monoid.mk_mul_action FreeMonoid.mkMulAction
#align free_add_monoid.mk_add_action FreeAddMonoid.mkAddAction
@[ to_additive ]
theorem smul_def ( f : α → β → β ) ( l : FreeMonoid : Type ?u.44664 → Type ?u.44664 α ) ( b : β ) :
haveI := mkMulAction f
l • b = l . toList . foldr : {α : Type ?u.45648} → {β : Type ?u.45647} → (α → β → β β → List α β f b := rfl : ∀ {α : Sort ?u.45668} {a : α }, a = a
#align free_monoid.smul_def FreeMonoid.smul_def
#align free_add_monoid.vadd_def FreeAddMonoid.vadd_def
@[ to_additive : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β l : List α b : β ), ↑FreeAddMonoid.ofList l +ᵥ b = List.foldr f b l to_additive ]
theorem ofList_smul ( f : α → β → β ) ( l : List α ) ( b : β ) :
haveI := mkMulAction f
ofList l • b = l . foldr : {α : Type ?u.46836} → {β : Type ?u.46835} → (α → β → β β → List α β f b := rfl : ∀ {α : Sort ?u.46855} {a : α }, a = a
#align free_monoid.of_list_smul FreeMonoid.ofList_smul : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β l : List α b : β ), ↑ofList l • b = List.foldr f b l
#align free_add_monoid.of_list_vadd FreeAddMonoid.ofList_vadd : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β l : List α b : β ), ↑FreeAddMonoid.ofList l +ᵥ b = List.foldr f b l
@[ to_additive ( attr := simp )]
theorem of_smul : ∀ (f : α → β → β x : α ) (y : β ), of x • y = f x y of_smul ( f : α → β → β ) ( x : α ) ( y : β ) :
( haveI := mkMulAction f
of x • y ) = f x y := rfl : ∀ {α : Sort ?u.47849} {a : α }, a = a
#align free_monoid.of_smul FreeMonoid.of_smul : ∀ {α : Type u_2} {β : Type u_1} (f : α → β → β x : α ) (y : β ), of x • y = f x y
#align free_add_monoid.of_vadd FreeAddMonoid.of_vadd
/-- The unique monoid homomorphism `FreeMonoid α →* FreeMonoid β` that sends
each `of x` to `of (f x)`. -/
@[ to_additive "The unique additive monoid homomorphism `FreeAddMonoid α →+ FreeAddMonoid β`
that sends each `of x` to `of (f x)`."]
def map ( f : α → β ) : FreeMonoid : Type ?u.47969 → Type ?u.47969 α →* FreeMonoid : Type ?u.47970 → Type ?u.47970 β
where
toFun l := ofList <| l . toList . map f
map_one' := rfl : ∀ {α : Sort ?u.49166} {a : α }, a = a
map_mul' _ _ := List.map_append _ _ _
#align free_monoid.map FreeMonoid.map
#align free_add_monoid.map FreeAddMonoid.map
@[ to_additive ( attr := simp )]
theorem map_of : ∀ (f : α → β x : α ), ↑(map f of x = of (f x map_of ( f : α → β ) ( x : α ) : map f ( of x ) = of ( f x ) := rfl : ∀ {α : Sort ?u.51605} {a : α }, a = a
#align free_monoid.map_of FreeMonoid.map_of : ∀ {α : Type u_2} {β : Type u_1} (f : α → β x : α ), ↑(map f of x = of (f x
#align free_add_monoid.map_of FreeAddMonoid.map_of
@[ to_additive ]
theorem toList_map ( f : α → β ) ( xs : FreeMonoid : Type ?u.51742 → Type ?u.51742 α ) : toList ( map f xs ) = xs . toList . map f := rfl : ∀ {α : Sort ?u.52230} {a : α }, a = a
#align free_monoid.to_list_map FreeMonoid.toList_map
#align free_add_monoid.to_list_map FreeAddMonoid.toList_map
@[ to_additive ]
theorem ofList_map ( f : α → β ) ( xs : List α ) : ofList ( xs . map f ) = map f ( ofList xs ) := rfl : ∀ {α : Sort ?u.52832} {a : α }, a = a
#align free_monoid.of_list_map FreeMonoid.ofList_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β xs : List α ↑ofList (List.map f xs = ↑(map f ↑ofList xs )
#align free_add_monoid.of_list_map FreeAddMonoid.ofList_map
@[ to_additive ]
theorem lift_of_comp_eq_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β (↑lift fun x => of (f x ) = map f lift_of_comp_eq_map ( f : α → β ) : ( lift fun x ↦ of ( f x )) = map f := hom_eq fun _ ↦ rfl : ∀ {α : Sort ?u.53334} {a : α }, a = a
#align free_monoid.lift_of_comp_eq_map FreeMonoid.lift_of_comp_eq_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β (↑lift fun x => of (f x ) = map f
#align free_add_monoid.lift_of_comp_eq_map FreeAddMonoid.lift_of_comp_eq_map
@[ to_additive ]
theorem map_comp ( g : β → γ ) ( f : α → β ) : map ( g ∘ f ) = ( map g ). comp ( map f ) := hom_eq fun _ ↦ rfl : ∀ {α : Sort ?u.54704} {a : α }, a = a
#align free_monoid.map_comp FreeMonoid.map_comp
#align free_add_monoid.map_comp FreeAddMonoid.map_comp
@[ to_additive ( attr := simp )]
theorem map_id : map (@ id : {α : Sort ?u.55114} → α → α α ) = MonoidHom.id ( FreeMonoid : Type ?u.55118 → Type ?u.55118 α ) := hom_eq fun _ ↦ rfl : ∀ {α : Sort ?u.55442} {a : α }, a = a
#align free_monoid.map_id FreeMonoid.map_id
#align free_add_monoid.map_id FreeAddMonoid.map_id
end FreeMonoid