English
There is a natural linear equivalence between the product ι → M and the space of linear maps (ι → R) → M, given by the π-construction.
Русский
Существует естественная линейная эквивалентность между произведением ι → M и пространством линейных отображений (ι → R) → M, задаваемая конструкцией π.
LaTeX
$$def piEquiv : (ι → M) ≃ₗ[R] ((ι → R) →ₗ[R] M)$$
Lean4
@[elab_as_elim]
theorem induction {motive : SymmetricAlgebra R M → Prop}
(algebraMap : ∀ r, motive (algebraMap R (SymmetricAlgebra R M) r)) (ι : ∀ x, motive (ι R M x))
(mul : ∀ a b, motive a → motive b → motive (a * b)) (add : ∀ a b, motive a → motive b → motive (a + b))
(a : SymmetricAlgebra R M) : motive a :=
by
rcases algHom_surjective _ _ a with ⟨a, rfl⟩
induction a using TensorAlgebra.induction with
| algebraMap r => rw [AlgHom.commutes]; exact algebraMap r
| ι x => exact ι x
| mul x y hx hy => rw [map_mul]; exact mul _ _ hx hy
| add x y hx hy => rw [map_add]; exact add _ _ hx hy
