[Merged by Bors] - feat: more API for Function.Exact

[joelriou]

If two diagrams involving additive maps are isomorphic, one is exact (in the sense of Function.Exact) iff the other is. In this PR, we also relate Function.Exact and ShortComplex.Exact in the categories of abelian groups and modules over a ring.

---

This shall be used in the (draft) PR #14515 which constructs the covariant long exact sequence of Ext-groups: even though this is phrased in terms of ShortComplex.Exact, proofs use Function.Exact because I need to change universes.

[github-actions]

PR summary 889da084dd

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Homology.ShortComplex.Ab	1141	1142	+1 (+0.09%)
Mathlib.Algebra.Homology.ShortComplex.ModuleCat	1157	1158	+1 (+0.09%)

Import changes for all files

Files

Import difference

13 files Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.Algebra.Category.Grp.AB5 Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.GroupTheory.FiniteAbelian Mathlib.Algebra.Module.PID Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Category.ModuleCat.Free Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Algebra.Homology.ConcreteCategory

1

---

Declarations diff

+ LinearEquiv.conj_exact_iff_exact
+ ShortExact.ab_exact_iff_function_exact
+ ShortExact.moduleCat_exact_iff_function_exact
+ addMonoidHom_comp_eq_zero
+ addMonoidHom_ker_eq
+ apply_apply_eq_zero
+ comp_eq_zero
+ comp_injective
+ iff_of_ladder_addEquiv
+ of_comp_eq_zero_of_ker_in_range
+ of_comp_of_mem_range
+ of_ladder_addEquiv_of_exact
+ of_ladder_addEquiv_of_exact'
++ exact_iff
++ exact_of_comp_eq_zero_of_ker_le_range
++ exact_of_comp_of_mem_range
- Exact.apply_apply_eq_zero
- Exact.comp_eq_zero
- Exact.comp_injective
- Exact.of_comp_eq_zero_of_ker_in_range
- Exact.of_comp_of_mem_range
- _root_.LinearEquiv.conj_exact_iff_exact
- _root_.LinearMap.exact_iff
- _root_.LinearMap.exact_of_comp_eq_zero_of_ker_le_range
- _root_.LinearMap.exact_of_comp_of_mem_range

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[AntoineChambert-Loir]

I have no serious comment to make except questions about the way mathlib is supposed to handle namespaces. The multiple invocations of _root_. (lines 78ff of Exact.lean) make me feel one should organize the code slightly differently (for readability, and also to minimize risks of giving functions an incorrect/inconsistent namespace), but I have no idea of what to do. (It has to do with the organization of a file in sections, and the behaviour of namespace, habits seem to differ.)

[joelriou]

I have no serious comment to make except questions about the way mathlib is supposed to handle namespaces. The multiple invocations of _root_. (lines 78ff of Exact.lean) make me feel one should organize the code slightly differently

I had just replicated the same organization which was already in this file in the LinearMap part. I have slightly reorganized the file so that there are no longer _root_.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style