English
Let R be a commutative semiring and X a type. For any predicate P on FreeAlgebra R X, if P holds for algebraMap(r) for all r ∈ R, and for ι_R(x) for all x ∈ X, and P is preserved under addition and multiplication, then P holds for all elements of FreeAlgebra R X.
Русский
Пусть R — коммутативная полукольца, X — множество. Для любого предиката P над FreeAlgebra R X, если P выполняется для algebraMap r для всех r ∈ R и для ι_R(x) для всех x ∈ X, и если P сохраняется при сложении и умножении, то P выполняется для всех элементов FreeAlgebra R X.
LaTeX
$$$\\forall P: FreeAlgebra\\,R\\,X \\to \\mathrm{Prop},\\; (\\forall r:\\,R,\\ P( algebraMap\\ R\\ (FreeAlgebra\\ R\\ X)\\ r)) \\\\quad\\land (\\forall x:\\,X,\\ P( ι\\ R\\ x)) \\\\quad\\land (\\forall a\, b,\\ P a \\to P b \\to P (a+b)) \\\\quad\\land (\\forall a\, b,\\ P a \\to P b \\to P (a*b)) \\\\quad\\Rightarrow (\\forall a:\\, FreeAlgebra\\,R\\ X,\\ P a) $$$
Lean4
/-- An induction principle for the free algebra.
If `C` holds for the `algebraMap` of `r : R` into `FreeAlgebra R X`, the `ι` of `x : X`, and is
preserved under addition and multiplication, then it holds for all of `FreeAlgebra R X`.
-/
@[elab_as_elim, induction_eliminator]
theorem induction {motive : FreeAlgebra R X → Prop} (grade0 : ∀ r, motive (algebraMap R (FreeAlgebra R X) r))
(grade1 : ∀ x, motive (ι R x)) (mul : ∀ a b, motive a → motive b → motive (a * b))
(add : ∀ a b, motive a → motive b → motive (a + b)) (a : FreeAlgebra R X) : motive a := by
-- the arguments are enough to construct a subalgebra, and a mapping into it from X
let s : Subalgebra R (FreeAlgebra R X) :=
{ carrier := motive
mul_mem' := mul _ _
add_mem' := add _ _
algebraMap_mem' := grade0 }
let of : X → s := Subtype.coind (ι R) grade1
have of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp (lift R of) :=
by
ext
simp [of, Subtype.coind]
-- finding a proof is finding an element of the subalgebra
suffices a = lift R of a by
rw [this]
exact Subtype.prop (lift R of a)
simp [AlgHom.ext_iff] at of_id
exact of_id a
