Commit 2024-11-09 14:01 5679548c

View on Github →

feat(LinearAlgebra/Dual): generalize results from Free to Projective (#18686) Also show that:

A finite projective module is also finitely presented (generalized from Free)
A direct summand of a reflexive module is reflexive. In particular, a finite projective module is reflexive.

Estimated changes

Modified Mathlib/Algebra/Module/FinitePresentation.lean

deleted theorem Module.finitePresentation_of_free

added theorem Module.finitePresentation_of_projective

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

added theorem LinearMap.injective_of_comp_eq_id

modified def LinearMap.inverse

added theorem LinearMap.surjective_of_comp_eq_id

Modified Mathlib/Algebra/Module/Projective.lean

Modified Mathlib/Algebra/Module/Submodule/Range.lean

added theorem LinearMap.injective_rangeRestrict_iff

added theorem LinearMap.ker_eq_range_of_comp_eq_id

Modified Mathlib/LinearAlgebra/Dual.lean

added theorem Module.Dual.eval_naturality

added theorem Module.IsReflexive.of_split

modified theorem Module.dual_rank_eq

modified theorem Module.erange_coe

modified theorem Module.eval_ker

modified theorem Module.finite_dual_iff

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Basic.lean

Modified Mathlib/RingTheory/Finiteness.lean

added theorem Module.Finite.exists_comp_eq_id_of_projective

Modified Mathlib/RingTheory/Localization/Free.lean