Ulift

📁 Source: Mathlib/Algebra/Category/ModuleCat/Ulift.lean

Statistics

Metric	Count
Definitions fullyFaithfulUliftFunctor, uliftFunctor, uliftFunctorForgetIso	3
Theorems instAdditiveUliftFunctor, instFaithfulUliftFunctor, instFullUliftFunctor, instLinearUliftFunctor, instPreservesFiniteColimitsUliftFunctor, instPreservesFiniteLimitsUliftFunctor, instPreservesInjectiveObjectsUliftFunctorOfSmall, instPreservesLimitsOfSizeUliftFunctor, instPreservesProjectiveObjectsUliftFunctorOfSmall, uliftFunctorForgetIso_hom_app, uliftFunctorForgetIso_inv_app, uliftFunctor_map, uliftFunctor_map_exact, uliftFunctor_obj	14
Total	17

ModuleCat

Definitions

Name	Category	Theorems
fullyFaithfulUliftFunctor 📖	CompOp	—
uliftFunctor 📖	CompOp	14 math math: instFullUliftFunctor, instPreservesFiniteColimitsUliftFunctor, uliftFunctorForgetIso_hom_app, uliftFunctorForgetIso_inv_app, uliftFunctor_map_exact, instAdditiveUliftFunctor, instFaithfulUliftFunctor, instPreservesLimitsOfSizeUliftFunctor, uliftFunctor_map, instPreservesFiniteLimitsUliftFunctor, uliftFunctor_obj, instPreservesInjectiveObjectsUliftFunctorOfSmall, instPreservesProjectiveObjectsUliftFunctorOfSmall, instLinearUliftFunctor
uliftFunctorForgetIso 📖	CompOp	2 math math: uliftFunctorForgetIso_hom_app, uliftFunctorForgetIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive ModuleCat moduleCategory instPreadditive uliftFunctor	—	—
instFaithfulUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful ModuleCat moduleCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Full ModuleCat moduleCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.full
instLinearUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring ModuleCat CommRing.toRing moduleCategory instPreadditive instLinear uliftFunctor	—	—
instPreservesFiniteColimitsUliftFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits ModuleCat moduleCategory uliftFunctor	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveUliftFunctor List.TFAE.out CategoryTheory.Functor.exact_tfae uliftFunctor_map_exact
instPreservesFiniteLimitsUliftFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits ModuleCat moduleCategory uliftFunctor	—	CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits instPreservesLimitsOfSizeUliftFunctor
instPreservesInjectiveObjectsUliftFunctorOfSmall 📖	mathematical	—	CategoryTheory.Functor.PreservesInjectiveObjects ModuleCat moduleCategory uliftFunctor	—	Module.injective_iff_injective_object Module.ulift_injective_of_injective
instPreservesLimitsOfSizeUliftFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize ModuleCat moduleCategory uliftFunctor	—	CategoryTheory.Limits.comp_preservesLimits forget_preservesLimits CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves forget_reflectsLimitsOfSize
instPreservesProjectiveObjectsUliftFunctorOfSmall 📖	mathematical	—	CategoryTheory.Functor.PreservesProjectiveObjects ModuleCat moduleCategory uliftFunctor	—	small_lift IsProjective.iff_projective Module.Projective.of_equiv projective_of_module_projective RingHomInvPair.ids
uliftFunctorForgetIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat moduleCategory CategoryTheory.types CategoryTheory.Functor.comp uliftFunctor CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftFunctor uliftFunctorForgetIso	—	—
uliftFunctorForgetIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat moduleCategory CategoryTheory.types CategoryTheory.Functor.comp uliftFunctor CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftFunctor uliftFunctorForgetIso	—	—
uliftFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map ModuleCat moduleCategory uliftFunctor ofHom carrier ULift.addCommGroup isAddCommGroup ULift.module' Ring.toSemiring AddCommGroup.toAddCommMonoid isModule LinearMap.comp ULift.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearEquiv.toLinearMap LinearEquiv.symm ULift.moduleEquiv Hom.hom	—	—
uliftFunctor_map_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	CategoryTheory.ShortComplex.map uliftFunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveUliftFunctor	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveUliftFunctor CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
uliftFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj ModuleCat moduleCategory uliftFunctor of carrier ULift.addCommGroup isAddCommGroup ULift.module' Ring.toSemiring AddCommGroup.toAddCommMonoid isModule	—	—

---

← Back to Index