Language homomorphism

structure Language.Hom (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

A language homomorphism from α to β is a map from List α to List β which preserves the empty word [] and concatenation (· ++ ·).

• toFun : List α → List β

  The map of a language homomorphism.

• map_nil' : self.toFun [] = []
• map_append' (as as' : List α) : self.toFun (as ++ as') = self.toFun as ++ self.toFun as'

theorem Language.Hom.ext_iff {α : Type u_3} {β : Type u_4} {x y : Hom α β} : x = y ↔ x.toFun = y.toFun

theorem Language.Hom.ext {α : Type u_3} {β : Type u_4} {x y : Hom α β} (toFun : x.toFun = y.toFun) : x = y

@[instance_reducible]

instance Language.instFunLikeHomList {α : Type u_1} {β : Type u_2} : FunLike (Hom α β) (List α) (List β)

This is to support the function application notation for language homomorphisms.

Equations

• Language.instFunLikeHomList = { coe := fun (f : Language.Hom α β) => f.toFun, coe_injective := ⋯ }

theorem Language.Hom.ext_iff' {α : Type u_1} {β : Type u_2} (f f' : Hom α β) : f = f' ↔ ∀ (as : List α), f as = f' as

@[simp]

theorem Language.Hom.map_nil {α : Type u_1} {β : Type u_2} (f : Hom α β) : f [] = []

@[simp]

theorem Language.Hom.map_append {α : Type u_1} {β : Type u_2} (f : Hom α β) (as as' : List α) : f (as ++ as') = f as ++ f as'

theorem Language.Hom.map_cons {α : Type u_1} {β : Type u_2} (f : Hom α β) (a : α) (as : List α) : f (a :: as) = f [a] ++ f as

def Language.Hom.liftAux {α : Type u_1} {β : Type u_2} (f : α → List β) : Hom α β

This auxiliary function should not be used outside this file. Instead, use the equivalence lift below.

Equations

• Language.Hom.liftAux f = { toFun := List.flatMap f, map_nil' := ⋯, map_append' := ⋯ }

theorem Language.Hom.liftAux_eq_flatMap {α : Type u_1} {β : Type u_2} (f : α → List β) : ⇑(liftAux f) = List.flatMap f

theorem Language.Hom.listAux_left_inv {α : Type u_1} {β : Type u_2} (f : α → List β) : (fun (f : Hom α β) (a : α) => f [a]) (liftAux f) = f

theorem Language.Hom.listAux_right_inv {α : Type u_1} {β : Type u_2} (f : Hom α β) : (liftAux fun (a : α) => f [a]) = f

def Language.Hom.lift {α : Type u_1} {β : Type u_2} : (α → List β) ≃ Hom α β

An equivalence from f : α → List β to Hom α β, whose forward direction can be used to define language homomorphisms conveniently.

Equations

• Language.Hom.lift = { toFun := Language.Hom.liftAux, invFun := fun (f : Language.Hom α β) (a : α) => f [a], left_inv := ⋯, right_inv := ⋯ }

theorem Language.Hom.lift_eq_flatMap {α : Type u_1} {β : Type u_2} (f : α → List β) : ⇑(lift f) = List.flatMap f

lift.toFun is in fact List.flatMap.

def Language.image {α : Type u_1} {β : Type u_2} (f : List α → List β) (l : Language α) : Language β

The image of a language under a function f, which need not be a language homomorphism.

Equations

• Language.image f l = f '' l

def Language.preimage {α : Type u_1} {β : Type u_2} (f : List α → List β) (l : Language β) : Language α

The preimage of a language under a function f, which need not be a language homomorphism.

Equations

• Language.preimage f l = f ⁻¹' l

@[simp]

theorem Language.mem_image {α : Type u_1} {β : Type u_2} (f : List α → List β) (l : Language α) (bs : List β) : bs ∈ image f l ↔ ∃ as ∈ l, f as = bs

@[simp]

theorem Language.mem_preimage {α : Type u_1} {β : Type u_2} (f : List α → List β) (l : Language β) (as : List α) : as ∈ preimage f l ↔ f as ∈ l

theorem Language.image_singleton {α : Type u_1} {β : Type u_2} (f : List α → List β) (as : List α) : image f {as} = {f as}

@[simp]

theorem Language.image_zero {α : Type u_1} {β : Type u_2} (f : List α → List β) : image f 0 = 0

theorem Language.image_add {α : Type u_1} {β : Type u_2} (f : List α → List β) (l1 l2 : Language α) : image f (l1 + l2) = image f l1 + image f l2

theorem Language.image_iSup {α : Type u_1} {β : Type u_2} (f : List α → List β) {I : Type u_3} (l : I → Language α) : image f (⨆ (i : I), l i) = ⨆ (i : I), image f (l i)

The following distributive laws for the image operation requires the function f to be a language homomorphism.

theorem Language.image_one {α : Type u_1} {β : Type u_2} (f : Hom α β) : image (⇑f) 1 = 1

theorem Language.image_mul {α : Type u_1} {β : Type u_2} (f : Hom α β) (l1 l2 : Language α) : image (⇑f) (l1 * l2) = image (⇑f) l1 * image (⇑f) l2

theorem Language.image_pow {α : Type u_1} {β : Type u_2} (f : Hom α β) (l : Language α) (n : ℕ) : image (⇑f) (l ^ n) = image (⇑f) l ^ n

theorem Language.image_kstar {α : Type u_1} {β : Type u_2} (f : Hom α β) (l : Language α) : image (⇑f) (KStar.kstar l) = KStar.kstar (image (⇑f) l)