English
Let C be a property of elements of TensorAlgebra R M. If C holds for all algebra maps algebraMap R (TensorAlgebra R M) r, for all r ∈ R; if C holds for all ι_R x with x ∈ M; and if C is closed under addition and multiplication, then C holds for every element of TensorAlgebra R M.
Русский
Пусть C — свойство элементов TensorAlgebra R M. Если C выполняется для всех отображений algebraMap R (TensorAlgebra R M) r, для всех r ∈ R, для всех x ∈ M в ι_R x и если C сохранено при сложении и умножении, то C выполняется для любого элемента TensorAlgebra R M.
LaTeX
$$$\\forall C: TensorAlgebra(R,M) \\to \\mathrm{Prop},\\ (\\forall r:\\, R, \\ C( algebraMap_R (TensorAlgebra R M) r))\\ \\land\\ (\\forall x:\\, M,\\ C( ι_R x))\\ \\land\\ (\\forall a,b:\\, TensorAlgebra R M,\\ C a \\to C b \\to C(a b))\\ \\land\\ (\\forall a,b:\\, TensorAlgebra R M,\\ C a \\to C b \\to C(a+b))\\ \\Rightarrow \\forall a:\\, TensorAlgebra R M,\\ C a$$$
Lean4
/-- If `C` holds for the `algebraMap` of `r : R` into `TensorAlgebra R M`, the `ι` of `x : M`,
and is preserved under addition and multiplication, then it holds for all of `TensorAlgebra R M`.
-/
@[elab_as_elim]
theorem induction {C : TensorAlgebra R M → Prop} (algebraMap : ∀ r, C (algebraMap R (TensorAlgebra R M) r))
(ι : ∀ x, C (ι R x)) (mul : ∀ a b, C a → C b → C (a * b)) (add : ∀ a b, C a → C b → C (a + b))
(a : TensorAlgebra R M) : C a := by
-- the arguments are enough to construct a subalgebra, and a mapping into it from M
let s : Subalgebra R (TensorAlgebra R M) :=
{ carrier := C
mul_mem' := @mul
add_mem' := @add
algebraMap_mem' := algebraMap }
let of : M →ₗ[R] s := (TensorAlgebra.ι R).codRestrict (Subalgebra.toSubmodule s) ι
have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) :=
by
ext
simp only [AlgHom.toLinearMap_id, LinearMap.id_comp, AlgHom.comp_toLinearMap, LinearMap.coe_comp,
Function.comp_apply, AlgHom.toLinearMap_apply, lift_ι_apply, Subalgebra.coe_val]
erw [LinearMap.codRestrict_apply]
-- finding a proof is finding an element of the subalgebra
rw [← AlgHom.id_apply (R := R) a, of_id]
exact Subtype.prop (lift R of a)
