kleeneAlgebra — Mathlib

English

Let α be a Kleene algebra and f: β → α an injective function. Then β admits a Kleene algebra structure obtained by pullback along f, with kstar on β compatible with that on α via f, i.e. f(a*) = f(a)* for all a ∈ β.

Русский

Пусть α — клинеева алгебра, и f: β → α — инъекция. Тогда β inherits Kleene algebra structure via перенос вдоль f, причём операция звёздочки на β согласуется с α: f(a*) = f(a)* для всех a ∈ β.

LaTeX

$$$\exists\text{ KleeneAlgebra on } \beta \text{ with } f(a^*) = (f(a))^* \text{ for all } a\in\beta.$$$

Lean4

/-- Pullback a `KleeneAlgebra` instance along an injective function. -/
protected abbrev kleeneAlgebra [KleeneAlgebra α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β]
    [Max β] [Bot β] [KStar β] (f : β → α) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) (sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) (kstar : ∀ a, f a∗ = (f a)∗) :
    KleeneAlgebra β :=
  { hf.idemSemiring f zero one add mul nsmul npow natCast sup bot,
    ‹KStar
        β› with
    one_le_kstar := fun a ↦
      one.trans_le <| by
        rw [kstar]
        exact one_le_kstar
    mul_kstar_le_kstar := fun a ↦ by
      change f _ ≤ _
      rw [mul, kstar]
      exact mul_kstar_le_kstar
    kstar_mul_le_kstar := fun a ↦ by
      change f _ ≤ _
      rw [mul, kstar]
      exact kstar_mul_le_kstar
    mul_kstar_le_self := fun a b (h : f _ ≤ _) ↦ by
      change f _ ≤ _
      rw [mul, kstar]
      rw [mul] at h
      exact mul_kstar_le_self h
    kstar_mul_le_self := fun a b (h : f _ ≤ _) ↦ by
      change f _ ≤ _
      rw [mul, kstar]
      rw [mul] at h
      exact kstar_mul_le_self h }

Похожие утверждения