OAI/Algebra/AuslanderReiten/Cones/ConeQuotientMap.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.ConeQuotientMap.Source line 17
2. abbrev OAI.ArExplicit.ConeQuotientMap.Target line 18
3. abbrev OAI.ArExplicit.ConeQuotientMap.Cone line 19
4. def OAI.ArExplicit.ConeQuotientMap.kernelInclusion line 26
5. def OAI.ArExplicit.ConeQuotientMap.quotientMap line 29
6. theorem OAI.ArExplicit.ConeQuotientMap.quotientMap_mk line 41
7. theorem OAI.ArExplicit.ConeQuotientMap.kernelInclusion_apply line 46
8. theorem OAI.ArExplicit.ConeQuotientMap.kernelInclusion_injective line 51
9. theorem OAI.ArExplicit.ConeQuotientMap.quotientMap_surjective line 72
10. theorem OAI.ArExplicit.ConeQuotientMap.exact line 79
11. def OAI.ArExplicit.ConeQuotientMap.stableIsomorphism line 107