ShortExact

Statistics

Metric	Count
Definitions	0
Theorems `reflects_shortExact_of_faithful`, `shortExact_map_iff`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`reflects_shortExact_of_faithful` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.map`	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Functor.reflects_exact_of_faithful` `CategoryTheory.ShortComplex.ShortExact.exact` `CategoryTheory.Functor.ReflectsMonomorphisms.reflects` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `CategoryTheory.ShortComplex.ShortExact.mono_f` `CategoryTheory.Functor.ReflectsEpimorphisms.reflects` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `CategoryTheory.ShortComplex.ShortExact.epi_g`
`shortExact_map_iff` 📖	mathematical	—	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.map`	—	`reflects_shortExact_of_faithful` `CategoryTheory.ShortComplex.ShortExact.map_of_exact`

---