Commit 2024-11-02 13:54 0ebaf5f5

View on Github →

feat(Algebra/Module): relation between Module.FinitePresentation and Module.Presentation (#18408) A module is finitely presented (in the sense of Module.Presentation) iff it has a presentation (in the sense of Module.Presentation) with finitely many generators and relations. The basic API for the presentation of modules is slightly improved: it should be more stable after this PR is merged.

Estimated changes

Modified Mathlib.lean

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

deleted theorem Module.Relations.Solution.IsPresentation.surjective_mapToKer

added theorem Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span

added theorem Module.Relations.Solution.isPresentation_iff

added theorem Module.Relations.Solution.isPresentation_mk

deleted theorem Module.Relations.Solution.mapToKer_coe

added theorem Module.Relations.Solution.range_π

added theorem Module.Relations.Solution.surjective_fromQuotient_iff_surjective_π

added theorem Module.Relations.Solution.surjective_π_iff_span_eq_top

added theorem Module.Relations.toQuotient_map

added theorem Module.Relations.toQuotient_map_apply

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

added theorem Module.Presentation.finite

added theorem Module.Presentation.finitePresentation

added theorem Module.finitePresentation_iff_exists_presentation

Modified Mathlib/RingTheory/Finiteness.lean

added theorem Submodule.fg_iff_exists_finite_generating_family