Commit 2024-10-30 05:45 39773322

View on Github →

feat(Algebra/Module): characterizations of free modules in terms of their presentations (#18327) In this PR, the API for the presentations of modules is slightly developed (uniqueness up to a linear equivalence of the module defined by generators and relations, constructor for the property IsPresentation), and this is used to show that a module is free iff it admits a presentation with generators and no relation.

depends on: #18295

Estimated changes

Modified Mathlib.lean

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

added def Module.Presentation.ofIsPresentation

added theorem Module.Relations.Quotient.linearMap_ext

added def Module.Relations.Quotient

added theorem Module.Relations.Solution.IsPresentation.ofLinearEquiv

added theorem Module.Relations.Solution.IsPresentation.postcomp_desc

added theorem Module.Relations.Solution.IsPresentation.postcomp_uniq

added theorem Module.Relations.Solution.IsPresentation.postcomp_uniq_symm

added theorem Module.Relations.Solution.IsPresentation.uniq_symm_var

added theorem Module.Relations.Solution.IsPresentation.uniq_var

added theorem Module.Relations.Solution.IsPresentationCore.desc_var

added def Module.Relations.Solution.IsPresentationCore.down

added theorem Module.Relations.Solution.IsPresentationCore.isPresentation

added structure Module.Relations.Solution.IsPresentationCore

added theorem Module.Relations.Solution.congr_postcomp

added theorem Module.Relations.Solution.congr_var

deleted theorem Module.Relations.Solution.fromQuotient_mk

added theorem Module.Relations.Solution.fromQuotient_toQuotient

added theorem Module.Relations.Solution.postcomp_comp

added theorem Module.Relations.Solution.postcomp_id

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

added theorem Module.Relations.Solution.IsPresentation.free

added theorem Module.Relations.solutionFinsupp_isPresentation

added theorem Module.free_iff_exists_presentation