Transfer

📁 Source: Mathlib/CategoryTheory/Preadditive/Transfer.lean

Statistics

Metric	Count
Definitions ofFullyFaithful	1
Theorems additive_inverse_of_FullyFaithful, additive_ofFullyFaithful	2
Total	3

CategoryTheory.Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
additive_inverse_of_FullyFaithful 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.Preadditive.ofFullyFaithful functor fullyFaithfulFunctor inverse	—	inverse_additive CategoryTheory.Functor.FullyFaithful.additive_ofFullyFaithful

CategoryTheory.Functor.FullyFaithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
additive_ofFullyFaithful 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.Preadditive.ofFullyFaithful	—	map_preimage

CategoryTheory.Preadditive

Definitions

Name	Category	Theorems
ofFullyFaithful 📖	CompOp	2 math math: CategoryTheory.Functor.FullyFaithful.additive_ofFullyFaithful, CategoryTheory.Equivalence.additive_inverse_of_FullyFaithful

---

← Back to Index