Commit 2024-10-28 13:33 ed81cec6

View on Github →

feat(Algebra/Module): presentation of modules (#18295) This PR defines a basic API for the description of modules in terms of generators and relations.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Presentation/Basic.lean

added structure Module.Presentation

added theorem Module.Relations.Solution.IsPresentation.desc_var

added theorem Module.Relations.Solution.IsPresentation.exact

added theorem Module.Relations.Solution.IsPresentation.ker_π

added theorem Module.Relations.Solution.IsPresentation.linearEquiv_apply

added theorem Module.Relations.Solution.IsPresentation.linearEquiv_symm_var

added theorem Module.Relations.Solution.IsPresentation.postcomp_injective

added theorem Module.Relations.Solution.IsPresentation.surjective_mapToKer

added theorem Module.Relations.Solution.IsPresentation.surjective_π

added structure Module.Relations.Solution.IsPresentation

added theorem Module.Relations.Solution.fromQuotient_comp_toQuotient

added theorem Module.Relations.Solution.fromQuotient_mk

added theorem Module.Relations.Solution.mapToKer_coe

added theorem Module.Relations.Solution.ofQuotient_fromQuotient

added theorem Module.Relations.Solution.ofQuotient_isPresentation

added theorem Module.Relations.Solution.ofQuotient_π

added theorem Module.Relations.Solution.ofπ'_π

added theorem Module.Relations.Solution.ofπ_π

added def Module.Relations.Solution.postcomp

added theorem Module.Relations.Solution.span_relation_le_ker_π

added theorem Module.Relations.Solution.π_comp_map

added theorem Module.Relations.Solution.π_comp_map_apply

added theorem Module.Relations.Solution.π_relation

added theorem Module.Relations.Solution.π_single

added structure Module.Relations.Solution

added theorem Module.Relations.ker_toQuotient

added theorem Module.Relations.map_single

added theorem Module.Relations.range_map

added theorem Module.Relations.surjective_toQuotient

added def Module.Relations.toQuotient

added theorem Module.Relations.toQuotient_relation

added structure Module.Relations