Commit 2020-06-17 11:06 077cd7c0

View on Github →

feat(algebra/category/Algebra): basic setup for category of bundled R-algebras (#3047) Just boilerplate. If I don't run out of enthusiasm I'll do tensor product of R-algebras soon. (#3050)

Estimated changes

Created src/algebra/category/Algebra/basic.lean

added theorem Algebra.coe_comp

added theorem Algebra.id_apply

added def Algebra.of

added theorem Algebra.of_apply

added def Algebra.of_self_iso

added structure Algebra

added def alg_equiv.to_Algebra_iso

added def alg_equiv_iso_Algebra_iso

added def category_theory.iso.to_alg_equiv

Modified src/algebra/category/Module/basic.lean

deleted def linear_equiv_iso_Group_iso

added def linear_equiv_iso_Module_iso

Modified src/ring_theory/algebra.lean

added theorem alg_equiv.coe_fun_injective

added theorem alg_equiv.coe_ring_equiv_injective

added theorem alg_equiv.ext