Transfer

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

Statistics

Metric	Count
Definitions abelian, preadditive, abelian, preadditive, abelianOfAdjunction, abelianOfEquivalence	6
Theorems hasCokernels, hasKernels, hasFiniteLimits, hasLimitsOfShape, instAdditiveDown, instAdditiveUp, hasFiniteLimits, hasLimitsOfShape, instAdditiveFunctor, instAdditiveInverse	10
Total	16

CategoryTheory

Definitions

Name	Category	Theorems
abelianOfAdjunction 📖	CompOp	—
abelianOfEquivalence 📖	CompOp	—

CategoryTheory.AbelianOfAdjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCokernels 📖	mathematical	—	CategoryTheory.Limits.HasCokernels CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Adjunction.leftAdjoint_preservesColimits CategoryTheory.NatIso.naturality_1 CategoryTheory.Limits.hasCokernel_epi_comp CategoryTheory.Limits.hasCokernel_comp_iso CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.NatIso.hom_app_isIso CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.inv_app_isIso
hasKernels 📖	mathematical	—	CategoryTheory.Limits.HasKernels CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.NatIso.naturality_1 CategoryTheory.Limits.hasKernel_iso_comp CategoryTheory.NatIso.inv_app_isIso CategoryTheory.Limits.hasKernel_comp_mono CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.Functor.instIsSplitMonoApp CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom

CategoryTheory.AsSmall

Definitions

Name	Category	Theorems
abelian 📖	CompOp	—
preadditive 📖	CompOp	2 math math: instAdditiveDown, instAdditiveUp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits CategoryTheory.AsSmall CategoryTheory.instSmallCategoryAsSmall	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.AsSmall CategoryTheory.instSmallCategoryAsSmall	—	CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence CategoryTheory.Equivalence.isEquivalence_inverse
instAdditiveDown 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.AsSmall CategoryTheory.instSmallCategoryAsSmall preadditive down	—	CategoryTheory.Functor.FullyFaithful.additive_ofFullyFaithful
instAdditiveUp 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.AsSmall CategoryTheory.instSmallCategoryAsSmall preadditive up	—	CategoryTheory.Equivalence.additive_inverse_of_FullyFaithful

CategoryTheory.ShrinkHoms

Definitions

Name	Category	Theorems
abelian 📖	CompOp	1 math math: isGrothendieckAbelian
preadditive 📖	CompOp	2 math math: instAdditiveInverse, instAdditiveFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits CategoryTheory.ShrinkHoms instCategory	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.ShrinkHoms instCategory	—	CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence instIsEquivalenceInverse
instAdditiveFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.ShrinkHoms instCategory preadditive functor	—	CategoryTheory.Equivalence.additive_inverse_of_FullyFaithful
instAdditiveInverse 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.ShrinkHoms instCategory preadditive inverse	—	CategoryTheory.Functor.FullyFaithful.additive_ofFullyFaithful

---

← Back to Index