[Merged by Bors] - feat: more API for Function.Exact#14520
[Merged by Bors] - feat: more API for Function.Exact#14520
Conversation
PR summary 889da084dd
|
| 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 filesMathlib.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>|
I have no serious comment to make except questions about the way mathlib is supposed to handle namespaces. The multiple invocations of |
I had just replicated the same organization which was already in this file in the |
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
|
Thanks! bors merge |
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. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
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 relateFunction.ExactandShortComplex.Exactin 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 ofShortComplex.Exact, proofs useFunction.Exactbecause I need to change universes.